Let F be given.
Assume HFsub: F ⊆ ω.
Assume HFfin: finite F.
We will prove ∃n ∈ ω, ∀m ∈ F, m ∈ n.
We prove the intermediate claim Hp0: (Empty ⊆ ω → ∃n ∈ ω, ∀m ∈ Empty, m ∈ n).
Assume Hsub0: Empty ⊆ ω.
We will prove ∃n ∈ ω, ∀m ∈ Empty, m ∈ n.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Let m be given.
Assume Hm: m ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE m Hm).
We prove the intermediate claim Hpstep: ∀A y, finite A → y ∉ A → (A ⊆ ω → ∃n ∈ ω, ∀m ∈ A, m ∈ n) → (A ∪ {y} ⊆ ω → ∃n0 ∈ ω, ∀m : set, m ∈ A ∪ {y} → m ∈ n0).
Let A and y be given.
Assume HAfin: finite A.
Assume HyA: y ∉ A.
Assume HpA: (A ⊆ ω → ∃n ∈ ω, ∀m ∈ A, m ∈ n).
Assume HsubAy: A ∪ {y} ⊆ ω.
We prove the intermediate claim HsubA: A ⊆ ω.
An exact proof term for the current goal is (Subq_tra A (A ∪ {y}) ω (binunion_Subq_1 A {y}) HsubAy).
We prove the intermediate claim Hexn: ∃n ∈ ω, ∀m ∈ A, m ∈ n.
An exact proof term for the current goal is (HpA HsubA).
Apply Hexn to the current goal.
Let n be given.
Assume Hnand.
We prove the intermediate claim Hn: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (∀m ∈ A, m ∈ n) Hnand).
We prove the intermediate claim Hnprop: ∀m ∈ A, m ∈ n.
An exact proof term for the current goal is (andER (n ∈ ω) (∀m ∈ A, m ∈ n) Hnand).
We will prove ∃n0 ∈ ω, ∀m : set, m ∈ A ∪ {y} → m ∈ n0.
We prove the intermediate claim Hy_in_union: y ∈ A ∪ {y}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (SingI y).
We prove the intermediate claim Hy_omega: y ∈ ω.
An exact proof term for the current goal is (HsubAy y Hy_in_union).
We prove the intermediate claim Hysucc_omega: ordsucc y ∈ ω.
An exact proof term for the current goal is (omega_ordsucc y Hy_omega).
We prove the intermediate claim Hn_union_omega: n ∪ ordsucc y ∈ ω.
An exact proof term for the current goal is (omega_binunion n (ordsucc y) Hn Hysucc_omega).
Set n0 to be the term ordsucc (n ∪ ordsucc y).
We prove the intermediate claim Hn0_omega: n0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (n ∪ ordsucc y) Hn_union_omega).
We use n0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn0_omega.
Let m be given.
Assume Hm: m ∈ A ∪ {y}.
We will prove m ∈ n0.
Apply (binunionE A {y} m Hm) to the current goal.
Assume HmA: m ∈ A.
We prove the intermediate claim Hmn: m ∈ n.
An exact proof term for the current goal is (Hnprop m HmA).
We prove the intermediate claim HmnU: m ∈ n ∪ ordsucc y.
An exact proof term for the current goal is (binunionI1 n (ordsucc y) m Hmn).
An exact proof term for the current goal is (ordsuccI1 (n ∪ ordsucc y) m HmnU).
Assume HmY: m ∈ {y}.
We prove the intermediate claim Hmy: m = y.
An exact proof term for the current goal is (SingE y m HmY).
rewrite the current goal using Hmy (from left to right).
We prove the intermediate claim Hy_in_succ: y ∈ ordsucc y.
An exact proof term for the current goal is (ordsuccI2 y).
We prove the intermediate claim Hy_in_U: y ∈ n ∪ ordsucc y.
An exact proof term for the current goal is (binunionI2 n (ordsucc y) y Hy_in_succ).
An exact proof term for the current goal is (ordsuccI1 (n ∪ ordsucc y) y Hy_in_U).
We prove the intermediate claim HpF: (F ⊆ ω → ∃n ∈ ω, ∀m ∈ F, m ∈ n).
An exact proof term for the current goal is (finite_ind (λA ⇒ A ⊆ ω → ∃n ∈ ω, ∀m ∈ A, m ∈ n) Hp0 Hpstep F HFfin).
An exact proof term for the current goal is (HpF HFsub).
∎