Let J, le and F be given.
Assume Hdir: directed_set J le.
Assume HFin: finite F.
Assume HFsubJ: F ⊆ J.
We will prove ∃k : set, k ∈ J ∧ ∀i : set, i ∈ F → (i,k) ∈ le.
Set P to be the term λF0 : set ⇒ F0 ⊆ J → ∃k : set, k ∈ J ∧ ∀i : set, i ∈ F0 → (i,k) ∈ le.
We prove the intermediate claim Hbase: P Empty.
We will prove Empty ⊆ J → ∃k : set, k ∈ J ∧ ∀i : set, i ∈ Empty → (i,k) ∈ le.
Assume Hsub: Empty ⊆ J.
We prove the intermediate claim HJne: J ≠ Empty.
An exact proof term for the current goal is (directed_set_nonempty J le Hdir).
We prove the intermediate claim Hexk: ∃k : set, k ∈ J.
An exact proof term for the current goal is (nonempty_has_element J HJne).
Apply Hexk to the current goal.
Let k be given.
Assume HkJ: k ∈ J.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HkJ.
Let i be given.
Assume HiE: i ∈ Empty.
An exact proof term for the current goal is (EmptyE i HiE ((i,k) ∈ le)).
We prove the intermediate claim Hstep: ∀F0 y : set, finite F0 → y ∉ F0 → P F0 → P (F0 ∪ {y}).
Let F0 and y be given.
Assume HFin0: finite F0.
Assume HyNot: y ∉ F0.
Assume IH: P F0.
We will prove P (F0 ∪ {y}).
Assume Hsub: (F0 ∪ {y}) ⊆ J.
We prove the intermediate claim HF0sub: F0 ⊆ J.
Let i be given.
Assume HiF0: i ∈ F0.
An exact proof term for the current goal is (Hsub i (binunionI1 F0 {y} i HiF0)).
We prove the intermediate claim HyJ: y ∈ J.
An exact proof term for the current goal is (Hsub y (binunionI2 F0 {y} y (SingI y))).
We prove the intermediate claim Hexk0: ∃k0 : set, k0 ∈ J ∧ ∀i : set, i ∈ F0 → (i,k0) ∈ le.
An exact proof term for the current goal is (IH HF0sub).
Apply Hexk0 to the current goal.
Let k0 be given.
Assume Hk0pack.
We prove the intermediate claim Hk0J: k0 ∈ J.
An exact proof term for the current goal is (andEL (k0 ∈ J) (∀i : set, i ∈ F0 → (i,k0) ∈ le) Hk0pack).
We prove the intermediate claim Hk0ub: ∀i : set, i ∈ F0 → (i,k0) ∈ le.
An exact proof term for the current goal is (andER (k0 ∈ J) (∀i : set, i ∈ F0 → (i,k0) ∈ le) Hk0pack).
We prove the intermediate claim Hexk: ∃k : set, k ∈ J ∧ (k0,k) ∈ le ∧ (y,k) ∈ le.
An exact proof term for the current goal is (directed_set_upper_bound_property J le Hdir k0 y Hk0J HyJ).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpack.
We prove the intermediate claim HkJ: k ∈ J.
Apply (and3E (k ∈ J) ((k0,k) ∈ le) ((y,k) ∈ le) Hkpack (k ∈ J)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H1.
We prove the intermediate claim Hk0k: (k0,k) ∈ le.
Apply (and3E (k ∈ J) ((k0,k) ∈ le) ((y,k) ∈ le) Hkpack ((k0,k) ∈ le)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H2.
We prove the intermediate claim Hyk: (y,k) ∈ le.
Apply (and3E (k ∈ J) ((k0,k) ∈ le) ((y,k) ∈ le) Hkpack ((y,k) ∈ le)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H3.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HkJ.
Let i be given.
Assume Hi: i ∈ (F0 ∪ {y}).
We will prove (i,k) ∈ le.
Apply (binunionE' F0 {y} i ((i,k) ∈ le)) to the current goal.
Assume HiF0: i ∈ F0.
We prove the intermediate claim Hik0: (i,k0) ∈ le.
An exact proof term for the current goal is (Hk0ub i HiF0).
We prove the intermediate claim Hpo: partial_order_on J le.
An exact proof term for the current goal is (directed_set_partial_order J le Hdir).
We prove the intermediate claim Htr: ∀a b c : set, a ∈ J → b ∈ J → c ∈ J → (a,b) ∈ le → (b,c) ∈ le → (a,c) ∈ le.
An exact proof term for the current goal is (partial_order_on_trans J le Hpo).
An exact proof term for the current goal is (Htr i k0 k (HF0sub i HiF0) Hk0J HkJ Hik0 Hk0k).
Assume Hiy: i ∈ {y}.
We prove the intermediate claim Hieq: i = y.
An exact proof term for the current goal is (SingE y i Hiy).
rewrite the current goal using Hieq (from left to right).
An exact proof term for the current goal is Hyk.
An exact proof term for the current goal is Hi.
We prove the intermediate claim Hall: ∀F0 : set, finite F0 → P F0.
An exact proof term for the current goal is (finite_ind P Hbase Hstep).
We prove the intermediate claim Hspec: P F.
An exact proof term for the current goal is (Hall F HFin).
An exact proof term for the current goal is (Hspec HFsubJ).
∎