Library ZFrank

Require Import ZF ZFnats ZFord ZFstable ZFfix.

  Definition VN := TI power.

Instance VN_morph : morph1 VN.
Qed.

  Lemma VN_def : ∀ x z,
    isOrd x ->
    (z ∈ VN x <-> exists2 y, y ∈ x & z ⊆ VN y).

  Lemma VN_trans : ∀ o x y,
    isOrd o ->
    x ∈ VN o ->
    y ∈ x ->
    y ∈ VN o.

  Lemma VN_incl : ∀ o x y,
    isOrd o ->
    y ⊆ x ->
    x ∈ VN o ->
    y ∈ VN o.

Lemma VN_mono : ∀ o x,
  isOrd o ->
  lt x o -> VN x ∈ VN o.

Lemma VN_mono_le : ∀ o o',
  isOrd o ->
  isOrd o' ->
  o ⊆ o' ->
  VN o ⊆ VN o'.

  Lemma VN_stable : stable_ord VN.

Lemma VN_compl : ∀ x z, isOrd x -> isOrd z -> z ∈ VN x -> VN z ∈ VN x.

Lemma VN_intro :
  ∀ x, isOrd x -> x ⊆ VN x.

Lemma VN_succ : ∀ x, isOrd x -> power (VN x) == VN (osucc x).

  Lemma VN_ord_inv : ∀ o x, isOrd o -> isOrd x -> x ∈ VN o -> lt x o.

  Lemma VN_subset : ∀ o x P, isOrd o -> x ∈ VN o -> subset x P ∈ VN o.

  Lemma VN_union : ∀ o x, isOrd o -> x ∈ VN o -> union x ∈ VN o.

  Lemma VNsucc_power : ∀ o x,
    isOrd o ->
    x ∈ VN o ->
    power x ∈ VN (osucc o).

  Lemma VNsucc_pair : ∀ o x y, isOrd o ->
    x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN (osucc o).

  Lemma VNlim_def : ∀ o x, limitOrd o ->
    (x ∈ VN o <-> exists2 o', lt o' o & x ∈ VN o').

  Lemma VNlim_power : ∀ o x, limitOrd o -> x ∈ VN o -> power x ∈ VN o.


  Lemma VNlim_pair : ∀ o x y, limitOrd o ->
    x ∈ VN o -> y ∈ VN o -> pair x y ∈ VN o.

Require Import ZFrelations.

  Lemma VN_func : ∀ o A B,
    isOrd o ->
    A ∈ VN o ->
    B ∈ VN o ->
    func A B ∈ VN (osucc (osucc (osucc (osucc o)))).

Require Import ZFwf.

Lemma VN_wf o x : isOrd o -> x ∈ VN o -> isWf x.

Lemma VN_osup2 o :
  isOrd o ->
  ∀ x y,
  x ∈ VN o ->
  y ∈ VN o ->
  x ⊔ y ∈ VN o.


Lemma VN_N : N ⊆ VN omega.

Definition VN_regular o :=
  ∀ x F,
  ext_fun x F ->
  x ∈ VN o ->
  (∀ y, y ∈ x -> F y ∈ VN o) ->
  sup x F ∈ VN o.

Definition bound_ord A o :=
  ∀ F, ext_fun A F ->
  (∀ n, n ∈ A -> lt (F n) o) ->
  lt (osup A F) o.

Lemma VN_ord_sup F o :
  isOrd o ->
  VN_regular o ->
  omega ∈ o ->
  (∀ n, F n ∈ VN o) ->
  ord_sup F ∈ VN o.

Lemma VN_reg_ord : ∀ o,
  isOrd o ->
  VN_regular o ->
  omega ∈ o ->
  ∀ x F,
  ext_fun x F ->
  x ∈ VN o ->
  (∀ y, y ∈ x -> lt (F y) o) ->
  lt (osup x F) o.

Definition VN_inaccessible o :=
  limitOrd o /\ VN_regular o.

Require Import ZFrepl.

Definition VN_regular_rel o :=
  ∀ x R,
  repl_rel x R ->
  x ∈ VN o ->
  (∀ y z, y ∈ x -> R y z -> z ∈ VN o) ->
  union (repl x R) ∈ VN o.

Definition VN_inaccessible_rel o :=
  limitOrd o /\ VN_regular_rel o.

Section UnionClosure.

  Variable mu : set.
  Hypothesis mu_ord : isOrd mu.
  Hypothesis mu_lim : ∀ x, lt x mu -> lt (osucc x) mu.
  Hypothesis mu_reg : VN_regular_rel mu.
  Hypothesis mu_inf : omega ∈ mu.

  Lemma VN_regular_weaker : VN_regular mu.

Let mul : limitOrd mu := conj mu_ord mu_lim.


  Lemma VN_clos_pair : ∀ x y,
    x ∈ VN mu -> y ∈ VN mu -> pair x y ∈ VN mu.

  Definition lt_cardf a b :=
    ∀ F, ext_fun a F ->
    exists2 y, y ∈ b & ∀ x, x ∈ a -> ~ y == F x.

  Lemma VN_cardf : ∀ a,
    a ∈ VN mu -> lt_cardf a mu.

Require Import ZFcard.

  Lemma VNcard : ∀ x,
    x ∈ VN mu -> lt_card x mu.

  Lemma reg_card : isCard mu.

End UnionClosure.