# 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.