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.
Qed.
Instance le_card_refl : Reflexive le_card.
Qed.
Instance le_card_trans : Transitive le_card.
Qed.
Definition lt_card x y :=
~ le_card y x.
Lemma incl_le_card : ∀ x y, x ⊆ y -> le_card x y.
Lemma cantor_le : ∀ x, lt_card x (power x).
Lemma discr_power : ∀ x, ~ x == power x.
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.
Qed.
Instance equi_card_refl : Reflexive equi_card.
Qed.
Instance equi_card_sym : Symmetric equi_card.
Qed.
Instance equi_card_trans : Transitive equi_card.
Qed.
Lemma equi_card_le : ∀ x y, equi_card x y -> le_card x y.
Lemma cantor : ∀ x, ~ equi_card x (power x).
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.
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.
Require Import ZFrelations.
Require Import Relations.
Section Hartog.
Variable X:set.
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)).
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).
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))).
Lemma order_type_assign_ord : ∀ R a o,
order_type_assign_rel R a o ->
isOrd o.
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))).
Instance order_type_ext : morph1 order_type.
Qed.
Definition wo := subset (rel X X) isWellOrder.
Lemma wo_def2 : ∀ r, r ∈ wo -> isWellOrder r.
Hint Resolve wo_def2.
Definition hartog_succ :=
osup wo order_type.
Lemma isOrd_hartog : isOrd hartog_succ.
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.
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.
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.
Qed.
Instance le_card_refl : Reflexive le_card.
Qed.
Instance le_card_trans : Transitive le_card.
Qed.
Definition lt_card x y :=
~ le_card y x.
Lemma incl_le_card : ∀ x y, x ⊆ y -> le_card x y.
Lemma cantor_le : ∀ x, lt_card x (power x).
Lemma discr_power : ∀ x, ~ x == power x.
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.
Qed.
Instance equi_card_refl : Reflexive equi_card.
Qed.
Instance equi_card_sym : Symmetric equi_card.
Qed.
Instance equi_card_trans : Transitive equi_card.
Qed.
Lemma equi_card_le : ∀ x y, equi_card x y -> le_card x y.
Lemma cantor : ∀ x, ~ equi_card x (power x).
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.
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.
Require Import ZFrelations.
Require Import Relations.
Section Hartog.
Variable X:set.
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)).
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).
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))).
Lemma order_type_assign_ord : ∀ R a o,
order_type_assign_rel R a o ->
isOrd o.
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))).
Instance order_type_ext : morph1 order_type.
Qed.
Definition wo := subset (rel X X) isWellOrder.
Lemma wo_def2 : ∀ r, r ∈ wo -> isWellOrder r.
Hint Resolve wo_def2.
Definition hartog_succ :=
osup wo order_type.
Lemma isOrd_hartog : isOrd hartog_succ.
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.
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.
End BuraliForti.
End Hartog.