Theory bnfInitial

⊢ ∀sta A s. bnfALG sta (A,s) ⇔ ∀x. x ∈ bnfFIN sta A ⇒ s x ∈ A

⊢ ∀A f x. bnfARBIFY A f x = if x ∈ A then f x else ARB

⊢ ∀mp sta.
    bnfBIGPROD mp sta =
    ({ff | ∀i. ff i ∈ FST (bnfMKALG sta i)},
     (λfv i. SND (bnfMKALG sta i) (mp (λff. ff i) fv)))

⊢ ∀sta As. bnfFIN sta As = {a | sta a ⊆ As}

⊢ ∀mp sta stb h A s B t.
    bnfHOM mp sta stb h (A,s) (B,t) ⇔
    bnfALG sta (A,s) ∧ bnfALG stb (B,t) ∧ (∀a. a ∈ A ⇒ h a ∈ B) ∧
    ∀af. af ∈ bnfFIN sta A ⇒ t (mp h af) = h (s af)

⊢ ∀stp mp sta. bnfIALG stp mp sta = bnfMINSET stp (bnfICONS mp sta)

⊢ ∀mp sta. bnfICONS mp sta = SND (bnfBIGPROD mp sta)

⊢ ∀sta s.
    bnfKK sta s 0 = ∅ ∧
    (∀a. bnfKK sta s a⁺ = bnfKK sta s a ∪ {s x | x | sta x ⊆ bnfKK sta s a}) ∧
    ∀a. 0 < a ∧ islimit a ⇒
        bnfKK sta s a = BIGUNION (IMAGE (bnfKK sta s) (preds a))

⊢ ∀sta s. bnfMINSET sta s = BIGINTER {B | bnfALG sta (B,s)}

⊢ ∀sta p. bnfMKALG sta p = if bnfALG sta p then p else (𝕌(:α),SND p)

⊢ ∀mp_ab mp_bc mp_ac.
    bnfMapComp mp_ab mp_bc mp_ac ⇔
    ∀f g x. mp_bc g (mp_ab f x) = mp_ac (g ∘ f) x

⊢ ∀mp sta.
    bnfMapCong mp sta ⇔
    ∀f g x. (∀a. a ∈ sta x ⇒ f a = g a) ⇒ mp f x = mp g x

⊢ ∀mp. bnfMapId mp ⇔ ∀x. mp I x = x

⊢ ∀mp_np s rep abs af. bnfNCONS mp_np s rep abs af = abs (s (mp_np rep af))

⊢ ∀mp sta stb. bnfNatural mp sta stb ⇔ ∀f x. stb (mp f x) = IMAGE f (sta x)

⊢ ∀sta A s B t.
    bnfSUBALG sta (A,s) (B,t) ⇔
    bnfALG sta (A,s) ∧ bnfALG sta (B,t) ∧
    (∀af. af ∈ bnfFIN sta A ⇒ s af = t af) ∧ A ⊆ B

⊢ bnfNatural mp_Fp stF stp ⇒
  bnfALG stp (A,s) ⇒
  bnfALG stF (bnfFIN stp A,mp_Fp s)

⊢ bnfALG stn (𝕌(:ξ),bnfNCONS mp_np s rep abs)

⊢ bnfALG sta (𝕌(:β),s)

⊢ (∀C. C ≼ bnfFIN sto C) ∧ (∀u v. u ≼ v ⇒ bnfFIN sta u ≼ bnfFIN stab v) ∧
  (∀B. 𝟚 ≼ B ⇒ bnfFIN stab B ≼ B ** cardSUC (bnfFIN sto (preds bd))) ⇒
  ω ≤ bd ⇒
  bnfKK sta s (csuc bd) ≼ 𝟚 ** cardSUC (bnfFIN sto (preds bd))

⊢ bnfALG sta (A,s) ∧ sta x ⊆ A ⇒ s x ∈ A

⊢ (∃w. sta w = ∅) ⇒ bnfALG sta (A,s) ⇒ A ≠ ∅

⊢ bnfNatural mp stp sta ⇒ bnfALG stp (bnfBIGPROD mp sta)

⊢ bnfNatural mp stp sta ⇒
  bnfALG stp (FST (bnfBIGPROD mp sta),bnfICONS mp sta)

⊢ bnfNatural mp stp sta ⇒
  bnfALG sta (A,s) ⇒
  bnfHOM mp stp sta (λff. ff (A,s)) (bnfBIGPROD mp sta) (A,s)

⊢ bnfNatural mp stp sta ⇒
  bnfALG sta (A,s) ⇒
  bnfHOM mp stp sta (λff. ff (A,s))
    (FST (bnfBIGPROD mp sta),bnfICONS mp sta) (A,s)

⊢ ∀s. s ≼ 𝕌(:α)

⊢ bnfNatural mp_a2o sta sto ∧ bnfNatural mp_o2a sto sta ∧
  bnfMapComp mp_a2o mp_o2a mp_aa ∧ bnfMapId mp_aa ∧ bnfMapCong mp_aa sta ∧
  (∀C. C ≼ bnfFIN sto C) ⇒
  ω ≤ bd ∧ (∀x. sta x ≼ preds bd) ⇒
  ∀B. 𝟚 ≼ B ⇒ bnfFIN sta B ≼ B ** cardSUC (bnfFIN sto (preds bd))

⊢ (∀n. abs (rep n) = n) ∧ (∀af. stn af = ∅) ⇒
  ∀P. (∀af. (∀y. y ∈ stn af ⇒ P y) ⇒ P (abs af)) ⇒ ∀n. P n

⊢ (∀n. abs (rep n) = n) ∧ (∀p. rep (abs p) = p) ∧ (∀h af. mp h af = af) ⇒
  ∀t. ∃!h. ∀af. h (abs af) = t af (mp h af)

⊢ (∀n. abs (rep n) = n) ∧ (∀p. rep (abs p) = p) ∧ (∀h af. mp h af = af) ⇒
  ∀t. ∃!h. ∀af. h (abs af) = t (mp h af)

⊢ s ⊆ t ⇒ bnfFIN sta s ⊆ bnfFIN sta t

⊢ bnfFIN sta 𝕌(:β) = 𝕌(:α)

⊢ bnfMapId mp_aa ∧ bnfMapCong mp_aa sta ∧ bnfNatural mp_ab sta stb ∧
  bnfMapComp mp_ab mp_ba mp_aa ⇒
  s ≼ t ⇒
  bnfFIN sta s ≼ bnfFIN stb t

⊢ bnfMapComp mp_pn mp_np mp_pp ∧ bnfMapId mp_pp ∧ bnfMapCong mp_pp stp ∧
  (∀p. p ∈ A ⇒ rep (abs p) = p) ∧ bnfALG stp (A,s) ⇒
  bnfHOM mp_pn stp stn abs (A,s) (𝕌(:ξ),bnfNCONS mp_np s rep abs)

⊢ bnfMapCong mp sta ⇒
  (bnfHOM mp sta stb (bnfARBIFY A f) (A,s) (B,t) ⇔
   bnfHOM mp sta stb f (A,s) (B,t))

⊢ bnfNatural mp_Fp stF stp ⇒
  bnfALG stp (A,s) ⇒
  bnfHOM mp_Fp stF stp s (bnfFIN stp A,mp_Fp s) (A,s)

⊢ bnfNatural mp_np stn stp ∧ (∀n. rep n ∈ A) ∧
  (∀p. p ∈ A ⇒ rep (abs p) = p) ∧ bnfALG stp (A,s) ⇒
  bnfHOM mp_np stn stp rep (𝕌(:ξ),bnfNCONS mp_np s rep abs) (A,s)

⊢ bnfMapCong mp sta ⇒
  bnfHOM mp sta stb h (A,s) (B,t) ⇒
  ∃j. bnfHOM mp sta stb j (A,s) (B,t) ∧ ∀x. x ∉ A ⇒ j x = ARB

⊢ ∀stb mp_ab mp_bc B t.
    bnfMapComp mp_ab mp_bc mp_ac ∧ bnfNatural mp_ab sta stb ∧
    bnfHOM mp_ab sta stb f (A,s) (B,t) ∧ bnfHOM mp_bc stb stc g (B,t) (C,u) ⇒
    bnfHOM mp_ac sta stc (g ∘ f) (A,s) (C,u)

⊢ bnfMapCong mp sta ⇒
  bnfHOM mp sta stb h (A,s) (B,t) ∧ (∀a. a ∈ A ⇒ h' a = h a) ⇒
  bnfHOM mp sta stb h' (A,s) (B,t)

⊢ bnfALG stp (bnfIALG stp mp sta,bnfICONS mp sta)

⊢ bnfNatural mp_pa stp sta ∧ bnfNatural mp_pp stp stp ∧ bnfMapId mp_pp ∧
  bnfMapComp mp_pp mp_pa mp_pa ∧ bnfNatural mp_pc stp stc ∧
  bnfMapComp mp_pa mp_ac mp_pc ∧ bnfMapComp mp_pc mp_cc mp_pc ∧
  bnfNatural mp_ac sta stc ∧ bnfNatural mp_ca stc sta ∧
  bnfMapComp mp_ca mp_ac mp_cc ∧ bnfMapId mp_cc ∧ bnfMapCong mp_cc stc ∧
  (∀t. bnfMINSET stc t ≼ 𝕌(:α)) ⇒
  ∀t G.
    bnfALG stc (G,t) ⇒
    ∃h. bnfHOM mp_pc stp stc h (bnfIALG stp mp_pa sta,bnfICONS mp_pa sta)
          (G,t)

⊢ (∃w. stp w = ∅) ⇒ ∃x. bnfIALG stp mp_pa sta x

⊢ bnfMapId mp_pp ∧ bnfNatural mp_pa stp sta ⇒
  bnfHOM mp_pp stp stp I (bnfIALG stp mp_pa sta,bnfICONS mp_pa sta)
    (FST (bnfBIGPROD mp_pa sta),bnfICONS mp_pa sta)

⊢ (∃w. stp w = ∅) ⇒ bnfIALG stp mp_pa sta ≠ ∅

⊢ ∀P. (∀x. stp x ⊆ bnfIALG stp mp_pa sta ∧ (∀y. y ∈ stp x ⇒ P y) ⇒
           P (bnfICONS mp_pa sta x)) ⇒
      ∀x. x ∈ bnfIALG stp mp_pa sta ⇒ P x

⊢ bnfMapCong mp_pc stp ∧ bnfNatural mp_pa stp sta ∧
  bnfNatural mp_pp stp stp ∧ bnfMapId mp_pp ∧
  bnfMapComp mp_pp mp_pa mp_pa ∧ bnfNatural mp_pc stp stc ∧
  bnfMapComp mp_pa mp_ac mp_pc ∧ bnfMapComp mp_pc mp_cc mp_pc ∧
  bnfNatural mp_ac sta stc ∧ bnfNatural mp_ca stc sta ∧
  bnfMapComp mp_ca mp_ac mp_cc ∧ bnfMapId mp_cc ∧ bnfMapCong mp_cc stc ∧
  (∀t. bnfMINSET stc t ≼ 𝕌(:α)) ⇒
  ∀t G.
    bnfALG stc (G,t) ⇒
    ∃!h.
      bnfHOM mp_pc stp stc h (bnfIALG stp mp_pa sta,bnfICONS mp_pa sta)
        (G,t) ∧ ∀x. x ∉ bnfIALG stp mp_pa sta ⇒ h x = ARB

⊢ a ∈ bnfFIN sta As ⇔ sta a ⊆ As

⊢ x ∈ bnfMINSET sta s ⇔ ∀A. bnfALG sta (A,s) ⇒ x ∈ A

⊢ ∀a. bnfKK sta s a ⊆ bnfMINSET sta s

⊢ {s x | x | sta x ⊆ bnfKK sta s e} = bnfKK sta s e ⇒
  bnfALG sta (bnfKK sta s e,s)

⊢ ∀b a. a < b ⇒ bnfKK sta s a ⊆ bnfKK sta s b

⊢ ∀a b. a ≤ b ⇒ bnfKK sta s a ⊆ bnfKK sta s b

⊢ BIGUNION (IMAGE (bnfKK sta s) (preds a)) ⊆ bnfKK sta s a

⊢ ords ≼ 𝕌(:num + η) ⇒
  bnfKK sta s (sup ords) = BIGUNION (IMAGE (bnfKK sta s) ords)

⊢ bnfKK sta s a =
  if a = 0o then ∅
  else
    BIGUNION (IMAGE (λb. {s fv | fv | sta fv ⊆ bnfKK sta s b}) (preds a))

⊢ bnfMapId mp ⇒
  ω ≤ bd ∧ (∀x. sta x ≼ preds bd) ⇒
  bnfKK sta s (csuc bd) = bnfMINSET sta s

⊢ bnfMapCong mp_pp stp ∧ bnfMapId mp_pp ∧ bnfNatural mp_Fp stF stp ∧
  bnfMapComp mp_pF mp_Fp mp_pp ∧ bnfMapCong mp_pF stp ∧
  bnfNatural mp_pF stp stF ∧ bnfALG stp (A,s) ∧
  (∀t G.
     bnfALG stF (G,t) ⇒
     ∃!h. bnfHOM mp_pF stp stF h (A,s) (G,t) ∧ ∀x. x ∉ A ⇒ h x = ARB) ∧
  (∀t G.
     bnfALG stp (G,t) ⇒
     ∃!h. bnfHOM mp_pp stp stp h (A,s) (G,t) ∧ ∀x. x ∉ A ⇒ h x = ARB) ⇒
  BIJ s (bnfFIN stp A) A

⊢ bnfMapId mp_aa ∧ bnfMapCong mp_aa sta ∧ bnfNatural mp_ab sta stab ∧
  bnfMapComp mp_ab mp_ba mp_aa ∧ bnfMapId mp_bb ∧ bnfMapCong mp_bb stab ∧
  bnfNatural mp_bo stab sto ∧ bnfNatural mp_ob sto stab ∧
  bnfMapComp mp_bo mp_ob mp_bb ∧ bnfNatural mp_oo sto sto ∧
  (∃x. sto x ≠ ∅) ∧ ω ≤ bd ∧ (∀x. sta x ≼ preds bd) ∧
  (∀x. stab x ≼ preds bd) ⇒
  ∀s. bnfMINSET sta s ≼ 𝟚 ** cardSUC (bnfFIN sto (preds bd))

⊢ bnfMapId mp ⇒
  bnfALG sta (A,s) ⇒
  bnfHOM mp sta sta I (bnfMINSET sta s,s) (A,s)

⊢ bnfALG sta (A,s) ⇒ bnfSUBALG sta (bnfMINSET sta s,s) (A,s)

⊢ ∀P. (∀x. sta x ⊆ bnfMINSET sta s ∧ (∀y. y ∈ sta x ⇒ P y) ⇒ P (s x)) ⇒
      ∀x. x ∈ bnfMINSET sta s ⇒ P x

⊢ ∀P. (∀x. (∀y. y ∈ sta x ⇒ y ∈ bnfMINSET sta s ∧ P y) ⇒ P (s x)) ⇒
      ∀x. x ∈ bnfMINSET sta s ⇒ P x

⊢ bnfALG sta (bnfMINSET sta s,s)

⊢ bnfMapCong mp sta ∧ bnfHOM mp sta stb h1 (bnfMINSET sta s,s) (B,t) ∧
  bnfHOM mp sta stb h2 (bnfMINSET sta s,s) (B,t) ⇒
  ∀a. a ∈ bnfMINSET sta s ⇒ h1 a = h2 a

⊢ bnfALG sta (bnfMKALG sta p)

⊢ bnfALG sta p ⇒ bnfMKALG sta p = p

⊢ (∀x. rep (abs x) = x) ∧ bnfMapComp mp_ab mp_bc mp_ac ⇒
  bnfMapComp (λf. abs ∘ mp_ab f) (λg. mp_bc g ∘ rep) mp_ac

⊢ (∀x. rep (abs x) = x) ∧ bnfMapComp mp_ab mp_bc mp_ac ⇒
  bnfMapComp mp_ab (λg. abs ∘ mp_bc g) (λg. abs ∘ mp_ac g)

⊢ bnfMapCong mp sta ∧ bnfMapId mp ⇒
  ∀f x. (∀a. a ∈ sta x ⇒ f a = a) ⇒ mp f x = x

⊢ bnfMapComp mp_pn mp_np mp_pp ∧ bnfMapId mp_pp ∧ bnfMapCong mp_pp stp ∧
  bnfNatural mp_pn stp stn ∧ (∀n. abs (rep n) = n) ∧
  (∀p. p ∈ bnfMINSET stp s ⇒ rep (abs p) = p) ∧
  (∀n. rep n ∈ bnfMINSET stp s) ⇒
  ∀P. (∀af. (∀y. y ∈ stn af ⇒ P y) ⇒ P (bnfNCONS mp_np s rep abs af)) ⇒
      ∀n. P n

⊢ bnfMapComp mp_pn mp_np mp_pp ∧ bnfMapId mp_pp ∧ bnfMapCong mp_pp stp ∧
  bnfNatural mp_np stn stp ∧ bnfNatural mp_pn stp stn ∧
  bnfMapComp mp_np mp_pc mp_nc ∧ bnfMapComp mp_pn mp_nc mp_pc ∧
  bnfMapCong mp_pc stp ∧ (∀n. abs (rep n) = n) ∧
  (∀p. p ∈ A ⇒ rep (abs p) = p) ∧ (∀n. rep n ∈ A) ∧ bnfALG stp (A,s) ∧
  (∀t G.
     bnfALG stc (G,t) ⇒
     ∃!h. bnfHOM mp_pc stp stc h (A,s) (G,t) ∧ ∀x. x ∉ A ⇒ h x = ARB) ⇒
  ∀t G.
    bnfALG stc (G,t) ⇒
    ∃!h. bnfHOM mp_nc stn stc h (𝕌(:ξ),bnfNCONS mp_np s rep abs) (G,t)

⊢ bnfMapComp mp_pn mp_np mp_pp ∧ bnfMapId mp_pp ∧ bnfMapCong mp_pp stp ∧
  bnfNatural mp_np stn stp ∧ bnfNatural mp_pn stp stn ∧
  bnfMapComp mp_np mp_pc mp_nc ∧ bnfMapComp mp_pn mp_nc mp_pc ∧
  bnfMapCong mp_pc stp ∧ (∀n. abs (rep n) = n) ∧
  (∀p. p ∈ A ⇒ rep (abs p) = p) ∧ (∀n. rep n ∈ A) ∧ bnfALG stp (A,s) ∧
  (∀t G.
     bnfALG stc (G,t) ⇒
     ∃!h. bnfHOM mp_pc stp stc h (A,s) (G,t) ∧ ∀x. x ∉ A ⇒ h x = ARB) ⇒
  ∀t. ∃!h. ∀af. h (bnfNCONS mp_np s rep abs af) = t (mp_nc h af)

⊢ (∀x. rep (abs x) = x) ∧ bnfNatural mp sta stb ⇒
  bnfNatural (λf. abs ∘ mp f) sta (stb ∘ rep)

⊢ (∀x. rep (abs x) = x) ∧ bnfNatural mp sta stb ⇒
  bnfNatural (λf. mp f ∘ rep) (sta ∘ rep) stb

⊢ bnfNatural mp stc sta ⇒ (∃x. stc x ≠ ∅) ⇒ ∀B. B ≼ bnfFIN sta B

⊢ bnfMapComp mp_nq mp_qn mp_nn ∧ bnfMapComp mp_nq mp_qc mp_nc ∧
  bnfMapId mp_nn ∧ (∀t. ∃!h. ∀af. h (cons af) = t (mp_nq h af)) ∧
  (∀t. ∃!h. ∀af. h (cons af) = t (mp_nn h af)) ⇒
  ∀t. ∃!h. ∀af. h (cons af) = t af (mp_nc h af)

⊢ bnfSUBALG sta A1 A2 ∧ bnfHOM mp sta stb f A2 C ⇒ bnfHOM mp sta stb f A1 C

⊢ preds bd =~ B ∧ s ≼ B ⇒ s ≼ preds bd

⊢ INFINITE B ∧ preds bd =~ B ⇒ ω ≤ bd

⊢ (∀a. abs (rep a) = a) ∧ (∀r. rep (abs r) = r) ⇒ ∀s. s ≼ 𝕌(:ψ) ⇒ s ≼ 𝕌(:ω)

⊢ ∀mp_aa B.
    bnfNatural mp_ba stb sta ∧ bnfNatural mp_ab sta stb ∧
    bnfMapComp mp_ab mp_ba mp_aa ∧ bnfMapId mp_aa ∧ bnfMapCong mp_aa sta ∧
    A ≼ B ∧ bnfALG sta (A,s) ⇒
    ∃B0 s' h j.
      bnfHOM mp_ba stb sta h (B0,s') (A,s) ∧
      bnfHOM mp_ab sta stb j (A,s) (B0,s') ∧ (∀a. a ∈ A ⇒ h (j a) = a) ∧
      ∀b. b ∈ B0 ⇒ j (h b) = b

⊢ (∀C. C ≼ bnfFIN sto C) ⇒
  preds bd ≼ preds (oleast a. preds a =~ bnfFIN sto (preds bd))

⊢ preds a ≼ preds (csuc a)

⊢ ω ≤ bd ∧ (∀x. sta x ≼ preds bd) ⇒ bnfALG sta (bnfKK sta s (csuc bd),s)