Let net, sub, J, leJ, K, leK, X, phi and j0 be given.
Assume Hsub: subnet_of_witness net sub J leJ K leK X phi.
Assume Hj0J: j0 ∈ J.
We will prove ∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → (j0,apply_fun phi k) ∈ leJ.
We prove the intermediate claim HdirJ: directed_set J leJ.
An exact proof term for the current goal is (subnet_of_witness_dirJ net sub J leJ K leK X phi Hsub).
We prove the intermediate claim Hcofinal: ∀j : set, j ∈ J → ∃k : set, k ∈ K ∧ (j,apply_fun phi k) ∈ leJ.
An exact proof term for the current goal is (subnet_of_witness_cofinal net sub J leJ K leK X phi Hsub).
We prove the intermediate claim Hmono: ∀i j : set, i ∈ K → j ∈ K → (i,j) ∈ leK → (apply_fun phi i,apply_fun phi j) ∈ leJ.
An exact proof term for the current goal is (subnet_of_witness_mono net sub J leJ K leK X phi Hsub).
We prove the intermediate claim Htotphi: total_function_on phi K J.
An exact proof term for the current goal is (subnet_of_witness_totphi net sub J leJ K leK X phi Hsub).
Apply (Hcofinal j0 Hj0J) to the current goal.
Let k0 be given.
Assume Hk0pair.
We use k0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (k0 ∈ K) ((j0,apply_fun phi k0) ∈ leJ) Hk0pair).
Let k be given.
Assume HkK: k ∈ K.
Assume Hk0k: (k0,k) ∈ leK.
We will prove (j0,apply_fun phi k) ∈ leJ.
We prove the intermediate claim Hj0phi0: (j0,apply_fun phi k0) ∈ leJ.
An exact proof term for the current goal is (andER (k0 ∈ K) ((j0,apply_fun phi k0) ∈ leJ) Hk0pair).
We prove the intermediate claim Hphi0J: apply_fun phi k0 ∈ J.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K J k0 Htotphi (andEL (k0 ∈ K) ((j0,apply_fun phi k0) ∈ leJ) Hk0pair)).
We prove the intermediate claim HphikJ: apply_fun phi k ∈ J.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K J k Htotphi HkK).
We prove the intermediate claim Hphimon: (apply_fun phi k0,apply_fun phi k) ∈ leJ.
An exact proof term for the current goal is (Hmono k0 k (andEL (k0 ∈ K) ((j0,apply_fun phi k0) ∈ leJ) Hk0pair) HkK Hk0k).
An exact proof term for the current goal is (directed_set_trans J leJ HdirJ j0 (apply_fun phi k0) (apply_fun phi k) Hj0J Hphi0J HphikJ Hj0phi0 Hphimon).
∎