Library ZFcard
Require Import ZF.
Definition le_card (x y:set) : Prop :=
exists2 R : set -> set -> Prop,
Proper (eq_set ==> eq_set ==> iff) R &
(∀ x', x' ∈ x -> exists2 y', y' ∈ y & R x' y') /\
(∀ x1 y1 x2 y2, x1 ∈ x -> x2 ∈ x -> y1 ∈ y -> y2 ∈ y ->
R x1 y1 -> R x2 y2 -> y1 == y2 -> x1 == x2).
Instance le_card_morph : Proper (eq_set ==> eq_set ==> iff) le_card.
split; destruct 1.
destruct H2.
exists x1; trivial; split; intros.
rewrite <- H in H4.
elim H2 with x'; intros; trivial.
exists x2; trivial.
rewrite <- H0; trivial.
rewrite <- H in H4,H5|-.
rewrite <- H0 in H6,H7|-.
eauto.
destruct H2.
exists x1; trivial; split; intros.
rewrite H in H4.
elim H2 with x'; intros; trivial.
exists x2; trivial.
rewrite H0; trivial.
rewrite H in H4,H5|-.
rewrite H0 in H6,H7|-.
eauto.
Qed.
Instance le_card_refl : Reflexive le_card.
exists (fun x' y' => x' == y').
do 3 red; intros.
rewrite H; rewrite H0; reflexivity.
split; intros.
exists x'; trivial; reflexivity.
rewrite H3; rewrite H4; trivial.
Qed.
Instance le_card_trans : Transitive le_card.
red.
destruct 1 as (R,Rm,(incl,inj));
destruct 1 as (R',R'm,(incl',inj')).
exists (fun x' z' => exists2 y', y' ∈ y & R x' y' /\ R' y' z'); [|split;intros].
do 3 red; intros.
apply ex2_morph.
red; reflexivity.
red; intros.
rewrite H; rewrite H0; reflexivity.
elim incl with x'; trivial; intros.
elim incl' with x0; trivial; intros.
exists x1; trivial.
exists x0; auto.
destruct H3 as (y1',in1,(r1,r1'));
destruct H4 as (y2',in2,(r2,r2')).
eauto.
Qed.
Definition lt_card x y :=
~ le_card y x.
Lemma incl_le_card : ∀ x y, x ⊆ y -> le_card x y.
intros.
exists (fun x y => x == y); [|split;intros].
do 3 red; intros.
rewrite H0; rewrite H1; reflexivity.
exists x'; auto.
reflexivity.
rewrite H4; rewrite H5; trivial.
Qed.
Lemma cantor_le : ∀ x, lt_card x (power x).
red; red; intros.
destruct H as (R,Rm,(incl,Rfun)).
pose (D := subset x (fun x' => ∀ x'' z, z ∈ power x ->
x'' == x' -> R z x'' -> ~ x'' ∈ z)).
assert (D ∈ power x).
apply power_intro; intros.
unfold D in H.
apply subset_elim1 with (1:=H).
elim incl with D; trivial; intros d in_d rel_d.
assert (~ d ∈ D).
red; intros.
unfold D in H0.
elim subset_elim2 with (1:=H0); intros.
apply H2 with d D; trivial.
apply H0.
unfold D; apply subset_intro; trivial.
intros.
rewrite H2.
assert (z == D).
apply Rfun with x'' d; auto.
rewrite H2; trivial.
rewrite H4; trivial.
Qed.
Lemma discr_power : ∀ x, ~ x == power x.
red; intros.
apply cantor_le with x.
rewrite <- H.
reflexivity.
Qed.
Definition equi_card (x y:set) : Prop :=
exists2 R : set -> set -> Prop,
Proper (eq_set ==> eq_set ==> iff) R &
(∀ x', x' ∈ x -> exists2 y', y' ∈ y & R x' y') /\
(∀ y', y' ∈ y -> exists2 x', x' ∈ x & R x' y') /\
(∀ x1 y1 x2 y2, x1 ∈ x -> x2 ∈ x -> y1 ∈ y -> y2 ∈ y ->
R x1 y1 -> R x2 y2 -> (x1 == x2 <-> y1 == y2)).
Instance equi_card_morph : Proper (eq_set ==> eq_set ==> iff) equi_card.
apply morph_impl_iff2; auto with *.
unfold equi_card; do 4 red; intros.
destruct H1 as (R,Rm,(incl1,(incl2,bij))).
exists R; [trivial|split;[|split]]; intros.
rewrite <- H in H1.
destruct (incl1 x'); trivial.
rewrite H0 in H2.
exists x1; trivial.
rewrite <- H0 in H1.
destruct (incl2 y'); trivial.
rewrite H in H2.
exists x1; trivial.
rewrite <- H in H1,H2.
rewrite <- H0 in H3,H4.
auto.
Qed.
Instance equi_card_refl : Reflexive equi_card.
exists (fun x' y' => x' == y').
do 3 red; intros.
rewrite H; rewrite H0; reflexivity.
split; [|split]; intros.
exists x'; trivial; reflexivity.
exists y'; trivial; reflexivity.
rewrite H3; rewrite H4; reflexivity.
Qed.
Instance equi_card_sym : Symmetric equi_card.
red; destruct 1 as (R,Rm,(incl1,(incl2,bij))).
exists (fun x' y' => R y' x'); intros; auto.
do 3 red; intros; apply Rm; trivial.
split;[|split]; trivial.
symmetry; auto.
Qed.
Instance equi_card_trans : Transitive equi_card.
red.
destruct 1 as (R,Rm,(incl1,(incl2,bij)));
destruct 1 as (R',R'm,(incl1',(incl2',bij'))).
exists (fun x' z' => exists2 y', y' ∈ y & R x' y' /\ R' y' z').
do 3 red; intros.
apply ex2_morph.
red; reflexivity.
red; intros.
rewrite H; rewrite H0; reflexivity.
split; [|split]; intros.
elim incl1 with x'; trivial; intros.
elim incl1' with x0; trivial; intros.
exists x1; trivial.
exists x0; auto.
elim incl2' with y'; trivial; intros.
elim incl2 with x0; trivial; intros.
exists x1; trivial.
exists x0; auto.
destruct H3 as (y1',in1,(r1,r1'));
destruct H4 as (y2',in2,(r2,r2')).
transitivity (y1' == y2'); auto.
Qed.
Lemma equi_card_le : ∀ x y, equi_card x y -> le_card x y.
destruct 1 as (R,Rm,(incl1,(incl2,bij))).
exists R; [trivial|split;intros;auto].
refine (proj2 (bij _ _ _ _ _ _ _ _ H3 H4) H5); trivial.
Qed.
Lemma cantor : ∀ x, ~ equi_card x (power x).
red; intros; apply (cantor_le x);
apply equi_card_le; apply equi_card_sym; trivial.
Qed.
Require Import ZFnats ZFord.
Definition isCard x :=
isOrd x /\ (∀ y, lt y x -> lt_card y x).
Definition regular_card o :=
∀ x F,
lt_card x o ->
ext_fun x F ->
(∀ y, y ∈ x -> lt_card (F y) o) ->
lt_card (sup x F) o.
Definition regular o := ∀ x F,
lt_card x o ->
ext_fun x F ->
(∀ y, y ∈ x -> lt (F y) o) ->
lt (sup x F) o.
Section RegularRelational.
Import ZFrepl.
Definition regular_rel o := ∀ x R,
lt_card x o ->
repl_rel x R ->
(∀ y z, y ∈ x -> R y z -> lt z o) ->
lt (union (repl x R)) o.
Lemma regular_weaker : ∀ o,
regular_rel o -> regular o.
red; intros.
change (sup x F) with (union (repl x (fun x y => y == F x))).
apply H; intros; auto.
apply repl_rel_fun; trivial.
rewrite H4; auto.
Qed.
End RegularRelational.
Definition regular' o := ∀ x F,
lt x o ->
ext_fun x F ->
(∀ y, y ∈ x -> lt (F y) o) ->
lt (sup x F) o.
Definition stronglyInaccessibleCard o :=
limitOrd o /\ regular o.
Definition lt_card2 a b :=
∀ R:set->set->Prop,
(∀ x x' y y', x ∈ a -> y ∈ b -> y' ∈ b ->
R x y -> R x' y' -> x==x' -> y==y') ->
exists2 y, y ∈ b & ∀ x, x ∈ a -> ~ R x y.
Lemma lt_card_weaker : ∀ a b,
lt_card2 a b -> lt_card a b.
red; red; intros.
destruct H0 as (R,?,(?,?)).
destruct (H (fun x y => R y x)).
intros.
apply H2 with x x'; trivial.
rewrite <- H8; trivial.
destruct H1 with x; trivial.
eapply H4; eauto.
Qed.
Require Import ZFrelations.
Require Import Relations.
Section Hartog.
Variable X:set.
Set Implciit Arguments.
Record REL A0 : Type := {
Rel :> A0 -> A0 -> Prop;
dom : A0 -> Prop;
wfrel : well_founded Rel
}.
Definition morphism A0 (R S : REL A0) (f : A0 -> A0) :=
(∀ x y, dom _ R x -> dom _ R y -> R x y -> S (f x) (f y)) /\
(∀ x, dom _ R x -> dom _ S (f x)).
Record emb A0 (R1 R2 : REL A0) : Prop := {
f : A0 -> A0;
fmorph : morphism _ R1 R2 f;
maj : A0;
majd : dom _ R2 maj;
majf : ∀ z, dom _ R1 z -> R2 (f z) maj}.
Parameter WF_emb : ∀ A0, well_founded (emb A0).
Definition emb0 A0 i0 (x y:A0) :=
exists2 R1, x = i0 R1 & exists2 R2, y = i0 R2 & emb A0 R1 R2.
Parameter WF_emb0 : ∀ A0 i0, well_founded (emb0 A0 i0).
Definition Emb A0 i0 (P:A0->Prop) : REL A0 :=
Build_REL _ (emb0 A0 i0) P (WF_emb0 A0 i0).
Parameter Burali_Forti
: ∀ (A0 : Type) (i0 : REL A0 -> A0),
(∀ R1 R2 : REL A0,
i0 R1 = i0 R2 -> exists f : A0 -> A0, morphism A0 R1 R2 f) -> False.
Definition order_type_assign_rel R a o :=
∀ P,
Proper (eq_set ==> eq_set ==> iff) P ->
(∀ x f,
let x' := subset X (fun y => rel_app R y x) in
ext_fun x' f ->
(∀ y, rel_app R y x -> P y (f y)) ->
P x (osup x' (fun y => osucc (f y)))) ->
P a o.
Instance order_type_assign_ext :
Proper (eq_set==>eq_set==>eq_set==>iff) order_type_assign_rel.
Admitted.
Lemma order_type_assign_rel_inv : ∀ r a x,
order_type_assign_rel r a x ->
exists2 f,
∀ b, rel_app r b a -> order_type_assign_rel r b (f b) &
let a' := subset X (fun b => rel_app r b a) in
ext_fun a' f /\ x == osup a' (fun y => osucc (f y)).
intros.
apply H; intros.
apply morph_impl_iff2; auto with *.
do 4 red; intros.
destruct H2.
exists x2; intros.
rewrite <- H0 in H4; auto.
destruct H3; split.
do 2 red; intros; apply H3; auto.
apply subset_intro.
apply subset_elim1 in H5; trivial.
apply subset_elim2 in H5; destruct H5.
rewrite H5; rewrite H0; trivial.
rewrite<- H1; rewrite H4.
apply osup_morph; auto.
apply subset_morph; auto with *.
red; intros.
rewrite H0; auto with *.
red; intros.
apply osucc_morph.
apply H3; trivial.
exists f; intros.
2:split; [trivial|reflexivity].
red; intros.
destruct H1 with b; trivial.
destruct H6.
rewrite H7.
apply H4; intros; trivial.
apply H5; trivial.
Qed.
Require Import ZFrepl.
Require Import Relations.
Definition isWellOrder R :=
∀ x, Acc (rel_app R) x.
Instance isWO_m : Proper (eq_set ==> iff) isWellOrder.
Admitted.
Lemma order_type_assign_uchoice : ∀ R a,
isWellOrder R ->
uchoice_pred (order_type_assign_rel R a).
intros.
elim (H a); intros.
split;[|split]; intros.
rewrite <- H2; trivial.
exists (osup (subset X (fun z => rel_app R z x))
(fun z => osucc (uchoice (order_type_assign_rel R z)))).
red; intros.
apply H3; intros.
do 2 red; intros.
apply uchoice_morph_raw.
red; intros.
rewrite H5; rewrite H6; reflexivity.
apply (uchoice_def _ (H1 _ H4)); trivial.
clear a.
revert x' H1 H3.
apply H2; intros.
apply morph_impl_iff2; auto with *.
do 4 red; intros.
rewrite <- H3; apply H4; intros.
apply H5.
rewrite <- H1; trivial.
rewrite H1; trivial.
destruct order_type_assign_rel_inv with (1:=H5) as (f',?,(_,?)).
rewrite H7.
apply osup_morph.
apply subset_morph; auto with *.
red; intros.
apply osucc_morph.
apply H3; intros; auto.
apply subset_elim2 in H8; destruct H8.
rewrite H8; trivial.
apply H4.
admit. rewrite H9.
apply H6.
rewrite <- H9.
apply subset_elim2 in H8; destruct H8.
rewrite H8; trivial.
Qed.
Lemma order_type_assign_rel_inv' : ∀ r a,
isWellOrder r ->
uchoice (order_type_assign_rel r a) ==
osup (subset X (fun b => rel_app r b a))
(fun b => osucc (uchoice (order_type_assign_rel r b))).
intros.
generalize (uchoice_def _ (order_type_assign_uchoice _ a H)); intro.
apply order_type_assign_rel_inv in H0; destruct H0.
destruct H1.
rewrite H2.
apply osup_morph; auto with *.
red; intros.
apply osucc_morph.
rewrite (H1 x0 x'); trivial.
rewrite H4 in H3; clear x0 H4.
apply subset_elim2 in H3; destruct H3.
rewrite <- H3 in H4 ;clear x0 H3.
apply H0 in H4.
apply uchoice_ext; trivial.
apply order_type_assign_uchoice; trivial.
Qed.
Lemma order_type_assign_ord : ∀ R a o,
order_type_assign_rel R a o ->
isOrd o.
intros.
red in H.
pattern a, o; apply H.
do 3 red; intros.
rewrite H1; reflexivity.
intros.
apply isOrd_osup; intros.
do 2 red; intros.
apply osucc_morph; apply H0; trivial.
apply subset_elim2 in H2; destruct H2.
rewrite <- H2 in H3; auto.
Qed.
Definition order_type R :=
osup X (fun a => osucc (uchoice (order_type_assign_rel R a))).
Lemma ot_ext : ∀ x x',
x == x' ->
eq_fun X
(fun a => osucc (uchoice (order_type_assign_rel x a)))
(fun a => osucc (uchoice (order_type_assign_rel x' a))).
red; intros.
apply osucc_morph.
apply uchoice_morph_raw.
apply order_type_assign_ext; auto with *.
Qed.
Instance order_type_ext : morph1 order_type.
unfold order_type.
do 2 red; intros.
apply osup_morph; auto with *.
apply ot_ext; trivial.
Qed.
Definition wo := subset (rel X X) isWellOrder.
Lemma wo_def2 : ∀ r, r ∈ wo -> isWellOrder r.
intros.
apply subset_elim2 in H; destruct H.
rewrite H; trivial.
Qed.
Hint Resolve wo_def2.
Definition hartog_succ :=
osup wo order_type.
Lemma isOrd_hartog : isOrd hartog_succ.
unfold hartog_succ.
apply isOrd_osup.
do 2 red; intros.
rewrite H0; reflexivity.
intros.
unfold order_type.
apply isOrd_osup.
red; apply ot_ext; reflexivity.
intros.
apply wo_def2 in H.
generalize (uchoice_def _ (order_type_assign_uchoice _ x0 H)).
intros.
apply isOrd_succ.
apply order_type_assign_ord with (1:=H1).
Qed.
Lemma hartog_assign_surj : ∀ x,
x ∈ hartog_succ ->
exists2 R, R ∈ wo &
∀ y, y ∈ x -> exists2 b, b ∈ X & order_type_assign_rel R b y.
Admitted.
Section BuraliForti.
Variable I : set -> set -> Prop.
Hypothesis ty_I : ∀ x,
x ∈ hartog_succ -> exists2 y, y ∈ X & I x y.
Hypothesis inj_I : ∀ x1 y1 x2 y2,
x1 ∈ hartog_succ ->
x2 ∈ hartog_succ ->
y1 ∈ X ->
y2 ∈ X ->
I x1 y1 ->
I x2 y2 ->
y1 == y2 -> x1 == x2.
Definition OT R :=
order_type (inject_rel (fun x y => dom _ R x /\ dom _ R y /\ R x y) X X).
Parameter OT_inj : ∀ (R1 R2:REL set),
(∀ x, dom _ R1 x -> x ∈ X) ->
(∀ x, dom _ R2 x -> x ∈ X) ->
OT R1 ⊆ OT R2 -> exists f, morphism _ R1 R2 f.
Lemma burali_forti : False.
generalize ty_I inj_I.
admit.
Qed.
End BuraliForti.
End Hartog.
Definition le_card (x y:set) : Prop :=
exists2 R : set -> set -> Prop,
Proper (eq_set ==> eq_set ==> iff) R &
(∀ x', x' ∈ x -> exists2 y', y' ∈ y & R x' y') /\
(∀ x1 y1 x2 y2, x1 ∈ x -> x2 ∈ x -> y1 ∈ y -> y2 ∈ y ->
R x1 y1 -> R x2 y2 -> y1 == y2 -> x1 == x2).
Instance le_card_morph : Proper (eq_set ==> eq_set ==> iff) le_card.
split; destruct 1.
destruct H2.
exists x1; trivial; split; intros.
rewrite <- H in H4.
elim H2 with x'; intros; trivial.
exists x2; trivial.
rewrite <- H0; trivial.
rewrite <- H in H4,H5|-.
rewrite <- H0 in H6,H7|-.
eauto.
destruct H2.
exists x1; trivial; split; intros.
rewrite H in H4.
elim H2 with x'; intros; trivial.
exists x2; trivial.
rewrite H0; trivial.
rewrite H in H4,H5|-.
rewrite H0 in H6,H7|-.
eauto.
Qed.
Instance le_card_refl : Reflexive le_card.
exists (fun x' y' => x' == y').
do 3 red; intros.
rewrite H; rewrite H0; reflexivity.
split; intros.
exists x'; trivial; reflexivity.
rewrite H3; rewrite H4; trivial.
Qed.
Instance le_card_trans : Transitive le_card.
red.
destruct 1 as (R,Rm,(incl,inj));
destruct 1 as (R',R'm,(incl',inj')).
exists (fun x' z' => exists2 y', y' ∈ y & R x' y' /\ R' y' z'); [|split;intros].
do 3 red; intros.
apply ex2_morph.
red; reflexivity.
red; intros.
rewrite H; rewrite H0; reflexivity.
elim incl with x'; trivial; intros.
elim incl' with x0; trivial; intros.
exists x1; trivial.
exists x0; auto.
destruct H3 as (y1',in1,(r1,r1'));
destruct H4 as (y2',in2,(r2,r2')).
eauto.
Qed.
Definition lt_card x y :=
~ le_card y x.
Lemma incl_le_card : ∀ x y, x ⊆ y -> le_card x y.
intros.
exists (fun x y => x == y); [|split;intros].
do 3 red; intros.
rewrite H0; rewrite H1; reflexivity.
exists x'; auto.
reflexivity.
rewrite H4; rewrite H5; trivial.
Qed.
Lemma cantor_le : ∀ x, lt_card x (power x).
red; red; intros.
destruct H as (R,Rm,(incl,Rfun)).
pose (D := subset x (fun x' => ∀ x'' z, z ∈ power x ->
x'' == x' -> R z x'' -> ~ x'' ∈ z)).
assert (D ∈ power x).
apply power_intro; intros.
unfold D in H.
apply subset_elim1 with (1:=H).
elim incl with D; trivial; intros d in_d rel_d.
assert (~ d ∈ D).
red; intros.
unfold D in H0.
elim subset_elim2 with (1:=H0); intros.
apply H2 with d D; trivial.
apply H0.
unfold D; apply subset_intro; trivial.
intros.
rewrite H2.
assert (z == D).
apply Rfun with x'' d; auto.
rewrite H2; trivial.
rewrite H4; trivial.
Qed.
Lemma discr_power : ∀ x, ~ x == power x.
red; intros.
apply cantor_le with x.
rewrite <- H.
reflexivity.
Qed.
Definition equi_card (x y:set) : Prop :=
exists2 R : set -> set -> Prop,
Proper (eq_set ==> eq_set ==> iff) R &
(∀ x', x' ∈ x -> exists2 y', y' ∈ y & R x' y') /\
(∀ y', y' ∈ y -> exists2 x', x' ∈ x & R x' y') /\
(∀ x1 y1 x2 y2, x1 ∈ x -> x2 ∈ x -> y1 ∈ y -> y2 ∈ y ->
R x1 y1 -> R x2 y2 -> (x1 == x2 <-> y1 == y2)).
Instance equi_card_morph : Proper (eq_set ==> eq_set ==> iff) equi_card.
apply morph_impl_iff2; auto with *.
unfold equi_card; do 4 red; intros.
destruct H1 as (R,Rm,(incl1,(incl2,bij))).
exists R; [trivial|split;[|split]]; intros.
rewrite <- H in H1.
destruct (incl1 x'); trivial.
rewrite H0 in H2.
exists x1; trivial.
rewrite <- H0 in H1.
destruct (incl2 y'); trivial.
rewrite H in H2.
exists x1; trivial.
rewrite <- H in H1,H2.
rewrite <- H0 in H3,H4.
auto.
Qed.
Instance equi_card_refl : Reflexive equi_card.
exists (fun x' y' => x' == y').
do 3 red; intros.
rewrite H; rewrite H0; reflexivity.
split; [|split]; intros.
exists x'; trivial; reflexivity.
exists y'; trivial; reflexivity.
rewrite H3; rewrite H4; reflexivity.
Qed.
Instance equi_card_sym : Symmetric equi_card.
red; destruct 1 as (R,Rm,(incl1,(incl2,bij))).
exists (fun x' y' => R y' x'); intros; auto.
do 3 red; intros; apply Rm; trivial.
split;[|split]; trivial.
symmetry; auto.
Qed.
Instance equi_card_trans : Transitive equi_card.
red.
destruct 1 as (R,Rm,(incl1,(incl2,bij)));
destruct 1 as (R',R'm,(incl1',(incl2',bij'))).
exists (fun x' z' => exists2 y', y' ∈ y & R x' y' /\ R' y' z').
do 3 red; intros.
apply ex2_morph.
red; reflexivity.
red; intros.
rewrite H; rewrite H0; reflexivity.
split; [|split]; intros.
elim incl1 with x'; trivial; intros.
elim incl1' with x0; trivial; intros.
exists x1; trivial.
exists x0; auto.
elim incl2' with y'; trivial; intros.
elim incl2 with x0; trivial; intros.
exists x1; trivial.
exists x0; auto.
destruct H3 as (y1',in1,(r1,r1'));
destruct H4 as (y2',in2,(r2,r2')).
transitivity (y1' == y2'); auto.
Qed.
Lemma equi_card_le : ∀ x y, equi_card x y -> le_card x y.
destruct 1 as (R,Rm,(incl1,(incl2,bij))).
exists R; [trivial|split;intros;auto].
refine (proj2 (bij _ _ _ _ _ _ _ _ H3 H4) H5); trivial.
Qed.
Lemma cantor : ∀ x, ~ equi_card x (power x).
red; intros; apply (cantor_le x);
apply equi_card_le; apply equi_card_sym; trivial.
Qed.
Require Import ZFnats ZFord.
Definition isCard x :=
isOrd x /\ (∀ y, lt y x -> lt_card y x).
Definition regular_card o :=
∀ x F,
lt_card x o ->
ext_fun x F ->
(∀ y, y ∈ x -> lt_card (F y) o) ->
lt_card (sup x F) o.
Definition regular o := ∀ x F,
lt_card x o ->
ext_fun x F ->
(∀ y, y ∈ x -> lt (F y) o) ->
lt (sup x F) o.
Section RegularRelational.
Import ZFrepl.
Definition regular_rel o := ∀ x R,
lt_card x o ->
repl_rel x R ->
(∀ y z, y ∈ x -> R y z -> lt z o) ->
lt (union (repl x R)) o.
Lemma regular_weaker : ∀ o,
regular_rel o -> regular o.
red; intros.
change (sup x F) with (union (repl x (fun x y => y == F x))).
apply H; intros; auto.
apply repl_rel_fun; trivial.
rewrite H4; auto.
Qed.
End RegularRelational.
Definition regular' o := ∀ x F,
lt x o ->
ext_fun x F ->
(∀ y, y ∈ x -> lt (F y) o) ->
lt (sup x F) o.
Definition stronglyInaccessibleCard o :=
limitOrd o /\ regular o.
Definition lt_card2 a b :=
∀ R:set->set->Prop,
(∀ x x' y y', x ∈ a -> y ∈ b -> y' ∈ b ->
R x y -> R x' y' -> x==x' -> y==y') ->
exists2 y, y ∈ b & ∀ x, x ∈ a -> ~ R x y.
Lemma lt_card_weaker : ∀ a b,
lt_card2 a b -> lt_card a b.
red; red; intros.
destruct H0 as (R,?,(?,?)).
destruct (H (fun x y => R y x)).
intros.
apply H2 with x x'; trivial.
rewrite <- H8; trivial.
destruct H1 with x; trivial.
eapply H4; eauto.
Qed.
Require Import ZFrelations.
Require Import Relations.
Section Hartog.
Variable X:set.
Set Implciit Arguments.
Record REL A0 : Type := {
Rel :> A0 -> A0 -> Prop;
dom : A0 -> Prop;
wfrel : well_founded Rel
}.
Definition morphism A0 (R S : REL A0) (f : A0 -> A0) :=
(∀ x y, dom _ R x -> dom _ R y -> R x y -> S (f x) (f y)) /\
(∀ x, dom _ R x -> dom _ S (f x)).
Record emb A0 (R1 R2 : REL A0) : Prop := {
f : A0 -> A0;
fmorph : morphism _ R1 R2 f;
maj : A0;
majd : dom _ R2 maj;
majf : ∀ z, dom _ R1 z -> R2 (f z) maj}.
Parameter WF_emb : ∀ A0, well_founded (emb A0).
Definition emb0 A0 i0 (x y:A0) :=
exists2 R1, x = i0 R1 & exists2 R2, y = i0 R2 & emb A0 R1 R2.
Parameter WF_emb0 : ∀ A0 i0, well_founded (emb0 A0 i0).
Definition Emb A0 i0 (P:A0->Prop) : REL A0 :=
Build_REL _ (emb0 A0 i0) P (WF_emb0 A0 i0).
Parameter Burali_Forti
: ∀ (A0 : Type) (i0 : REL A0 -> A0),
(∀ R1 R2 : REL A0,
i0 R1 = i0 R2 -> exists f : A0 -> A0, morphism A0 R1 R2 f) -> False.
Definition order_type_assign_rel R a o :=
∀ P,
Proper (eq_set ==> eq_set ==> iff) P ->
(∀ x f,
let x' := subset X (fun y => rel_app R y x) in
ext_fun x' f ->
(∀ y, rel_app R y x -> P y (f y)) ->
P x (osup x' (fun y => osucc (f y)))) ->
P a o.
Instance order_type_assign_ext :
Proper (eq_set==>eq_set==>eq_set==>iff) order_type_assign_rel.
Admitted.
Lemma order_type_assign_rel_inv : ∀ r a x,
order_type_assign_rel r a x ->
exists2 f,
∀ b, rel_app r b a -> order_type_assign_rel r b (f b) &
let a' := subset X (fun b => rel_app r b a) in
ext_fun a' f /\ x == osup a' (fun y => osucc (f y)).
intros.
apply H; intros.
apply morph_impl_iff2; auto with *.
do 4 red; intros.
destruct H2.
exists x2; intros.
rewrite <- H0 in H4; auto.
destruct H3; split.
do 2 red; intros; apply H3; auto.
apply subset_intro.
apply subset_elim1 in H5; trivial.
apply subset_elim2 in H5; destruct H5.
rewrite H5; rewrite H0; trivial.
rewrite<- H1; rewrite H4.
apply osup_morph; auto.
apply subset_morph; auto with *.
red; intros.
rewrite H0; auto with *.
red; intros.
apply osucc_morph.
apply H3; trivial.
exists f; intros.
2:split; [trivial|reflexivity].
red; intros.
destruct H1 with b; trivial.
destruct H6.
rewrite H7.
apply H4; intros; trivial.
apply H5; trivial.
Qed.
Require Import ZFrepl.
Require Import Relations.
Definition isWellOrder R :=
∀ x, Acc (rel_app R) x.
Instance isWO_m : Proper (eq_set ==> iff) isWellOrder.
Admitted.
Lemma order_type_assign_uchoice : ∀ R a,
isWellOrder R ->
uchoice_pred (order_type_assign_rel R a).
intros.
elim (H a); intros.
split;[|split]; intros.
rewrite <- H2; trivial.
exists (osup (subset X (fun z => rel_app R z x))
(fun z => osucc (uchoice (order_type_assign_rel R z)))).
red; intros.
apply H3; intros.
do 2 red; intros.
apply uchoice_morph_raw.
red; intros.
rewrite H5; rewrite H6; reflexivity.
apply (uchoice_def _ (H1 _ H4)); trivial.
clear a.
revert x' H1 H3.
apply H2; intros.
apply morph_impl_iff2; auto with *.
do 4 red; intros.
rewrite <- H3; apply H4; intros.
apply H5.
rewrite <- H1; trivial.
rewrite H1; trivial.
destruct order_type_assign_rel_inv with (1:=H5) as (f',?,(_,?)).
rewrite H7.
apply osup_morph.
apply subset_morph; auto with *.
red; intros.
apply osucc_morph.
apply H3; intros; auto.
apply subset_elim2 in H8; destruct H8.
rewrite H8; trivial.
apply H4.
admit. rewrite H9.
apply H6.
rewrite <- H9.
apply subset_elim2 in H8; destruct H8.
rewrite H8; trivial.
Qed.
Lemma order_type_assign_rel_inv' : ∀ r a,
isWellOrder r ->
uchoice (order_type_assign_rel r a) ==
osup (subset X (fun b => rel_app r b a))
(fun b => osucc (uchoice (order_type_assign_rel r b))).
intros.
generalize (uchoice_def _ (order_type_assign_uchoice _ a H)); intro.
apply order_type_assign_rel_inv in H0; destruct H0.
destruct H1.
rewrite H2.
apply osup_morph; auto with *.
red; intros.
apply osucc_morph.
rewrite (H1 x0 x'); trivial.
rewrite H4 in H3; clear x0 H4.
apply subset_elim2 in H3; destruct H3.
rewrite <- H3 in H4 ;clear x0 H3.
apply H0 in H4.
apply uchoice_ext; trivial.
apply order_type_assign_uchoice; trivial.
Qed.
Lemma order_type_assign_ord : ∀ R a o,
order_type_assign_rel R a o ->
isOrd o.
intros.
red in H.
pattern a, o; apply H.
do 3 red; intros.
rewrite H1; reflexivity.
intros.
apply isOrd_osup; intros.
do 2 red; intros.
apply osucc_morph; apply H0; trivial.
apply subset_elim2 in H2; destruct H2.
rewrite <- H2 in H3; auto.
Qed.
Definition order_type R :=
osup X (fun a => osucc (uchoice (order_type_assign_rel R a))).
Lemma ot_ext : ∀ x x',
x == x' ->
eq_fun X
(fun a => osucc (uchoice (order_type_assign_rel x a)))
(fun a => osucc (uchoice (order_type_assign_rel x' a))).
red; intros.
apply osucc_morph.
apply uchoice_morph_raw.
apply order_type_assign_ext; auto with *.
Qed.
Instance order_type_ext : morph1 order_type.
unfold order_type.
do 2 red; intros.
apply osup_morph; auto with *.
apply ot_ext; trivial.
Qed.
Definition wo := subset (rel X X) isWellOrder.
Lemma wo_def2 : ∀ r, r ∈ wo -> isWellOrder r.
intros.
apply subset_elim2 in H; destruct H.
rewrite H; trivial.
Qed.
Hint Resolve wo_def2.
Definition hartog_succ :=
osup wo order_type.
Lemma isOrd_hartog : isOrd hartog_succ.
unfold hartog_succ.
apply isOrd_osup.
do 2 red; intros.
rewrite H0; reflexivity.
intros.
unfold order_type.
apply isOrd_osup.
red; apply ot_ext; reflexivity.
intros.
apply wo_def2 in H.
generalize (uchoice_def _ (order_type_assign_uchoice _ x0 H)).
intros.
apply isOrd_succ.
apply order_type_assign_ord with (1:=H1).
Qed.
Lemma hartog_assign_surj : ∀ x,
x ∈ hartog_succ ->
exists2 R, R ∈ wo &
∀ y, y ∈ x -> exists2 b, b ∈ X & order_type_assign_rel R b y.
Admitted.
Section BuraliForti.
Variable I : set -> set -> Prop.
Hypothesis ty_I : ∀ x,
x ∈ hartog_succ -> exists2 y, y ∈ X & I x y.
Hypothesis inj_I : ∀ x1 y1 x2 y2,
x1 ∈ hartog_succ ->
x2 ∈ hartog_succ ->
y1 ∈ X ->
y2 ∈ X ->
I x1 y1 ->
I x2 y2 ->
y1 == y2 -> x1 == x2.
Definition OT R :=
order_type (inject_rel (fun x y => dom _ R x /\ dom _ R y /\ R x y) X X).
Parameter OT_inj : ∀ (R1 R2:REL set),
(∀ x, dom _ R1 x -> x ∈ X) ->
(∀ x, dom _ R2 x -> x ∈ X) ->
OT R1 ⊆ OT R2 -> exists f, morphism _ R1 R2 f.
Lemma burali_forti : False.
generalize ty_I inj_I.
admit.
Qed.
End BuraliForti.
End Hartog.