Let S1, S2 and n be given.
Assume HnO: n ∈ ω.
Assume HSsub: S1 ⊆ S2.
Assume Hcard2: cardinality_at_most S2 n.
We prove the intermediate claim HnOrd: ordinal n.
An exact proof term for the current goal is (andEL (ordinal n) (∃k : set, ordinal k ∧ k ⊆ n ∧ equip S2 k) Hcard2).
We prove the intermediate claim Hexk: ∃k : set, ordinal k ∧ k ⊆ n ∧ equip S2 k.
An exact proof term for the current goal is (andER (ordinal n) (∃k : set, ordinal k ∧ k ⊆ n ∧ equip S2 k) Hcard2).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpack: ordinal k ∧ k ⊆ n ∧ equip S2 k.
We prove the intermediate claim HkLeft: ordinal k ∧ k ⊆ n.
An exact proof term for the current goal is (andEL (ordinal k ∧ k ⊆ n) (equip S2 k) Hkpack).
We prove the intermediate claim HeqS2k: equip S2 k.
An exact proof term for the current goal is (andER (ordinal k ∧ k ⊆ n) (equip S2 k) Hkpack).
We prove the intermediate claim HkOrd: ordinal k.
An exact proof term for the current goal is (andEL (ordinal k) (k ⊆ n) HkLeft).
We prove the intermediate claim HkSubn: k ⊆ n.
An exact proof term for the current goal is (andER (ordinal k) (k ⊆ n) HkLeft).
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 HnSubOmega: n ⊆ ω.
An exact proof term for the current goal is (HomegaTr n HnO).
We prove the intermediate claim Hkn: k ∈ n ∨ k = n.
Apply (ordinal_trichotomy_or_impred k n HkOrd HnOrd (k ∈ n ∨ k = n)) to the current goal.
Assume HkInN: k ∈ n.
An exact proof term for the current goal is (orIL (k ∈ n) (k = n) HkInN).
Assume HkEq: k = n.
An exact proof term for the current goal is (orIR (k ∈ n) (k = n) HkEq).
Assume HnInk: n ∈ k.
Apply FalseE to the current goal.
We prove the intermediate claim HnInN: n ∈ n.
An exact proof term for the current goal is (HkSubn n HnInk).
An exact proof term for the current goal is ((In_irref n) HnInN).
Apply Hkn to the current goal.
Assume HkInN: k ∈ n.
An exact proof term for the current goal is (HnSubOmega k HkInN).
Assume HkEq: k = n.
rewrite the current goal using HkEq (from left to right).
An exact proof term for the current goal is HnO.
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (omega_nat_p k HkOmega).
Apply HeqS2k to the current goal.
Let f be given.
Assume Hbij: bij S2 k f.
We prove the intermediate claim HfInj: inj S2 k f.
An exact proof term for the current goal is (bij_inj S2 k f Hbij).
We prove the intermediate claim Hfk: inj S1 k (λx : set ⇒ f x).
We will prove inj S1 k (λx : set ⇒ f x).
We will prove (∀u ∈ S1, f u ∈ k) ∧ (∀u v ∈ S1, f u = f v → u = v).
Apply andI to the current goal.
Let u be given.
Assume Hu1: u ∈ S1.
We prove the intermediate claim Hu2: u ∈ S2.
An exact proof term for the current goal is (HSsub u Hu1).
We prove the intermediate claim Hcod: ∀x ∈ S2, f x ∈ k.
An exact proof term for the current goal is (andEL (∀x ∈ S2, f x ∈ k) (∀x z ∈ S2, f x = f z → x = z) HfInj).
An exact proof term for the current goal is (Hcod u Hu2).
Let u be given.
Assume Hu1: u ∈ S1.
Let v be given.
Assume Hv1: v ∈ S1.
Assume Heq: f u = f v.
We prove the intermediate claim Hu2: u ∈ S2.
An exact proof term for the current goal is (HSsub u Hu1).
We prove the intermediate claim Hv2: v ∈ S2.
An exact proof term for the current goal is (HSsub v Hv1).
We prove the intermediate claim Hinj2: ∀x z ∈ S2, f x = f z → x = z.
An exact proof term for the current goal is (andER (∀x ∈ S2, f x ∈ k) (∀x z ∈ S2, f x = f z → x = z) HfInj).
An exact proof term for the current goal is (Hinj2 u Hu2 v Hv2 Heq).
Set Img to be the term {f x|x ∈ S1}.
We prove the intermediate claim HeqS1Img: equip S1 Img.
An exact proof term for the current goal is (inj_equip_image S1 k (λx : set ⇒ f x) Hfk).
We prove the intermediate claim HImgSubk: Img ⊆ k.
Let y be given.
Assume Hy: y ∈ Img.
Apply (ReplE_impred S1 (λx0 : set ⇒ f x0) y Hy (y ∈ k)) to the current goal.
Let x be given.
Assume Hx1: x ∈ S1.
Assume Hyeq: y = f x.
We prove the intermediate claim Hcod: ∀u ∈ S1, f u ∈ k.
An exact proof term for the current goal is (andEL (∀u ∈ S1, f u ∈ k) (∀u v ∈ S1, f u = f v → u = v) Hfk).
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is (Hcod x Hx1).
We prove the intermediate claim Hexm: ∃m : set, nat_p m ∧ (m ⊆ k ∧ equip Img m).
An exact proof term for the current goal is (finite_ordinal_subset_equip_subordinal k Img HkNat HImgSubk).
Apply Hexm to the current goal.
Let m be given.
Assume HmPack: nat_p m ∧ (m ⊆ k ∧ equip Img 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 Img m) HmPack).
We prove the intermediate claim HmTail: m ⊆ k ∧ equip Img m.
An exact proof term for the current goal is (andER (nat_p m) (m ⊆ k ∧ equip Img m) HmPack).
We prove the intermediate claim HmSubk: m ⊆ k.
An exact proof term for the current goal is (andEL (m ⊆ k) (equip Img m) HmTail).
We prove the intermediate claim HeqImgm: equip Img m.
An exact proof term for the current goal is (andER (m ⊆ k) (equip Img m) HmTail).
We prove the intermediate claim HeqS1m: equip S1 m.
An exact proof term for the current goal is (equip_tra S1 Img m HeqS1Img HeqImgm).
We prove the intermediate claim HmSubn: m ⊆ n.
An exact proof term for the current goal is (Subq_tra m k n HmSubk HkSubn).
We will prove cardinality_at_most S1 n.
We will prove ordinal n ∧ ∃k : set, ordinal k ∧ k ⊆ n ∧ equip S1 k.
Apply andI to the current goal.
An exact proof term for the current goal is HnOrd.
We use m to witness the existential quantifier.
We will prove (ordinal m ∧ m ⊆ n) ∧ equip S1 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 HmSubn.
An exact proof term for the current goal is HeqS1m.
∎