We will prove infinite K_set.
We prove the intermediate claim Hatleast: ∃f : set → set, inj ω K_set f.
We use (λn : set ⇒ inv_nat (ordsucc n)) to witness the existential quantifier.
We will prove inj ω K_set (λn : set ⇒ inv_nat (ordsucc n)).
We will prove (∀u ∈ ω, inv_nat (ordsucc u) ∈ K_set) ∧ (∀u v ∈ ω, inv_nat (ordsucc u) = inv_nat (ordsucc v) → u = v).
Apply andI to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
We will prove inv_nat (ordsucc n) ∈ K_set.
We prove the intermediate claim HsuccO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n Hn).
We prove the intermediate claim HsuccNot0: ordsucc n ∉ {0}.
Assume Hmem: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) Hmem).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim HsuccIn: ordsucc n ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc n) HsuccO HsuccNot0).
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λk : set ⇒ inv_nat k) (ordsucc n) HsuccIn).
Let n be given.
Assume Hn: n ∈ ω.
Let m be given.
Assume Hm: m ∈ ω.
Assume Heq: inv_nat (ordsucc n) = inv_nat (ordsucc m).
An exact proof term for the current goal is (inv_nat_ordsucc_inj n m Hn Hm Heq).
An exact proof term for the current goal is (atleastp_omega_infinite K_set Hatleast).
∎