# Equivalence of ZF>=1 and ZF+Inf

Require Export Stage.

Section Infinity.

(* We assume a model of ZF and define binary union and adjunction *)

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

Lemma binunion_el x y z :
z el binunion x y <-> z el x \/ z el y.
Proof.
split; intros H.
- apply Union in H as [y'[Y1 Y2]].
apply pair_el in Y1 as [->| ->]; auto.
- destruct H as [H|H]; apply Union.
* exists x. split; trivial. apply Pair. now left.
* exists y. split; trivial. apply Pair. now right.
Qed.

binunion y (sing x).

Lemma adj_el x y z :
z el adj x y <-> z el y \/ z = x.
Proof.
split; intros H.
- apply binunion_el in H as [H|H]; auto.
apply sing_el in H as ->. now right.
- destruct H as [H| ->]; apply binunion_el; auto.
right. apply sing_el. reflexivity.
Qed.

## Definition of Omega

Hypothesis MI :
Inf M.

Definition om :=
delta (fun om' => agree finpow om').

Lemma Infinity' :
agree finpow om.
Proof.
unfold om. destruct MI as [om' H].
apply (delta_spec H). apply agree_unique.
Qed.

Lemma Infinity :
forall x, x el om <-> exists n, x = powit n.
Proof.
intros x. rewrite (Infinity' x).
split; intros [n H]; exists n; now apply ZFExt.
Qed.

Definition OM :=
union om.

(* OM is a limit stage *)

Lemma OM_powit n :
powit n el OM.
Proof.
apply Union. exists (powit (S n)). split.
- apply Infinity. now exists (S n).
- now apply Power.
Qed.

Lemma OM_ex_powit x :
x el OM -> exists n, x el powit n.
Proof.
intros [y[Y1 Y2]] % Union.
apply Infinity in Y1 as [n ->].
now exists n.
Qed.

Lemma OM_eset :
0 el OM.
Proof.
assert (H : eset = powit 0) by trivial.
rewrite H. apply OM_powit.
Qed.

Lemma powit_stage n :
Stage (powit n).
Proof.
induction n.
- apply Stage_eset.
- now constructor.
Qed.

Lemma OM_stage :
Stage OM.
Proof.
constructor. intros y H.
apply Infinity in H as [n ->].
apply powit_stage.
Qed.

Lemma OM_limit :
OM <<= union OM.
Proof.
intros x [X[H1 H2]] % Union.
apply Infinity in H1 as [n ->].
apply Union. exists (powit n). split; trivial.
apply OM_powit.
Qed.

Lemma limit_OM :
limit OM.
Proof.
split; auto using OM_stage, OM_limit.
Qed.

## Hereditarily finite sets (HF)

Inductive Fin : M -> Prop :=
| FinE : Fin 0
| FinA x y : Fin y -> Fin (adj x y).

Inductive HF x : Prop :=
HFI : (forall y, y el x -> HF y) -> Fin x -> HF x.

Fact HF_Fin x :
HF x -> Fin x.
Proof.
intros [_ H]. assumption.
Qed.

x el y -> y = adj x (sep (fun a => a <> x) y).
Proof.
intros H. apply Ext; intros z Z.
- destruct (classic (z = x)) as [-> | N]; apply adj_el; auto.
left. apply sep_el. now split.
- apply adj_el in Z as [Z| ->]; trivial.
now apply sep_el in Z as [Z1 Z2].
Qed.

Lemma Fin_subset x y :
Fin x -> y <<= x -> Fin y.
Proof.
intros H. revert y. induction H as [|x z H IH].
- intros y -> % sub_eset. constructor.
- intros y HY. destruct (classic (x el y)) as [X|X].
+ rewrite -> (adj_sep X). constructor.
apply IH. intros a [A1 A2] % sep_el.
specialize (HY a A1). apply adj_el in HY as [A|A]; tauto.
+ apply IH. intros a A. specialize (HY a A).
apply adj_el in HY as [I|I]; subst; tauto.
Qed.

(* Fin and HF are closed under replacement *)

Lemma rep_eset R :
functional R -> rep R 0 = 0.
Proof.
intros H. apply sub_eset.
intros x [y[Y1 Y2]] % Rep; trivial.
Qed.

Lemma rep_sing R x y :
functional R -> R x y -> y = union (rep R (sing x)).
Proof.
intros FR H. apply Ext; intros z Z.
- apply Union. exists y. split; trivial.
apply Rep; trivial. exists x. split; trivial.
apply Pair. now left.
- apply Union in Z as [b[B1 B2]].
apply Rep in B1 as [a[A1 A2]]; trivial.
apply pair_el in A1 as [A1|A1]; subst a; now rewrite (FR x y b H A2).
Qed.

Lemma rep_adj R x y :
functional R -> rep R (adj x y) <<= adj (union (rep R (sing x))) (rep R y).
Proof.
intros FR b [a[A1 A2]] % Rep; trivial.
apply adj_el in A1 as [A1|A1].
- apply adj_el. left. apply Rep; trivial. now exists a.
- subst x. apply adj_el. right. now apply rep_sing.
Qed.

Lemma Fin_rep R x :
functional R -> Fin x -> Fin (rep R x).
Proof.
intros FR H. induction H as [|x y H IH].
- rewrite rep_eset; trivial. constructor.
- apply Fin_subset with (x:=adj (union (rep R (sing x))) (rep R y)).
+ now constructor.
Qed.

Lemma Fin_frep F x :
Fin x -> Fin (frep F x).
Proof.
intros H. rewrite rep_frep.
apply Fin_rep; trivial. congruence.
Qed.

Lemma HF_rep :
closed_rep HF.
Proof.
intros R x FR H RR. split.
- intros y [z[Z1 Z2]] % Rep; trivial.
apply RR, Rep; trivial. now exists z.
- apply Fin_rep; trivial. apply H.
Qed.

(* Fin and HF are closed under power *)

Lemma binunion_eset x :
binunion 0 x = x.
Proof.
apply Ext; intros y Y.
- apply binunion_el in Y as [Y|Y]; auto.
- apply binunion_el. now right.
Qed.

Lemma binunion_adj x y z :
Proof.
apply Ext; intros a A.
- apply adj_el. apply binunion_el in A as [A|A].
+ apply adj_el in A as [A| ->]; auto.
left. apply binunion_el. now left.
+ left. apply binunion_el. now right.
- apply binunion_el. apply adj_el in A as [A | ->].
+ apply binunion_el in A as [A|A]; auto.
+ left. apply adj_el. now right.
Qed.

Lemma Fin_binunion x y :
Fin x -> Fin y -> Fin (binunion x y).
Proof.
intros H. revert y. induction H as [|x z H IH].
- intros y FY. now rewrite binunion_eset.
- intros y FY. rewrite binunion_adj.
constructor. now apply IH.
Qed.

power (adj x y) = binunion (power y) (frep (adj x) (power y)).
Proof.
apply Ext; intros z Z.
- apply Power in Z. destruct (classic (x el z)) as [H|H].
+ apply binunion_el. right. apply frep_el.
exists (sep (fun a => a <> x) z). split; try now apply adj_sep.
apply Power. intros a [A1 A2] % sep_el.
specialize (Z a A1). apply adj_el in Z as [Z|Z]; tauto.
+ apply binunion_el. left. apply Power.
intros a A. specialize (Z a A).
apply adj_el in Z as [Z|Z]; trivial.
- apply Power. intros a A. apply binunion_el in Z as [Z|Z].
+ apply Power in Z. apply adj_el. left. now apply Z.
+ apply frep_el in Z as [y'[Y1 % Power Y2]]. subst.
Qed.

Lemma pow_eset :
power 0 = adj 0 0.
Proof.
apply Ext; intros x X.
- apply Power in X. apply sub_eset in X as <-.
- apply adj_el in X as [X| ->].
+ apply Power. auto.
Qed.

Lemma power_Fin :
closed_power Fin.
Proof.
intros x. induction 1 as [|x y H IH].
- rewrite pow_eset. repeat constructor.
- rewrite adj_power. apply Fin_binunion; trivial.
rewrite rep_frep. apply Fin_rep; trivial. congruence.
Qed.

Lemma HF_power :
closed_power HF.
Proof.
intros x [H1 H2]. split.
- intros y Y % Power. constructor; auto.
now apply (Fin_subset H2).
- now apply power_Fin.
Qed.

(* HF is ZF-closed *)

Lemma HF_ctrans :
ctrans HF.
Proof.
intros x y [H]. apply H.
Qed.

Lemma HF_eset :
HF 0.
Proof.
constructor; auto using Fin.
Qed.

union (adj x y) = binunion x (union y).
Proof.
apply Ext; intros z H.
- apply binunion_el.
apply Union in H as [z'[H1 H2]].
apply adj_el in H1 as [H1| ->]; auto.
right. apply Union. now exists z'.
- apply Union.
apply binunion_el in H as [H|H].
+ exists x. split; trivial. apply adj_el; auto.
+ apply Union in H as [z'[H1 H2]].
exists z'. split; trivial. apply adj_el; auto.
Qed.

Lemma HF_union :
closed_union HF.
Proof.
intros x [H1 H2]. constructor.
- intros z [y[Y1 Y2]] % Union.
apply H1 in Y1 as [Y1]. now apply Y1.
- induction H2.
+ rewrite union_eset. constructor.
* apply HF_Fin, H1, adj_el. now right.
* apply IHFin. intros z H.
Qed.

Fact HF_ZF :
closed_ZF HF.
Proof.
apply ZF_rep.
split; try apply HF_ctrans.
split; try apply HF_eset.
split; try apply HF_union.
split; try apply HF_power.
apply HF_rep.
Qed.

## The class HF is realized by Omega

Lemma eset_HF :
HF 0.
Proof.
split; auto using FinE.
Qed.

Lemma powit_HF n :
HF (powit n).
Proof.
induction n as [| n IH].
- apply eset_HF.
- now apply HF_power.
Qed.

Lemma powit_Fin n :
Fin (powit n).
Proof.
induction n.
- constructor.
- now apply power_Fin.
Qed.

Lemma OM_Fin x :
x el OM -> Fin x.
Proof.
intros [n H] % OM_ex_powit.
destruct n.
- apply (Fin_subset (powit_Fin n)).
now apply Power.
Qed.

Lemma OM_rho_el x :
x el OM -> rho x el OM.
Proof.
intros [X[X1 X2]] % Union.
apply Infinity in X1 as [n ->].
apply (Stage_swelled OM_stage (x:=powit n)).
- apply OM_powit.
- destruct (@Stage_lin _ _ (rho x) (powit n)) as [H|H].
+ apply rho_rank.
+ apply powit_stage.
+ assumption.
+ exfalso. apply H in X2. now apply rho_rank in X2.
Qed.

Definition chain x :=
forall y z, y el x -> z el x -> y <<= z \/ z <<= y.

Lemma chain_sub x y :
x <<= y -> chain y -> chain x.
Proof.
intros H1 H2 a b A B. apply H2; auto.
Qed.

Proof.
intros z Z. apply adj_el. now left.
Qed.

Lemma Fin_chain_max x :
Fin x -> inhab x -> chain x -> union x el x.
Proof.
induction 1 as [|x y H IH]; intros H1 H2.
- destruct (classic (inhab y)) as [H3|H3].
+ specialize (IH H3 (chain_sub (@adj_sub x y) H2)).
assert (XA : x el adj x y) by (apply adj_el; auto).
assert (YA : (union y) el adj x y) by (apply adj_el; auto).
destruct (H2 x (union y) XA YA) as [XY|YX]; apply adj_el.
* left. cutrewrite (union (adj x y) = union y); trivial. apply Ext.
-- apply union_sub. intros a [A| ->] % adj_el; trivial.
now apply union_el_sub.
-- apply union_el_sub. apply adj_el. now left.
* right. apply Ext.
-- apply union_sub. intros a [A| ->] % adj_el; trivial.
intros b B. apply YX. apply Union. now exists a.
-- apply union_el_sub. apply adj_el. now right.
+ apply adj_el. right. apply Ext.
* apply union_sub. intros a [A| ->] % adj_el; trivial.
* apply union_el_sub. apply adj_el. now right.
Qed.

Lemma HF_rho x :
HF x -> rho x el OM.
Proof.
induction 1 as [x _ IH H].
pose (X := (frep power (frep rho x))).
destruct (classic (inhab x)) as [[z Z]| -> % inhab_not].
- assert (H3 : chain X).
+ intros a b [a'[A ->]] % frep_el [b'[B ->]] % frep_el.
apply frep_el in A as [a[A ->]]. apply frep_el in B as [b[B ->]].
apply Stage_lin; constructor; apply rho_rank.
+ assert (IR : inhab X).
{ exists (power (rho z)). apply frep_el. exists (rho z).
split; trivial. apply frep_el. now exists z. }
apply Fin_chain_max in H3; try (repeat apply Fin_frep; trivial).
apply frep_el in H3 as [Y[[y [Y1 Y2]] % frep_el Y3]]; subst.
rewrite rho_rho'. unfold rho'. fold X. rewrite Y3.
apply (limit_power limit_OM). now apply IH.
- cutrewrite (rho 0 = 0); try apply OM_eset.
apply (rank_fun (rho_rank 0)).
repeat split; auto using Stage_eset, Eset.
Qed.

Lemma HF_OM :
agree HF OM.
Proof.
intros x. split; intros H.
- apply Union in H as [y [[n ->] % Infinity Y2]].
destruct (powit_HF n) as [H _]. now apply H.
- apply (Stage_swelled OM_stage (x:=rho x)).
+ now apply HF_rho.
+ apply rho_rank.
Qed.

## Inf implies that Omega is a universe

(* OM is closed under replacement and hence a universe *)

Lemma OM_repclosed :
closed_rep (cl OM).
Proof.
intros R x FR X XR. apply HF_OM.
apply HF_rep; trivial.
- now apply HF_OM.
- intros z [y[H1 H2]] % Rep; trivial.
apply HF_OM, XR, Rep; trivial. now exists y.
Qed.

Theorem OM_universe :
universe OM.
Proof.
apply universe_limit. repeat split.
- apply OM_stage.
- apply OM_limit.
- exists eset. now apply OM_eset.
- apply OM_repclosed.
Qed.

Theorem OM_ZF1 :
ZFge 1 M.
Proof.
split; trivial.
exists (power OM), OM. simpl.
split; auto using power_eager.
split; auto using OM_universe.
Qed.

(* OM is in fact the least limit and universe *)

Lemma om_limit x :
limit x -> inhab x -> om <<= x.
Proof.
intros H1 H2 y Y.
apply Infinity in Y as [n ->].
induction n as [|n IH].
- apply Stage_inhab; firstorder.
- now apply limit_power.
Qed.

Lemma om_infinite :
~ Fin om.
Proof.
intros H. apply Fin_chain_max in H.
- apply Infinity in H as [n H].
apply (WF_no_loop (x:=powit n)).
rewrite <- H at 2. apply OM_powit.
- exists 0. apply Infinity. now exists O.
- intros x y [n ->] % Infinity [n' ->] % Infinity.
apply Stage_lin; apply powit_stage.
Qed.

Lemma limit_infinite x :
limit x -> inhab x -> ~ Fin x.
Proof.
intros H1 H2 H3. apply om_infinite.
now apply (Fin_subset H3), om_limit.
Qed.

Fact OM_least_limit x :
limit x -> inhab x -> OM <<= x.
Proof.
intros H1 H2. assert (S1 : Stage x) by apply H1.
assert (S2 : Stage OM) by apply universe_stage, OM_universe.
destruct (Stage_lin_el S2 S1) as [I|I]; trivial.
exfalso. apply (limit_infinite H1 H2). now apply OM_Fin.
Qed.

Corollary OM_least u :
universe u -> OM <<= u.
Proof.
intros H % universe_limit.
apply OM_least_limit; apply H.
Qed.

End Infinity.

## Models of ZF>=1 satisfy Infinity

Section Inf.

Context { M : ZFStruct }.
Context { MZF1 : ZFge 1 M }.

Instance MZF : ZF M :=
proj1 MZF1.

Fact MI :
Inf M.
Proof.
destruct MZF1 as [MZF[X[U[_[HU _]]]]].
pose (om := sep finpow U).
exists om. intros x. split; intros H.
- now apply sep_el in H.
- destruct H as [n ->]. apply sep_el.
split; try now exists n.
induction n; simpl; now apply HU.
Qed.

End Inf.