Let Fam, Y and n be given.
Assume HnO: n ∈ ω.
Assume Hcard: cardinality_at_most Fam (ordsucc n).
We prove the intermediate claim HordN: ordinal (ordsucc n).
An exact proof term for the current goal is (andEL (ordinal (ordsucc n)) (∃k : set, ordinal k ∧ k ⊆ ordsucc n ∧ equip Fam k) Hcard).
We prove the intermediate claim Hexk: ∃k : set, ordinal k ∧ k ⊆ ordsucc n ∧ equip Fam k.
An exact proof term for the current goal is (andER (ordinal (ordsucc n)) (∃k : set, ordinal k ∧ k ⊆ ordsucc n ∧ equip Fam k) Hcard).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpack: ordinal k ∧ k ⊆ ordsucc n ∧ equip Fam 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 Fam k) Hkpack).
We prove the intermediate claim HeqFamk: equip Fam k.
An exact proof term for the current goal is (andER (ordinal k ∧ k ⊆ ordsucc n) (equip Fam 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 HsuccNO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
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 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 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 HeqFamk to the current goal.
Let f be given.
Assume Hbij: bij Fam k f.
We prove the intermediate claim HfInj: inj Fam k f.
An exact proof term for the current goal is (bij_inj Fam k f Hbij).
Set idx to be the term (λW : set ⇒ Eps_i (λa : set ⇒ a ∈ k ∧ ∃U : set, U ∈ Fam ∧ a = f U ∧ U ∩ Y = W)).
We prove the intermediate claim HidxInj: inj (restrict_family_to_subspace Fam Y) k idx.
We will prove inj (restrict_family_to_subspace Fam Y) k idx.
We will prove (∀W ∈ restrict_family_to_subspace Fam Y, idx W ∈ k) ∧ (∀W1 W2 ∈ restrict_family_to_subspace Fam Y, idx W1 = idx W2 → W1 = W2).
Apply andI to the current goal.
Let W be given.
Assume HW: W ∈ restrict_family_to_subspace Fam Y.
We prove the intermediate claim HexU: ∃U : set, U ∈ Fam ∧ W = U ∩ Y.
Apply (ReplE_impred Fam (λU0 : set ⇒ U0 ∩ Y) W HW (∃U : set, U ∈ Fam ∧ W = U ∩ Y)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Fam.
Assume HWeq: W = U0 ∩ Y.
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU0.
An exact proof term for the current goal is HWeq.
Apply HexU to the current goal.
Let U be given.
Assume HU: U ∈ Fam ∧ W = U ∩ Y.
We prove the intermediate claim HUFam: U ∈ Fam.
An exact proof term for the current goal is (andEL (U ∈ Fam) (W = U ∩ Y) HU).
We prove the intermediate claim HWeq: W = U ∩ Y.
An exact proof term for the current goal is (andER (U ∈ Fam) (W = U ∩ Y) HU).
We prove the intermediate claim HfCod: ∀x ∈ Fam, f x ∈ k.
An exact proof term for the current goal is (andEL (∀x ∈ Fam, f x ∈ k) (∀x z ∈ Fam, f x = f z → x = z) HfInj).
We prove the intermediate claim Hexa: ∃a : set, a ∈ k ∧ ∃U0 : set, U0 ∈ Fam ∧ a = f U0 ∧ U0 ∩ Y = W.
We use (f U) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HfCod U HUFam).
We use U to witness the existential quantifier.
We will prove (U ∈ Fam ∧ (f U = f U)) ∧ U ∩ Y = W.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUFam.
Use reflexivity.
rewrite the current goal using HWeq (from right to left).
Use reflexivity.
We prove the intermediate claim HidxP: (λa : set ⇒ a ∈ k ∧ ∃U0 : set, U0 ∈ Fam ∧ a = f U0 ∧ U0 ∩ Y = W) (idx W).
An exact proof term for the current goal is (Eps_i_ex (λa : set ⇒ a ∈ k ∧ ∃U0 : set, U0 ∈ Fam ∧ a = f U0 ∧ U0 ∩ Y = W) Hexa).
An exact proof term for the current goal is (andEL (idx W ∈ k) (∃U0 : set, U0 ∈ Fam ∧ idx W = f U0 ∧ U0 ∩ Y = W) HidxP).
Let W1 be given.
Assume HW1: W1 ∈ restrict_family_to_subspace Fam Y.
Let W2 be given.
Assume HW2: W2 ∈ restrict_family_to_subspace Fam Y.
Assume HeqIdx: idx W1 = idx W2.
We prove the intermediate claim HexU1: ∃U : set, U ∈ Fam ∧ idx W1 = f U ∧ U ∩ Y = W1.
We prove the intermediate claim HexU0: ∃U0 : set, U0 ∈ Fam ∧ W1 = U0 ∩ Y.
Apply (ReplE_impred Fam (λU0 : set ⇒ U0 ∩ Y) W1 HW1 (∃U0 : set, U0 ∈ Fam ∧ W1 = U0 ∩ Y)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Fam.
Assume HWeq: W1 = U0 ∩ Y.
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU0.
An exact proof term for the current goal is HWeq.
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Fam ∧ W1 = U0 ∩ Y.
We prove the intermediate claim HU0Fam: U0 ∈ Fam.
An exact proof term for the current goal is (andEL (U0 ∈ Fam) (W1 = U0 ∩ Y) HU0).
We prove the intermediate claim HW1eq: W1 = U0 ∩ Y.
An exact proof term for the current goal is (andER (U0 ∈ Fam) (W1 = U0 ∩ Y) HU0).
We prove the intermediate claim HfCod: ∀x ∈ Fam, f x ∈ k.
An exact proof term for the current goal is (andEL (∀x ∈ Fam, f x ∈ k) (∀x z ∈ Fam, f x = f z → x = z) HfInj).
We prove the intermediate claim Hexa: ∃a : set, a ∈ k ∧ ∃U : set, U ∈ Fam ∧ a = f U ∧ U ∩ Y = W1.
We use (f U0) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HfCod U0 HU0Fam).
We use U0 to witness the existential quantifier.
We will prove (U0 ∈ Fam ∧ (f U0 = f U0)) ∧ U0 ∩ Y = W1.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU0Fam.
Use reflexivity.
rewrite the current goal using HW1eq (from right to left).
Use reflexivity.
We prove the intermediate claim HidxP: idx W1 ∈ k ∧ ∃U : set, U ∈ Fam ∧ idx W1 = f U ∧ U ∩ Y = W1.
An exact proof term for the current goal is (Eps_i_ex (λa : set ⇒ a ∈ k ∧ ∃U : set, U ∈ Fam ∧ a = f U ∧ U ∩ Y = W1) Hexa).
An exact proof term for the current goal is (andER (idx W1 ∈ k) (∃U : set, U ∈ Fam ∧ idx W1 = f U ∧ U ∩ Y = W1) HidxP).
We prove the intermediate claim HexU2: ∃U : set, U ∈ Fam ∧ idx W2 = f U ∧ U ∩ Y = W2.
We prove the intermediate claim HexU0: ∃U0 : set, U0 ∈ Fam ∧ W2 = U0 ∩ Y.
Apply (ReplE_impred Fam (λU0 : set ⇒ U0 ∩ Y) W2 HW2 (∃U0 : set, U0 ∈ Fam ∧ W2 = U0 ∩ Y)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Fam.
Assume HWeq: W2 = U0 ∩ Y.
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU0.
An exact proof term for the current goal is HWeq.
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Fam ∧ W2 = U0 ∩ Y.
We prove the intermediate claim HU0Fam: U0 ∈ Fam.
An exact proof term for the current goal is (andEL (U0 ∈ Fam) (W2 = U0 ∩ Y) HU0).
We prove the intermediate claim HW2eq: W2 = U0 ∩ Y.
An exact proof term for the current goal is (andER (U0 ∈ Fam) (W2 = U0 ∩ Y) HU0).
We prove the intermediate claim HfCod: ∀x ∈ Fam, f x ∈ k.
An exact proof term for the current goal is (andEL (∀x ∈ Fam, f x ∈ k) (∀x z ∈ Fam, f x = f z → x = z) HfInj).
We prove the intermediate claim Hexa: ∃a : set, a ∈ k ∧ ∃U : set, U ∈ Fam ∧ a = f U ∧ U ∩ Y = W2.
We use (f U0) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HfCod U0 HU0Fam).
We use U0 to witness the existential quantifier.
We will prove (U0 ∈ Fam ∧ (f U0 = f U0)) ∧ U0 ∩ Y = W2.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU0Fam.
Use reflexivity.
rewrite the current goal using HW2eq (from right to left).
Use reflexivity.
We prove the intermediate claim HidxP: idx W2 ∈ k ∧ ∃U : set, U ∈ Fam ∧ idx W2 = f U ∧ U ∩ Y = W2.
An exact proof term for the current goal is (Eps_i_ex (λa : set ⇒ a ∈ k ∧ ∃U : set, U ∈ Fam ∧ a = f U ∧ U ∩ Y = W2) Hexa).
An exact proof term for the current goal is (andER (idx W2 ∈ k) (∃U : set, U ∈ Fam ∧ idx W2 = f U ∧ U ∩ Y = W2) HidxP).
Apply HexU1 to the current goal.
Let U1 be given.
Assume HU1: U1 ∈ Fam ∧ idx W1 = f U1 ∧ U1 ∩ Y = W1.
Apply HexU2 to the current goal.
Let U2 be given.
Assume HU2: U2 ∈ Fam ∧ idx W2 = f U2 ∧ U2 ∩ Y = W2.
We prove the intermediate claim HU1left: (U1 ∈ Fam ∧ idx W1 = f U1).
An exact proof term for the current goal is (andEL (U1 ∈ Fam ∧ idx W1 = f U1) (U1 ∩ Y = W1) HU1).
We prove the intermediate claim HU2left: (U2 ∈ Fam ∧ idx W2 = f U2).
An exact proof term for the current goal is (andEL (U2 ∈ Fam ∧ idx W2 = f U2) (U2 ∩ Y = W2) HU2).
We prove the intermediate claim HU1cap: U1 ∩ Y = W1.
An exact proof term for the current goal is (andER (U1 ∈ Fam ∧ idx W1 = f U1) (U1 ∩ Y = W1) HU1).
We prove the intermediate claim HU2cap: U2 ∩ Y = W2.
An exact proof term for the current goal is (andER (U2 ∈ Fam ∧ idx W2 = f U2) (U2 ∩ Y = W2) HU2).
We prove the intermediate claim HU1Fam: U1 ∈ Fam.
An exact proof term for the current goal is (andEL (U1 ∈ Fam) (idx W1 = f U1) HU1left).
We prove the intermediate claim HU2Fam: U2 ∈ Fam.
An exact proof term for the current goal is (andEL (U2 ∈ Fam) (idx W2 = f U2) HU2left).
We prove the intermediate claim Hidx1: idx W1 = f U1.
An exact proof term for the current goal is (andER (U1 ∈ Fam) (idx W1 = f U1) HU1left).
We prove the intermediate claim Hidx2: idx W2 = f U2.
An exact proof term for the current goal is (andER (U2 ∈ Fam) (idx W2 = f U2) HU2left).
We prove the intermediate claim Hinj2: ∀x z ∈ Fam, f x = f z → x = z.
An exact proof term for the current goal is (andER (∀x ∈ Fam, f x ∈ k) (∀x z ∈ Fam, f x = f z → x = z) HfInj).
We prove the intermediate claim HfEq: f U1 = f U2.
We will prove f U1 = f U2.
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 HUeq: U1 = U2.
An exact proof term for the current goal is (Hinj2 U1 HU1Fam U2 HU2Fam HfEq).
We will prove W1 = W2.
rewrite the current goal using HU1cap (from right to left).
rewrite the current goal using HU2cap (from right to left).
rewrite the current goal using HUeq (from left to right).
Use reflexivity.
Set Img to be the term {idx W|W ∈ restrict_family_to_subspace Fam Y}.
We prove the intermediate claim HeqDomImg: equip (restrict_family_to_subspace Fam Y) Img.
An exact proof term for the current goal is (inj_equip_image (restrict_family_to_subspace Fam Y) k idx HidxInj).
We prove the intermediate claim HImgSubk: Img ⊆ k.
Let a be given.
Assume Ha: a ∈ Img.
Apply (ReplE_impred (restrict_family_to_subspace Fam Y) (λW0 : set ⇒ idx W0) a Ha (a ∈ k)) to the current goal.
Let W be given.
Assume HW: W ∈ restrict_family_to_subspace Fam Y.
Assume Haeq: a = idx W.
We prove the intermediate claim Hcod: ∀W0 ∈ restrict_family_to_subspace Fam Y, idx W0 ∈ k.
An exact proof term for the current goal is (andEL (∀W0 ∈ restrict_family_to_subspace Fam Y, idx W0 ∈ k) (∀W1 W2 ∈ restrict_family_to_subspace Fam Y, idx W1 = idx W2 → W1 = W2) HidxInj).
rewrite the current goal using Haeq (from left to right).
An exact proof term for the current goal is (Hcod W HW).
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 HeqDomm: equip (restrict_family_to_subspace Fam Y) m.
An exact proof term for the current goal is (equip_tra (restrict_family_to_subspace Fam Y) Img m HeqDomImg HeqImgm).
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 (restrict_family_to_subspace Fam Y) (ordsucc n).
We will prove ordinal (ordsucc n) ∧ ∃k0 : set, ordinal k0 ∧ k0 ⊆ ordsucc n ∧ equip (restrict_family_to_subspace Fam Y) k0.
Apply andI to the current goal.
An exact proof term for the current goal is HordN.
We use m to witness the existential quantifier.
We will prove (ordinal m ∧ m ⊆ ordsucc n) ∧ equip (restrict_family_to_subspace Fam Y) 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 HeqDomm.
∎