Models of ZF with Infinity are uncountable

Require Export ST.

Section Uncountable.

(* We assume a countable model containing a set omega
that is an injective image of nat *)

Variable set : SetStruct.
Variable ZFS : ZF set.

Variable f : nat -> set.
Variable f_sur : forall x, exists n, f n = x.

Variable num : nat -> set.
Variable num_inj : forall m n, num m = num n -> m = n.

Definition Num x :=
exists n, x = num n.

Variable ident omega : set.
Variable Inf : agree Num omega.

(* With a diagonalisation argument we derive a contradiction *)

Definition N n :=
(num n) nel (f n).

Definition M :=
omega ! fun x => exists n, num n = x /\ N n.

Lemma help n :
f n = M -> (num n nel M <-> (num n el omega /\ (exists m, num m = num n /\ N m))).
Proof.
intros H. split; intros I.
- split.
+ apply Inf. now exists n.
+ exists n. split; trivial. unfold N. now rewrite H.
- intros J. destruct I as [I1[m[I2 I3]]].
apply I3. apply num_inj in I2. subst m. now rewrite H.
Qed.

Lemma false :
False.
Proof.
destruct (f_sur M) as [n H].
specialize (sep_el omega (fun x => exists n, num n = x /\ N n)).
intros I. specialize (I (num n)). fold N in I.
apply help in H. tauto.
Qed.

End Uncountable.