Let S, n and f be given.
Assume HnO: n ∈ ω.
Assume Hcard: cardinality_at_most S (ordsucc n).
We prove the intermediate claim HordSucc: ordinal (ordsucc n).
An exact proof term for the current goal is (andEL (ordinal (ordsucc n)) (∃k : set, ordinal k ∧ k ⊆ ordsucc n ∧ equip S k) Hcard).
We prove the intermediate claim Hexk: ∃k : set, ordinal k ∧ k ⊆ ordsucc n ∧ equip S k.
An exact proof term for the current goal is (andER (ordinal (ordsucc n)) (∃k : set, ordinal k ∧ k ⊆ ordsucc n ∧ equip S k) Hcard).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpack: ordinal k ∧ k ⊆ ordsucc n ∧ equip S k.
We prove the intermediate claim HkLeft: ordinal k ∧ k ⊆ ordsucc n.
An exact proof term for the current goal is (andEL (ordinal k ∧ k ⊆ ordsucc n) (equip S k) Hkpack).
We prove the intermediate claim HkOrd: ordinal k.
An exact proof term for the current goal is (andEL (ordinal k) (k ⊆ ordsucc n) HkLeft).
We prove the intermediate claim HkSub: k ⊆ ordsucc n.
An exact proof term for the current goal is (andER (ordinal k) (k ⊆ ordsucc n) HkLeft).
We prove the intermediate claim HeqSk: equip S k.
An exact proof term for the current goal is (andER (ordinal k ∧ k ⊆ ordsucc n) (equip S k) Hkpack).
We prove the intermediate claim HsuccNO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HsuccNOrd: ordinal (ordsucc n).
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (ordsucc n) HsuccNO).
We prove the intermediate claim HkOmega: k ∈ ω.
We prove the intermediate claim HomegaTr: TransSet ω.
An exact proof term for the current goal is (ordinal_TransSet ω omega_ordinal).
We prove the intermediate claim HsuccNSubOmega: ordsucc n ⊆ ω.
An exact proof term for the current goal is (HomegaTr (ordsucc n) HsuccNO).
We prove the intermediate claim Hkn: k ∈ (ordsucc n) ∨ k = ordsucc n.
Apply (ordinal_trichotomy_or_impred k (ordsucc n) HkOrd HsuccNOrd (k ∈ ordsucc n ∨ k = ordsucc n)) to the current goal.
Assume HkIn: k ∈ ordsucc n.
An exact proof term for the current goal is (orIL (k ∈ ordsucc n) (k = ordsucc n) HkIn).
Assume HkEq: k = ordsucc n.
An exact proof term for the current goal is (orIR (k ∈ ordsucc n) (k = ordsucc n) HkEq).
Assume HsuccIn: (ordsucc n) ∈ k.
Apply FalseE to the current goal.
We prove the intermediate claim HsuccInSucc: (ordsucc n) ∈ (ordsucc n).
An exact proof term for the current goal is (HkSub (ordsucc n) HsuccIn).
An exact proof term for the current goal is ((In_irref (ordsucc n)) HsuccInSucc).
Apply Hkn to the current goal.
Assume HkIn: k ∈ ordsucc n.
An exact proof term for the current goal is (HsuccNSubOmega k HkIn).
Assume HkEq: k = ordsucc n.
rewrite the current goal using HkEq (from left to right).
An exact proof term for the current goal is HsuccNO.
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (omega_nat_p k HkOmega).
Apply HeqSk to the current goal.
Let g be given.
Assume Hbij: bij S k g.
We prove the intermediate claim Hginj: inj S k g.
An exact proof term for the current goal is (bij_inj S k g Hbij).
Set Img to be the term {f x|x ∈ S}.
Set idx to be the term (λy : set ⇒ Eps_i (λa : set ⇒ a ∈ k ∧ ∃x : set, x ∈ S ∧ a = g x ∧ f x = y)).
We prove the intermediate claim HidxInj: inj Img k idx.
We prove the intermediate claim Hcod: ∀y ∈ Img, idx y ∈ k.
Let y be given.
Assume Hy: y ∈ Img.
We prove the intermediate claim Hexx: ∃x : set, x ∈ S ∧ y = f x.
Apply (ReplE_impred S (λx0 : set ⇒ f x0) y Hy (∃x : set, x ∈ S ∧ y = f x)) to the current goal.
Let x0 be given.
Assume Hx0: x0 ∈ S.
Assume Hyeq: y = f x0.
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx0.
An exact proof term for the current goal is Hyeq.
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair: x ∈ S ∧ y = f x.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (y = f x) Hxpair).
We prove the intermediate claim Hyeq: y = f x.
An exact proof term for the current goal is (andER (x ∈ S) (y = f x) Hxpair).
We prove the intermediate claim Hgcod: ∀u ∈ S, g u ∈ k.
An exact proof term for the current goal is (andEL (∀u ∈ S, g u ∈ k) (∀u v ∈ S, g u = g v → u = v) Hginj).
We prove the intermediate claim Hexa: ∃a : set, a ∈ k ∧ ∃x1 : set, x1 ∈ S ∧ a = g x1 ∧ f x1 = y.
We use (g x) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (Hgcod x HxS).
We use x to witness the existential quantifier.
We will prove (x ∈ S ∧ g x = g x) ∧ f x = y.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HxS.
Use reflexivity.
rewrite the current goal using Hyeq (from right to left).
Use reflexivity.
We prove the intermediate claim HidxP: (λa : set ⇒ a ∈ k ∧ ∃x1 : set, x1 ∈ S ∧ a = g x1 ∧ f x1 = y) (idx y).
An exact proof term for the current goal is (Eps_i_ex (λa : set ⇒ a ∈ k ∧ ∃x1 : set, x1 ∈ S ∧ a = g x1 ∧ f x1 = y) Hexa).
An exact proof term for the current goal is (andEL (idx y ∈ k) (∃x1 : set, x1 ∈ S ∧ idx y = g x1 ∧ f x1 = y) HidxP).
We prove the intermediate claim Hinj2: ∀y1 y2 ∈ Img, idx y1 = idx y2 → y1 = y2.
Let y1 be given.
Assume Hy1: y1 ∈ Img.
Let y2 be given.
Assume Hy2: y2 ∈ Img.
Assume HeqIdx: idx y1 = idx y2.
We prove the intermediate claim Hex1: ∃x1 : set, x1 ∈ S ∧ idx y1 = g x1 ∧ f x1 = y1.
We prove the intermediate claim Hexx: ∃x : set, x ∈ S ∧ y1 = f x.
Apply (ReplE_impred S (λx0 : set ⇒ f x0) y1 Hy1 (∃x : set, x ∈ S ∧ y1 = f x)) to the current goal.
Let x0 be given.
Assume Hx0: x0 ∈ S.
Assume Hyeq: y1 = f x0.
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx0.
An exact proof term for the current goal is Hyeq.
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair: x ∈ S ∧ y1 = f x.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (y1 = f x) Hxpair).
We prove the intermediate claim Hyeq: y1 = f x.
An exact proof term for the current goal is (andER (x ∈ S) (y1 = f x) Hxpair).
We prove the intermediate claim Hgcod: ∀u ∈ S, g u ∈ k.
An exact proof term for the current goal is (andEL (∀u ∈ S, g u ∈ k) (∀u v ∈ S, g u = g v → u = v) Hginj).
We prove the intermediate claim Hexa: ∃a : set, a ∈ k ∧ ∃x1 : set, x1 ∈ S ∧ a = g x1 ∧ f x1 = y1.
We use (g x) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (Hgcod x HxS).
We use x to witness the existential quantifier.
We will prove (x ∈ S ∧ g x = g x) ∧ f x = y1.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HxS.
Use reflexivity.
rewrite the current goal using Hyeq (from right to left).
Use reflexivity.
We prove the intermediate claim HidxP: idx y1 ∈ k ∧ ∃x1 : set, x1 ∈ S ∧ idx y1 = g x1 ∧ f x1 = y1.
An exact proof term for the current goal is (Eps_i_ex (λa : set ⇒ a ∈ k ∧ ∃x1 : set, x1 ∈ S ∧ a = g x1 ∧ f x1 = y1) Hexa).
An exact proof term for the current goal is (andER (idx y1 ∈ k) (∃x1 : set, x1 ∈ S ∧ idx y1 = g x1 ∧ f x1 = y1) HidxP).
We prove the intermediate claim Hex2: ∃x2 : set, x2 ∈ S ∧ idx y2 = g x2 ∧ f x2 = y2.
We prove the intermediate claim Hexx: ∃x : set, x ∈ S ∧ y2 = f x.
Apply (ReplE_impred S (λx0 : set ⇒ f x0) y2 Hy2 (∃x : set, x ∈ S ∧ y2 = f x)) to the current goal.
Let x0 be given.
Assume Hx0: x0 ∈ S.
Assume Hyeq: y2 = f x0.
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx0.
An exact proof term for the current goal is Hyeq.
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair: x ∈ S ∧ y2 = f x.
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is (andEL (x ∈ S) (y2 = f x) Hxpair).
We prove the intermediate claim Hyeq: y2 = f x.
An exact proof term for the current goal is (andER (x ∈ S) (y2 = f x) Hxpair).
We prove the intermediate claim Hgcod: ∀u ∈ S, g u ∈ k.
An exact proof term for the current goal is (andEL (∀u ∈ S, g u ∈ k) (∀u v ∈ S, g u = g v → u = v) Hginj).
We prove the intermediate claim Hexa: ∃a : set, a ∈ k ∧ ∃x2 : set, x2 ∈ S ∧ a = g x2 ∧ f x2 = y2.
We use (g x) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (Hgcod x HxS).
We use x to witness the existential quantifier.
We will prove (x ∈ S ∧ g x = g x) ∧ f x = y2.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HxS.
Use reflexivity.
rewrite the current goal using Hyeq (from right to left).
Use reflexivity.
We prove the intermediate claim HidxP: idx y2 ∈ k ∧ ∃x2 : set, x2 ∈ S ∧ idx y2 = g x2 ∧ f x2 = y2.
An exact proof term for the current goal is (Eps_i_ex (λa : set ⇒ a ∈ k ∧ ∃x2 : set, x2 ∈ S ∧ a = g x2 ∧ f x2 = y2) Hexa).
An exact proof term for the current goal is (andER (idx y2 ∈ k) (∃x2 : set, x2 ∈ S ∧ idx y2 = g x2 ∧ f x2 = y2) HidxP).
Apply Hex1 to the current goal.
Let x1 be given.
Assume Hx1pack: x1 ∈ S ∧ idx y1 = g x1 ∧ f x1 = y1.
Apply Hex2 to the current goal.
Let x2 be given.
Assume Hx2pack: x2 ∈ S ∧ idx y2 = g x2 ∧ f x2 = y2.
We prove the intermediate claim Hx1pair: x1 ∈ S ∧ idx y1 = g x1.
An exact proof term for the current goal is (andEL (x1 ∈ S ∧ idx y1 = g x1) (f x1 = y1) Hx1pack).
We prove the intermediate claim Hx2pair: x2 ∈ S ∧ idx y2 = g x2.
An exact proof term for the current goal is (andEL (x2 ∈ S ∧ idx y2 = g x2) (f x2 = y2) Hx2pack).
We prove the intermediate claim Hy1eq: f x1 = y1.
An exact proof term for the current goal is (andER (x1 ∈ S ∧ idx y1 = g x1) (f x1 = y1) Hx1pack).
We prove the intermediate claim Hy2eq: f x2 = y2.
An exact proof term for the current goal is (andER (x2 ∈ S ∧ idx y2 = g x2) (f x2 = y2) Hx2pack).
We prove the intermediate claim Hx1S: x1 ∈ S.
An exact proof term for the current goal is (andEL (x1 ∈ S) (idx y1 = g x1) Hx1pair).
We prove the intermediate claim Hx2S: x2 ∈ S.
An exact proof term for the current goal is (andEL (x2 ∈ S) (idx y2 = g x2) Hx2pair).
We prove the intermediate claim Hidx1: idx y1 = g x1.
An exact proof term for the current goal is (andER (x1 ∈ S) (idx y1 = g x1) Hx1pair).
We prove the intermediate claim Hidx2: idx y2 = g x2.
An exact proof term for the current goal is (andER (x2 ∈ S) (idx y2 = g x2) Hx2pair).
We prove the intermediate claim HgInj: ∀u v ∈ S, g u = g v → u = v.
An exact proof term for the current goal is (andER (∀u ∈ S, g u ∈ k) (∀u v ∈ S, g u = g v → u = v) Hginj).
We prove the intermediate claim Hgx: g x1 = g x2.
rewrite the current goal using Hidx1 (from right to left).
rewrite the current goal using Hidx2 (from right to left).
An exact proof term for the current goal is HeqIdx.
We prove the intermediate claim Hxeq: x1 = x2.
An exact proof term for the current goal is (HgInj x1 Hx1S x2 Hx2S Hgx).
rewrite the current goal using Hy1eq (from right to left).
rewrite the current goal using Hy2eq (from right to left).
rewrite the current goal using Hxeq (from left to right).
Use reflexivity.
An exact proof term for the current goal is (andI (∀y ∈ Img, idx y ∈ k) (∀y1 y2 ∈ Img, idx y1 = idx y2 → y1 = y2) Hcod Hinj2).
Set ImgIdx to be the term {idx y|y ∈ Img}.
We prove the intermediate claim HeqImg: equip Img ImgIdx.
An exact proof term for the current goal is (inj_equip_image Img k idx HidxInj).
We prove the intermediate claim HImgIdxSub: ImgIdx ⊆ k.
Let a be given.
Assume Ha: a ∈ ImgIdx.
Apply (ReplE_impred Img (λy0 : set ⇒ idx y0) a Ha (a ∈ k)) to the current goal.
Let y0 be given.
Assume Hy0: y0 ∈ Img.
Assume HaEq: a = idx y0.
We prove the intermediate claim HidxCod: ∀y ∈ Img, idx y ∈ k.
An exact proof term for the current goal is (andEL (∀y ∈ Img, idx y ∈ k) (∀y1 y2 ∈ Img, idx y1 = idx y2 → y1 = y2) HidxInj).
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is (HidxCod y0 Hy0).
We prove the intermediate claim Hexm: ∃m : set, nat_p m ∧ (m ⊆ k ∧ equip ImgIdx m).
An exact proof term for the current goal is (finite_ordinal_subset_equip_subordinal k ImgIdx HkNat HImgIdxSub).
Apply Hexm to the current goal.
Let m be given.
Assume HmPack: nat_p m ∧ (m ⊆ k ∧ equip ImgIdx m).
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (andEL (nat_p m) (m ⊆ k ∧ equip ImgIdx m) HmPack).
We prove the intermediate claim HmTail: m ⊆ k ∧ equip ImgIdx m.
An exact proof term for the current goal is (andER (nat_p m) (m ⊆ k ∧ equip ImgIdx m) HmPack).
We prove the intermediate claim HmSubk: m ⊆ k.
An exact proof term for the current goal is (andEL (m ⊆ k) (equip ImgIdx m) HmTail).
We prove the intermediate claim HeqImgIdxm: equip ImgIdx m.
An exact proof term for the current goal is (andER (m ⊆ k) (equip ImgIdx m) HmTail).
We prove the intermediate claim HeqImgm: equip Img m.
An exact proof term for the current goal is (equip_tra Img ImgIdx m HeqImg HeqImgIdxm).
We prove the intermediate claim HmSubSucc: m ⊆ ordsucc n.
An exact proof term for the current goal is (Subq_tra m k (ordsucc n) HmSubk HkSub).
We will prove cardinality_at_most Img (ordsucc n).
We will prove ordinal (ordsucc n) ∧ ∃k0 : set, ordinal k0 ∧ k0 ⊆ ordsucc n ∧ equip Img k0.
Apply andI to the current goal.
An exact proof term for the current goal is HordSucc.
We use m to witness the existential quantifier.
We will prove (ordinal m ∧ m ⊆ ordsucc n) ∧ equip Img m.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_ordinal m HmNat).
An exact proof term for the current goal is HmSubSucc.
An exact proof term for the current goal is HeqImgm.
∎