Zermelo's Embedding Theorem

Require Export Stage.

(* Definition of Iso, the model similarity *)

Definition btot (M N : ZFStruct) (R : M -> N -> Prop) x a :=
forall y, y el x -> exists b, b el a /\ R y b.

Definition bsur (M N : ZFStruct) (R : M -> N -> Prop) x a :=
forall b, b el a -> exists y, y el x /\ R y b.

Inductive Iso (M N : ZFStruct) (x : M) (a : N) : Prop :=
| II : btot Iso x a -> bsur Iso x a -> Iso x a.

Definition iso (M N : ZFStruct) :=
total (@Iso M N) /\ surjective (@Iso M N).

(* Iso is symmetric *)

Lemma Iso_sym (M N : ZFStruct) (MZF : ZF M) (x : M) (a : N) :
Iso x a -> Iso a x.
Proof.
assert (H : WF x) by apply MZF.
revert a. induction H as [x _ IHx].
intros a [H1 H2]. split.
- intros b B. destruct (H2 b B) as [y[Y1 Y2]].
exists y. split; trivial. apply IHx; trivial.
- intros y Y. destruct (H1 y Y) as [b[B1 B2]].
exists b. split; trivial. apply IHx; trivial.
Qed.

Lemma btot_bsur (M N : ZFStruct) {MZF : ZF M} {NZF : ZF N} (x : M) (a : N) :
btot (@Iso M N) x a <-> bsur (@Iso N M) a x.
Proof.
split.
- intros H y Y. destruct (H y Y) as [b[B1 B2]].
exists b. split; trivial. now apply Iso_sym.
- intros H y Y. destruct (H y Y) as [b[B1 B2]].
exists b. split; trivial. now apply Iso_sym.
Qed.

(* Iso is functional and respects membership *)

Section Iso.

Context { M : ZFStruct }.
Context { MZF : ZF M }.

Context { N : ZFStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Definition domain x :=
exists a, Iso x a.

Definition range a :=
exists x, Iso x a.

Fact tot_sur :
surjective (@Iso N M) <-> total (@Iso M N).
Proof.
split; intros H x; destruct (H x) as [a I % Iso_sym]; eauto.
Qed.

Fact Iso_btot x a :
Iso x a -> btot (@Iso M N) x a.
Proof.
now intros [].
Qed.

Fact Iso_bsur x a :
Iso x a -> bsur (@Iso M N) x a.
Proof.
now intros [].
Qed.

Lemma Iso_fun :
functional (@Iso M N).
Proof.
intros x.
induction (AxWF x) as [x _ IH].
intros a b [H1 H2] [I1 I2].
apply Ext; intros c C.
- destruct (H2 c C) as [y [Y1 Y2]].
destruct (I1 y Y1) as [d [D1 D2]].
rewrite (IH y Y1 c d); eauto.
- destruct (I2 c C) as [y [Y1 Y2]].
destruct (H1 y Y1) as [d [D1 D2]].
rewrite (IH y Y1 c d); eauto.
Qed.

Lemma Iso_res x y a b :
Iso x a -> Iso y b -> y el x -> b el a.
Proof.
intros [X _] Y H.
destruct (X y H) as [b'[B1 B2]].
now rewrite (Iso_fun Y B2).
Qed.

End Iso.

(* Iso respects the other set constructors *)

Section Cons.

Context { M : ZFStruct }.
Context { MZF : ZF M }.

Context { N : ZFStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Fact Iso_inj :
injective (@Iso M N).
Proof.
intros x y a X % Iso_sym Y % Iso_sym; trivial.
apply (Iso_fun X Y).
Qed.

Fact Iso_mem x y a b :
Iso x a -> Iso y b -> (y el x <-> b el a).
Proof.
intros X Y. split; intros H.
- now apply (Iso_res X Y).
- now apply (Iso_res (Iso_sym MZF X) (Iso_sym MZF Y)).
Qed.

Lemma btot_eset :
btot (@Iso M N) 0 0.
Proof.
intros x H. auto.
Qed.

Lemma btot_union x a :
btot (@Iso M N) x a -> btot (@Iso M N) (union x) (union a).
Proof.
intros H y [z[Z1 Z2]] % Union.
destruct (H z Z1) as [c[C1 [C2 _]]].
destruct (C2 y Z2) as [b[B1 B2]].
exists b. split; trivial. apply Union. now exists c.
Qed.

Lemma btot_power x a :
btot (@Iso M N) x a -> btot (@Iso M N) (power x) (power a).
Proof.
intros H y Y % Power.
pose (b := sep (fun c => exists z, z el y /\ Iso z c) a).
exists b. split; try apply Power, sep_sub. split.
- intros z Z. destruct (H z (Y z Z)) as [c [C1 C2]].
exists c. split; trivial. apply sep_el. split; eauto.
- intros c C. now apply sep_el in C as [].
Qed.

Definition MtoN (R : M -> M -> Prop) a b :=
exists x y, Iso x a /\ Iso y b /\ R x y.

Fact MtoN_fun R :
functional R -> functional (MtoN R).
Proof.
intros H a b c (x&y&I1&I2&I3) (x'&z&J1&J2&J3).
rewrite (Iso_inj J1 I1) in J3.
rewrite (H x y z I3 J3) in I2.
apply (Iso_fun I2 J2).
Qed.

Lemma btot_rep R x a :
functional R -> (rep R x) <=c domain ->
btot (@Iso M N) x a -> btot (@Iso M N) (rep R x) (rep (MtoN R) a).
Proof with eauto using MtoN_fun.
intros FR XD H y Y. destruct (XD y Y) as [b B].
exists b. split; trivial. apply Rep...
apply Rep in Y as [z[Z1 Z2]]...
destruct (H z Z1) as [c[C1 C2]].
exists c. split; trivial. now exists z, y.
Qed.

Fact bsur_rep R x a :
functional R -> (rep R x) <=c domain ->
Iso x a -> bsur (@Iso M N) (rep R x) (rep (MtoN R) a).
Proof with eauto using MtoN_fun.
intros FR XD H b B. apply Rep in B as [c[C[z[y[Z[Y I]]]]]]...
exists y. split; trivial. apply Rep... exists z. split; trivial.
now apply (Iso_mem H Z).
Qed.

End Cons.

(* The domain forms a universe *)

Section Domain.

Context { M : ZFStruct }.
Context { MZF : ZF M }.

Context { N : ZFStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Lemma Iso_eset :
(@Iso M N) 0 0.
Proof.
split.
- apply btot_eset.
- now apply btot_bsur, btot_eset.
Qed.

Lemma Iso_union x a :
Iso x a -> Iso (union x) (union a).
Proof.
intros [H I]. split.
- now apply btot_union.
- now apply btot_bsur, btot_union, btot_bsur.
Qed.

Lemma Iso_power x a :
Iso x a -> Iso (power x) (power a).
Proof.
intros [H I]. split.
- now apply btot_power.
- now apply btot_bsur, btot_power, btot_bsur.
Qed.

Lemma Iso_rep R x a :
functional R -> (rep R x) <=c domain ->
Iso x a -> Iso (rep R x) (rep (MtoN R) a).
Proof.
intros FR XD H. split.
- now apply btot_rep, H.
- now apply bsur_rep.
Qed.

Fact Iso_dom x a :
Iso x a -> (@domain M N) x.
Proof.
intros H. now exists a.
Qed.

Fact Iso_dom' x a :
Iso x a -> (@domain N M) a.
Proof.
intros H % Iso_sym; trivial. unfold domain. now exists x.
Qed.

Fact domain_union x :
domain x -> domain (union x).
Proof.
intros [a H % Iso_union]. now exists (union a).
Qed.

Fact domain_power x :
domain x -> domain (power x).
Proof.
intros [a H % Iso_power]. now exists (power a).
Qed.

Fact domain_rep R x :
functional R -> (rep R x) <=c domain ->
domain x -> domain (rep R x).
Proof.
intros FR XD [a H % (Iso_rep FR XD)]. eapply Iso_dom, H.
Qed.

Fact domain_el x y :
domain x -> y el x -> domain y.
Proof.
intros [a H] I. destruct (Iso_btot H I) as [b [_ J]]. now exists b.
Qed.

Fact domain_sub x y :
domain x -> y <<= x -> domain y.
Proof.
intros [a H % Iso_power] I % Power.
destruct (Iso_btot H I) as [b [_ J]]. now exists b.
Qed.

Fact union_domain x :
domain (union x) -> domain x.
Proof.
intros [b H % Iso_power % Iso_power].
assert (I : x el (power (power (union x)))).
- apply Power. intros y I. apply Power. now apply union_el_sub.
- destruct (Iso_btot H I) as [a [_ J]]. now exists a.
Qed.

Lemma domain_universe :
agree (@domain M N) <=p universe.
Proof.
intros u H. apply ZF_rep. repeat split.
- intros x y X % H Y. apply H. now apply (domain_el X Y).
- apply H. exists 0. apply Iso_eset.
- intros x X % H. apply H. now apply domain_union.
- intros x X % H. apply H. now apply domain_power.
- intros R x FR X XD. apply H. apply domain_rep; trivial; try now apply H.
intros y [z [Z1 Z2]] % Rep; trivial. apply H.
apply XD. apply Rep; trivial. now exists z.
Qed.

Lemma Iso_Stage x a :
Iso x a -> Stage x -> Stage a.
Proof.
intros H I. revert a H. induction I as [x I IH | x I IH].
- intros b H. destruct (Iso_btot H (power_eager x)) as [a [A1 A2]].
specialize (IH a A2). apply Iso_power in A2.
rewrite <- (Iso_fun A2); auto. now constructor.
- intros b H. destruct (union_domain (Iso_dom H)) as [a J].
rewrite (Iso_fun H (Iso_union J)). constructor. intros c C.
destruct (Iso_bsur J C) as [y [Y1 Y2]]. now apply (IH y).
Qed.

End Domain.

(* Iso respects universes and strength *)

Section Universes.

Context { M : ZFStruct }.
Context { MZF : ZF M }.

Context { N : ZFStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Fact Iso_trans x a :
Iso x a -> trans x -> trans a.
Proof.
intros H1 H2 b c B C.
destruct (Iso_bsur H1 B) as [y[Y1 Y2]].
destruct (Iso_bsur Y2 C) as [z[Z1 Z2]].
apply (Iso_mem H1 Z2). now apply (H2 y).
Qed.

Fact Iso_closed_union x a :
Iso x a -> closed_union (cl x) -> closed_union (cl a).
Proof.
intros H1 H2 b B. destruct (Iso_bsur H1 B) as [y[Y1 Y2]].
apply Iso_union in Y2. now apply (Iso_mem H1 Y2), H2.
Qed.

Fact Iso_closed_power x a :
Iso x a -> closed_power (cl x) -> closed_power (cl a).
Proof.
intros H1 H2 b B. destruct (Iso_bsur H1 B) as [y[Y1 Y2]].
apply Iso_power in Y2. now apply (Iso_mem H1 Y2), H2.
Qed.

Fact Iso_closed_rep x a :
Iso x a -> closed_rep (cl x) -> closed_rep (cl a).
Proof.
intros H1 H2 R b H3 B H4. destruct (Iso_bsur H1 B) as [y[Y1 Y2]].
apply Iso_sym, (Iso_rep H3) in Y2 as Y3; trivial.
- apply Iso_sym in H1; trivial.
apply (Iso_mem H1 Y3), H2; trivial.
+ now apply MtoN_fun.
+ intros z [z' [Z1 [c [c'[C1 [C2 C3]]]]]] % Rep; try now apply MtoN_fun.
apply (Iso_mem H1 C2). apply (H4 c').
apply Rep; trivial. exists c. split; trivial.
now apply (Iso_mem Y2 C1).
- intros c [d[D1 D2]] % Rep; trivial.
apply (domain_el (x:=a)); trivial.
+ exists x. now apply Iso_sym.
+ apply (H4 c). apply Rep; trivial. now exists d.
Qed.

Lemma Iso_universe x a :
Iso x a -> universe x -> universe a.
Proof.
intros H1 H2. apply ZF_rep. repeat split.
- apply (Iso_trans H1), universe_trans, H2.
- apply (Iso_mem H1 Iso_eset). apply H2.
- apply (Iso_closed_union H1), H2.
- apply (Iso_closed_power H1), H2.
- apply (Iso_closed_rep H1), ZF_rep, H2.
Qed.

Fact Iso_strength n x a :
strength n x -> Iso x a -> strength n a.
Proof.
revert x a. induction n; simpl; intros x a H1; auto.
intros H2. destruct H1 as [y[Y1[Y2 Y3]]].
destruct (Iso_btot H2 Y1) as [b[B1 B2]].
exists b. split; trivial. split; try now apply (IHn y).
now apply (Iso_universe B2).
Qed.

End Universes.

Section Stages.

Context { M : ZFStruct }.
Context { MZF : ZF M }.

Context { N : ZFStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Fact Stage_btot x a :
least (fun x' => Stage x' /\ ~ domain x') x -> Stage a -> ~ (@domain N M) a -> btot (@Iso M N) x a.
Proof.
intros [[XS XD] XL] AS AR.
induction XS as [x H IH | x H IH].
- exfalso. destruct (classic (domain x)).
+ now apply XD, domain_power.
+ now apply (power_above (x:=x)), XL.
- destruct (Stage_dicho H) as [I|I]; try now apply IH.
intros y Y. apply Union in Y as [z [Z1 Z2]].
destruct (classic (domain z)) as [[c C]|J].
+ assert (CS : Stage c) by exact (Iso_Stage C (H z Z1)).
destruct (Stage_lin_el AS CS) as [J|J].
* exfalso. apply AR. apply (domain_sub (Iso_dom' C) J).
* destruct (Iso_btot C Z2) as [b [B1 B2]].
exists b. split; trivial. now apply (Stage_trans AS J).
+ exfalso. apply (WF_no_loop (x:=z)).
assert (Z : Stage z) by now apply H. apply XL; auto.
Qed.

Fact not_total_exists :
~ total (@Iso M N) -> exists x, Stage x /\ ~ domain x.
Proof.
intros H. contra H1. apply H.
intros y. contra H2. apply H1.
destruct (WF_reachable y) as [z [Z1 Z2]].
exists z. split; trivial. intros [a I].
destruct (Iso_btot I Z2) as [b [B1 B2]].
apply H2. now exists b.
Qed.

Lemma domain_Stage_sub x :
total (@Iso N M) -> Stage x -> ~ domain x -> domain <=s x.
Proof.
intros S H I y [a A].
destruct (WF_reachable a) as [b [B1 B2]].
destruct (S b) as [z H1].
assert (H2 : Stage z) by now apply (Iso_Stage H1).
apply Iso_sym in H1; trivial.
assert (H3 : y el z) by now apply (Iso_mem H1 A).
destruct (Stage_lin_el H2 H) as [J|J]; auto.
contradict I. apply (domain_el (Iso_dom H1) J).
Qed.

Lemma not_total_domain :
~ total (@Iso M N) -> total (@Iso N M) -> small (@domain M N).
Proof.
intros H I. apply not_total_exists in H as [x [X1 X2]].
apply (bounded_small (domain_Stage_sub I X1 X2)).
Qed.

Fact range_domain x :
@ domain M N x <-> @ range N M x.
Proof.
split; intros [a H % Iso_sym]; trivial; now exists a.
Qed.

Fact range_domain_small x :
agree (@domain M N) x <-> agree (@range N M) x.
Proof.
split; intros X; intros y; split; intros H.
- now apply range_domain, X.
- now apply X, range_domain.
- now apply range_domain, X.
- now apply X, range_domain.
Qed.

Fact range_universe :
agree (@range N M) <=p universe.
Proof.
intros x H. apply domain_universe.
now apply range_domain_small.
Qed.

End Stages.

(* Main results *)

(* We assume two models of ZF for the rest of the development *)

Section Main.

Context { M : ZFStruct }.
Context { MZF : ZF M }.

Context { N : ZFStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Fact Stage_Iso x a :
least (fun x' => Stage x' /\ ~ (@domain M N) x') x ->
least (fun a' => Stage a' /\ ~ (@domain N M) a') a ->
Iso x a.
Proof.
intros H I. split.
- apply Stage_btot; trivial; apply I.
- apply btot_bsur; auto.
apply Stage_btot; trivial; apply H.
Qed.

Lemma Iso_Stage_max :
Stage <=p (@domain M N) \/ Stage <=p (@domain N M).
Proof.
contra H. apply not_or_and in H as [H1 H2].
apply class_not_sub in H1 as [x[X1 X2]].
apply class_not_sub in H2 as [a[A1 A2]].
destruct (Stage_least (p:=fun x => ~ (@domain M N) x) X1 X2) as [y HY].
destruct (Stage_least (p:=fun a => ~ (@domain N M) a) A1 A2) as [b HB].
apply HY. exists b. now apply Stage_Iso.
Qed.

Theorem Iso_max :
total (@Iso M N) \/ surjective (@Iso M N).
Proof.
contra H. apply not_or_and in H as [H1 H2]. rewrite tot_sur in H2.
apply not_total_exists in H1 as [x [X1 X2]].
apply not_total_exists in H2 as [a [A1 A2]].
destruct (Iso_Stage_max) as [H|H]; auto.
Qed.

Theorem Iso_tricho :
iso M N \/
(surjective (@Iso M N) /\ small (@domain M N)) \/
(total (@Iso M N) /\ small (@range M N)).
Proof.
destruct (classic (total (@Iso M N))), (classic (surjective (@Iso M N))).
- now left.
- right. right. split; trivial. rewrite tot_sur in H0.
apply not_total_domain in H0 as [x X]; trivial.
exists x. now apply range_domain_small.
- right. left. split; trivial.
rewrite tot_sur in H0. now apply not_total_domain.
Qed.

(* To simplify further proofs, we turn the relation Iso into two functions *)

Definition i x := delta (fun a => Iso x a).
Definition j a := delta (fun x => Iso x a).

Fact j_Iso a :
(@range M N) a -> Iso (j a) a.
Proof.
intros [x H]. unfold j. eapply delta_spec; eauto.
hnf. intros. apply (Iso_inj H0 H1).
Qed.

Fact i_Iso x :
(@domain M N) x -> Iso x (i x).
Proof.
intros [a H]. unfold i. eapply delta_spec; eauto.
hnf. intros. apply (Iso_fun H0 H1).
Qed.

Fact ij a :
(@range M N) a -> i (j a) = a.
Proof.
intros H. apply delta_eq.
- hnf. apply Iso_fun.
- now apply j_Iso.
Qed.

Fact ji x :
(@domain M N) x -> j (i x) = x.
Proof.
intros H. apply delta_eq.
- hnf. intros. eapply Iso_inj; eauto.
- now apply i_Iso.
Qed.

Fact j_dom a :
surjective (@Iso M N) -> (@domain M N) (j a).
Proof.
intros H. exists a. apply j_Iso, H.
Qed.

Fact i_ran x :
total (@Iso M N) -> (@range M N) (i x).
Proof.
intros H. exists x. apply i_Iso, H.
Qed.

End Main.