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.