Library ZFcard
Require Import ZF.
Import IZF.
Definition le_card (x y:set) : Prop :=
exists2 R : set -> set -> Prop,
(forall x', x' \in x -> exists2 y', y' \in y & R x' y') &
(forall x1 y1 x2 y2, x1 \in x -> x2 \in x -> y1 \in y -> y2 \in 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.
Lemma incl_le_card : forall x y, x \incl y -> le_card x y.
Lemma cantor_le : forall x, ~ le_card (power x) x.
Lemma discr_power : forall x, ~ x == power x.
Definition equi_card (x y:set) : Prop :=
exists2 R : set -> set -> Prop,
(forall x', x' \in x -> exists2 y', y' \in y & R x' y') /\
(forall y', y' \in y -> exists2 x', x' \in x & R x' y') &
(forall x1 y1 x2 y2, x1 \in x -> x2 \in x -> y1 \in y -> y2 \in 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 : forall x y, equi_card x y -> le_card x y.
Lemma cantor : forall x, ~ equi_card x (power x).
Require Import ZFnats ZFord.
Definition lt_card x y :=
~ le_card y x.
Definition isCard x :=
isOrd x /\ (forall y, lt y x -> lt_card y x).
Definition regular_card o :=
forall x F,
lt_card x o ->
ext_fun x F ->
(forall y, y \in x -> lt_card (F y) o) ->
lt_card (sup x F) o.
Lemma lt_card_non_zero :
forall x o, isOrd o -> lt_card x o -> lt zero o.
Definition regular o := forall x F,
lt_card x o ->
ext_fun x F ->
(forall y, y \in x -> lt (F y) o) ->
lt (sup x F) o.
Definition regular' o := forall x F,
lt x o ->
ext_fun x F ->
(forall y, y \in x -> lt (F y) o) ->
lt (sup x F) o.
Definition stronglyInaccessibleCard o :=
limitOrd o /\ regular o.
Import IZF.
Definition le_card (x y:set) : Prop :=
exists2 R : set -> set -> Prop,
(forall x', x' \in x -> exists2 y', y' \in y & R x' y') &
(forall x1 y1 x2 y2, x1 \in x -> x2 \in x -> y1 \in y -> y2 \in 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.
Lemma incl_le_card : forall x y, x \incl y -> le_card x y.
Lemma cantor_le : forall x, ~ le_card (power x) x.
Lemma discr_power : forall x, ~ x == power x.
Definition equi_card (x y:set) : Prop :=
exists2 R : set -> set -> Prop,
(forall x', x' \in x -> exists2 y', y' \in y & R x' y') /\
(forall y', y' \in y -> exists2 x', x' \in x & R x' y') &
(forall x1 y1 x2 y2, x1 \in x -> x2 \in x -> y1 \in y -> y2 \in 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 : forall x y, equi_card x y -> le_card x y.
Lemma cantor : forall x, ~ equi_card x (power x).
Require Import ZFnats ZFord.
Definition lt_card x y :=
~ le_card y x.
Definition isCard x :=
isOrd x /\ (forall y, lt y x -> lt_card y x).
Definition regular_card o :=
forall x F,
lt_card x o ->
ext_fun x F ->
(forall y, y \in x -> lt_card (F y) o) ->
lt_card (sup x F) o.
Lemma lt_card_non_zero :
forall x o, isOrd o -> lt_card x o -> lt zero o.
Definition regular o := forall x F,
lt_card x o ->
ext_fun x F ->
(forall y, y \in x -> lt (F y) o) ->
lt (sup x F) o.
Definition regular' o := forall x F,
lt x o ->
ext_fun x F ->
(forall y, y \in x -> lt (F y) o) ->
lt (sup x F) o.
Definition stronglyInaccessibleCard o :=
limitOrd o /\ regular o.