Set Implicit Arguments.

Require Setoid.

Parameter XM : ∀ P, P ∨ ¬ P.

Lemma DN P :
  ¬ ¬ P ↔ P.

Notation "'set' X" := (X → Prop) (at level 70).
Notation "p <<= q" := (∀ x, p x → q x) (at level 70).
Definition inhab X (p : set X) := ∃ x, p x.

Structure pot :=
  { pot_X :> Type;
    pot_le : pot_X → pot_X → Prop;
    pot_refl : ∀ x, pot_le x x;
    pot_anti : ∀ x y, pot_le x y → pot_le y x → x = y;
    pot_trans : ∀ x y z, pot_le x y → pot_le y z → pot_le x z }.

Notation "x <= y" := (pot_le x y).
Notation "x < y" := (x ≤ y ∧ x ≠ y).

Section POT.
  Variable X : pot.

  Implicit Types x y z u : X.
  Implicit Types p q : set X.

  Definition sup p x := ∀ z, x ≤ z ↔ ∀ y, p y → y ≤ z.
  Definition min p x := p x ∧ ¬ ∃ y, p y ∧ y < x.
  Definition chain p := ∀ x y, p x → p y → x ≤ y ∨ y ≤ x.
  Definition wf p := ∀ q, q <<= p → inhab q → inhab (min q).
  Definition well_order := chain (fun x ⇒ True) ∧ wf (fun x ⇒ True).

  Fact le_lt x y :
    x ≤ y → x = y ∨ x < y.

  Fact lt_neq x :
    ¬ x < x.

  Fact lt_le x y :
    x < y → x ≤ y.

  Fact lt_le' x y z :
    x < y → y ≤ z → x < z.

  Fact lt_not_le x y :
    x < y → ¬ y ≤ x.

  Fact chain_not_le p x y :
    chain p → p x → p y → ¬ x ≤ y → y < x.

  Fact sup_le x p u :
    p x → sup p u → x ≤ u.

  Fact sup_le' x y p u :
    x ≤ y → p y → sup p u → x ≤ u.

  Fact sup_ex p u x :
    sup p u → x < u → ∃ y, p y ∧ ¬ y ≤ x.

  Fact sup_ex' x u p :
    sup p u → ¬ u ≤ x → ∃ y, p y ∧ ¬ y ≤ x.

  Inductive ind p : set X :=
  | indI x : (∀ y, p y → y < x → ind p y) → ind p x.

  Lemma ind_iff p x :
    ind p x ↔ ∀ y, p y → y < x → ind p y .

  Fact ind_wf p :
    p <<= ind p → wf p.

  Fact wf_ind p :
    wf p → p <<= ind p.

End POT.

Section Bourbaki.
  Variable X : pot.
  Variable a : X.
  Variable f : X → X.
  Variable f_inc : ∀ x, x ≤ f x.

  Implicit Types x y z u : X.
  Implicit Types p q : set X.

  Inductive T : set X :=
  | Ta : T a
  | Tf x : T x → T (f x)
  | Tsup p u : p <<= T → inhab p → sup p u → T u.

  Fact f_inc' x y :
    x ≤ y → x ≤ f y.

  Fact f_inc'' x y :
    f x ≤ y → x ≤ y.

  Fact T_a_least x :
    T x → a ≤ x.

  Definition R x := T x ∧ ∀ y, T y → y < x → f y ≤ x.

  Lemma BL1 x y :
    T x → R y → x ≤ y ∨ f y ≤ x.

  Lemma BL2 :
    T <<= R.

  Theorem Bourbaki x y :
    T x → T y → x ≤ y ∨ f y ≤ x.

  Corollary T_chain :
    chain T.

  Corollary T_f_monotone x y :
    T x → T y → x ≤ y → f x ≤ f y.

  Corollary T_f_succ x y :
    T x → T y → x < f y → x ≤ y.

  Corollary T_sup u :
    sup T u → T u.

  Corollary T_sup_FP u :
    sup T u ↔ f u = u ∧ T u.

  Lemma T_wf :
    wf T.

  Theorem Bourbaki_Witt :
    (∀ p, wf p → chain p → ∃ u, sup p u) → ∃ u, f u = u ∧ a ≤ u.

End Bourbaki.

Section SetStuff.
  Variable X : Type.

  Implicit Types x : X.
  Implicit Types p q r : set X.
  Implicit Types F : set (set X).

  Definition sing x : set X := fun z ⇒ z = x.
  Definition comp p : set X := fun z ⇒ ¬ p z.
  Definition union F : set X := fun x ⇒ ∃ p, F p ∧ p x.
  Definition unique p : Prop := ∀ x y, p x → p y → x = y.

  Fact sing_eq x y :
    sing x y → x = y.

  Fact sing_eq' x y :
    sing x = sing y → x = y.

  Fact union_incl p F :
    F p → p <<= union F.

  Fact incl_refl p :
    p <<= p.

  Fact incl_trans p q r :
    p <<= q → q <<= r → p <<= r.

End SetStuff.

Structure ect :=
  { ect_X :> Type;
    ect_ext : ∀ p q : set ect_X, p <<= q → q <<= p → p = q;
    gamma : set ect_X → set ect_X;
    gamma_unique : ∀ p, unique (gamma p);
    gamma_incl : ∀ p, gamma p <<= p;
    gamma_inhab : ∀ p, inhab p → inhab (gamma p) }.

Section Zermelo.
  Variable X : ect.

  Definition xset : pot := @Build_pot (set X) (fun p q ⇒ p <<= q)
                           (@incl_refl X) (@ect_ext X) (@incl_trans X).

  Implicit Types x y z u : X.
  Implicit Types p q r : xset.
  Implicit Types F : set xset.

  Fact sup_union F :
    sup F (union F).

  Fact unique_sing p x :
    unique p → p x → p = sing x.

  Definition eta p : xset := gamma (comp p).
  Definition a : xset := fun x ⇒ False.
  Definition f p : xset := fun x ⇒ p x ∨ eta p x.

  Fact f_inc p :
    p ≤ f p.

  Fact T_union F :
    F <<= T a f → T a f (union F).

  Definition seg x : xset := union (fun p ⇒ T a f p ∧ ¬ p x).

  Fact seg_T x :
    T a f (seg x).

  Fact seg_open x :
    ¬ seg x x.

  Fact seg_eta x :
    eta (seg x) x.

  Fact eta_seg x :
    eta (seg x) = sing x.

  Fact seg_injective x y :
    seg x = seg y → x = y.

  Definition le x y := seg x <<= seg y.
  Lemma le_refl x : le x x.
  Lemma le_anti x y : le x y → le y x → x = y.
  Lemma le_trans x y z : le x y → le y z → le x z.

  Definition poX : pot := @Build_pot X le le_refl le_anti le_trans.

  Theorem Zermelo :
    well_order poX.

End Zermelo.

Check Zermelo.
Print Assumptions Zermelo.