Library ZFfix

Require Import ZF.
Require Import ZFrelations.
Import IZF.

Require Import ZFord.
Require Import ZFnats.

Section IterMonotone.

  Variable F : set -> set.
  Variable Fmono : Proper (incl_set ==> incl_set) F.

  Instance Fmono_morph: Proper (eq_set ==> eq_set) F.

Qed.
Hint Resolve Fmono_morph.

  Lemma TI_mono : increasing (TI F).

  Lemma TI_incl : forall o, isOrd o ->
    forall o', lt o' o ->
    TI F o' \incl TI F o.

  Lemma TI_mono_succ : forall o,
    isOrd o ->
    TI F (osucc o) == F (TI F o).

  Lemma TI_pre_fix : forall fx o,
     isOrd o ->
     F fx \incl fx ->
     TI F o \incl fx.


End IterMonotone.

  Definition VN := TI power.

  Lemma VN_trans : forall o x y,
    isOrd o ->
    x \in VN o ->
    y \in x ->
    y \in VN o.

  Lemma VN_incl : forall o x y,
    isOrd o ->
    y \incl x ->
    x \in VN o ->
    y \in VN o.

  Lemma VNsucc_power : forall o x,
    isOrd o ->
    x \in VN o ->
    power x \in VN (osucc o).

  Lemma VNlim_clos_power : forall o x, limitOrd o -> x \in VN o -> power x \in VN o.

  Lemma VN_clos_union : forall o x, isOrd o -> x \in VN o -> union x \in VN o.

Require Import ZFcard.
Require Import ZFrepl.
Require Import ZFordcl ZFord_equiv.
Import ZFord.

  Lemma repl_rel_incl : forall x y R,
    x \incl y ->
    repl_rel y R ->
    repl_rel x R.

Section Inaccessible.

  Variable mu : set.
  Variable mu_ord : isOrd mu.
  Variable mu_lim : forall x, lt x mu -> lt (osucc x) mu.
  Variable mu_regular : regular mu.

  Lemma VNcard : forall x,
    x \in VN mu -> lt_card x mu.

  Lemma VNlim_clos_union_repl : forall I R,
    repl_rel I R ->
    I \in VN mu ->
    (forall x y, x \in I -> R x y -> y \in VN mu) ->
    union (repl I R) \in VN mu.

End Inaccessible.

Section InaccessibleCard.

  Variable mu : set.
  Variable mu_card : isCard mu.
  Variable mu_lim : forall x, lt x mu -> lt (osucc x) mu.
  Variable mu_regular : regular_card mu.

  Let mu_ord : isOrd mu.
Qed.
  Let mu_lt : forall x, lt x mu -> lt_card x mu.
Qed.

  Lemma lt_card_lt : forall x, isOrd x -> lt_card x mu -> lt x mu.

  Lemma VNcard' : forall x,
    x \in VN mu -> lt_card x mu.

  Lemma VNreg_clos_sup : forall I F,
    ext_fun I F ->
    I \in VN mu ->
    (forall x, x \in I -> F x \in VN mu) ->
    sup I F \in VN mu.

End InaccessibleCard.