Let x be given.

Assume HxX: x ∈ X.

We prove the intermediate claim Hnacc: ¬ (accumulation_point_of_net_on X Tx net J le x).

We prove the intermediate claim Hall: ∀x0 : set, ¬ (accumulation_point_of_net_on X Tx net J le x0).

An exact proof term for the current goal is (not_ex_all_demorgan_i (λx0 : set ⇒ accumulation_point_of_net_on X Tx net J le x0) Hno).

An exact proof term for the current goal is (Hall x).

We prove the intermediate claim HnotForallU: ¬ (∀U : set, U ∈ Tx → x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

Assume HallU: ∀U : set, U ∈ Tx → x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U.

Apply Hnacc to the current goal.

We will prove accumulation_point_of_net_on X Tx net J le x.

An exact proof term for the current goal is (and7I (topology_on X Tx) (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) (x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U) HTx HdirJ Htotnet Hgraphnet Hdomnet HxX HallU).

Apply (not_all_ex_demorgan_i (λU : set ⇒ U ∈ Tx → x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U) HnotForallU) to the current goal.

Let U be given.

Assume HnU: ¬ (U ∈ Tx → x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

We prove the intermediate claim HUa: U ∈ Tx ∧ ¬ (x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

An exact proof term for the current goal is (not_imp (U ∈ Tx) (x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U) HnU).

We prove the intermediate claim HUTx: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (¬ (x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U)) HUa).

We prove the intermediate claim Hn2: ¬ (x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

An exact proof term for the current goal is (andER (U ∈ Tx) (¬ (x ∈ U → ∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U)) HUa).

We prove the intermediate claim Hxb: x ∈ U ∧ ¬ (∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

An exact proof term for the current goal is (not_imp (x ∈ U) (∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U) Hn2).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andEL (x ∈ U) (¬ (∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U)) Hxb).

We prove the intermediate claim HnForallj0: ¬ (∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

An exact proof term for the current goal is (andER (x ∈ U) (¬ (∀j0 : set, j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U)) Hxb).

Apply (not_all_ex_demorgan_i (λj0 : set ⇒ j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U) HnForallj0) to the current goal.

Let j0 be given.

Assume Hnj0: ¬ (j0 ∈ J → ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

We prove the intermediate claim Hj0a: j0 ∈ J ∧ ¬ (∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

An exact proof term for the current goal is (not_imp (j0 ∈ J) (∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U) Hnj0).

We prove the intermediate claim Hj0J: j0 ∈ J.

An exact proof term for the current goal is (andEL (j0 ∈ J) (¬ (∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U)) Hj0a).

We prove the intermediate claim HnExj: ¬ (∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U).

An exact proof term for the current goal is (andER (j0 ∈ J) (¬ (∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U)) Hj0a).

We use U to witness the existential quantifier.

We use j0 to witness the existential quantifier.

We will prove ((U ∈ Tx ∧ x ∈ U) ∧ j0 ∈ J) ∧ ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U).

Apply andI to the current goal.

An exact proof term for the current goal is HUTx.

An exact proof term for the current goal is HxU.

An exact proof term for the current goal is Hj0J.

Let j be given.

Assume HjJ: j ∈ J.

Assume Hj0j: (j0,j) ∈ le.

We will prove ¬ (apply_fun net j ∈ U).

Assume HjU: apply_fun net j ∈ U.

Apply HnExj to the current goal.

We use j to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HjJ.

An exact proof term for the current goal is Hj0j.

An exact proof term for the current goal is HjU.

We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.

An exact proof term for the current goal is (topology_sub_Power X Tx HTx).

We prove the intermediate claim HpickBad: ∀x : set, x ∈ X → Bad x ((pickpair x) 0) ((pickpair x) 1).

Let x be given.

Assume HxX: x ∈ X.

We prove the intermediate claim HexUJ: ∃U j0 : set, Bad x U j0.

An exact proof term for the current goal is (HexBad x HxX).

Apply HexUJ to the current goal.

Let U be given.

Assume Hexj0: ∃j0 : set, Bad x U j0.

Apply Hexj0 to the current goal.

Let j0 be given.

Assume Hbad: Bad x U j0.

We prove the intermediate claim Hbadleft: (U ∈ Tx ∧ x ∈ U) ∧ j0 ∈ J.

An exact proof term for the current goal is (andEL ((U ∈ Tx ∧ x ∈ U) ∧ j0 ∈ J) (∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U)) Hbad).

We prove the intermediate claim HbadUx: U ∈ Tx ∧ x ∈ U.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (j0 ∈ J) Hbadleft).

We prove the intermediate claim HUTx: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HbadUx).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HbadUx).

We prove the intermediate claim Hj0J: j0 ∈ J.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (j0 ∈ J) Hbadleft).

We prove the intermediate claim Htail: ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U).

An exact proof term for the current goal is (andER ((U ∈ Tx ∧ x ∈ U) ∧ j0 ∈ J) (∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U)) Hbad).

We prove the intermediate claim Hp: (((U,j0) ∈ setprod Tx J ∧ x ∈ ((U,j0) 0)) ∧ ((U,j0) 1) ∈ J) ∧ ∀j : set, j ∈ J → (((U,j0) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((U,j0) 0)).

Apply andI to the current goal.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Tx J U j0 HUTx Hj0J).

rewrite the current goal using (tuple_2_0_eq U j0) (from left to right).

An exact proof term for the current goal is HxU.

rewrite the current goal using (tuple_2_1_eq U j0) (from left to right).

An exact proof term for the current goal is Hj0J.

Let j be given.

Assume HjJ: j ∈ J.

Assume Hj0j: (((U,j0) 1),j) ∈ le.

We will prove ¬ (apply_fun net j ∈ ((U,j0) 0)).

We prove the intermediate claim Hj0j': (j0,j) ∈ le.

rewrite the current goal using (tuple_2_1_eq U j0) (from right to left).

An exact proof term for the current goal is Hj0j.

rewrite the current goal using (tuple_2_0_eq U j0) (from left to right).

An exact proof term for the current goal is (Htail j HjJ Hj0j').

We prove the intermediate claim Hprop: Bad x ((pickpair x) 0) ((pickpair x) 1) ∧ pickpair x ∈ setprod Tx J.

We prove the intermediate claim Hpa: pickpair x ∈ setprod Tx J ∧ x ∈ ((pickpair x) 0) ∧ ((pickpair x) 1) ∈ J ∧ ∀j : set, j ∈ J → (((pickpair x) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair x) 0)).

An exact proof term for the current goal is (Eps_i_ax (λp : set ⇒ p ∈ setprod Tx J ∧ x ∈ (p 0) ∧ (p 1) ∈ J ∧ ∀j : set, j ∈ J → ((p 1),j) ∈ le → ¬ (apply_fun net j ∈ (p 0))) (U,j0) Hp).

We prove the intermediate claim HpaL: (pickpair x ∈ setprod Tx J ∧ x ∈ ((pickpair x) 0)) ∧ ((pickpair x) 1) ∈ J.

An exact proof term for the current goal is (andEL ((pickpair x ∈ setprod Tx J ∧ x ∈ ((pickpair x) 0)) ∧ ((pickpair x) 1) ∈ J) (∀j : set, j ∈ J → (((pickpair x) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair x) 0))) Hpa).

We prove the intermediate claim HpaA: pickpair x ∈ setprod Tx J ∧ x ∈ ((pickpair x) 0).

An exact proof term for the current goal is (andEL (pickpair x ∈ setprod Tx J ∧ x ∈ ((pickpair x) 0)) (((pickpair x) 1) ∈ J) HpaL).

We prove the intermediate claim Hpp: pickpair x ∈ setprod Tx J.

An exact proof term for the current goal is (andEL (pickpair x ∈ setprod Tx J) (x ∈ ((pickpair x) 0)) HpaA).

We prove the intermediate claim HUx': ((pickpair x) 0) ∈ Tx.

An exact proof term for the current goal is (ap0_Sigma Tx (λ_ : set ⇒ J) (pickpair x) Hpp).

We prove the intermediate claim HxU': x ∈ ((pickpair x) 0).

An exact proof term for the current goal is (andER (pickpair x ∈ setprod Tx J) (x ∈ ((pickpair x) 0)) HpaA).

We prove the intermediate claim Hj0': ((pickpair x) 1) ∈ J.

An exact proof term for the current goal is (andER (pickpair x ∈ setprod Tx J ∧ x ∈ ((pickpair x) 0)) (((pickpair x) 1) ∈ J) HpaL).

We prove the intermediate claim Htail': ∀j : set, j ∈ J → (((pickpair x) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair x) 0)).

An exact proof term for the current goal is (andER ((pickpair x ∈ setprod Tx J ∧ x ∈ ((pickpair x) 0)) ∧ ((pickpair x) 1) ∈ J) (∀j : set, j ∈ J → (((pickpair x) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair x) 0))) Hpa).

We prove the intermediate claim Hbad': Bad x ((pickpair x) 0) ((pickpair x) 1).

An exact proof term for the current goal is (andI (((((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0)) ∧ ((pickpair x) 1) ∈ J)) (∀j : set, j ∈ J → (((pickpair x) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair x) 0))) (andI (((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0)) (((pickpair x) 1) ∈ J) (andI (((pickpair x) 0) ∈ Tx) (x ∈ ((pickpair x) 0)) HUx' HxU') Hj0') Htail').

An exact proof term for the current goal is (andI (Bad x ((pickpair x) 0) ((pickpair x) 1)) (pickpair x ∈ setprod Tx J) Hbad' Hpp).

An exact proof term for the current goal is (andEL (Bad x ((pickpair x) 0) ((pickpair x) 1)) (pickpair x ∈ setprod Tx J) Hprop).

We will prove ((topology_on X Tx ∧ Fam ⊆ 𝒫 X) ∧ X ⊆ ⋃ Fam) ∧ (∀U : set, U ∈ Fam → U ∈ Tx).

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

Let U be given.

Assume HU: U ∈ Fam.

We will prove U ∈ 𝒫 X.

Apply PowerI to the current goal.

Let y be given.

Assume Hy: y ∈ U.

We will prove y ∈ X.

We prove the intermediate claim Hexx: ∃x : set, x ∈ X ∧ U = ((pickpair x) 0).

An exact proof term for the current goal is (ReplE X (λx0 : set ⇒ ((pickpair x0) 0)) U HU).

Apply Hexx to the current goal.

Let x be given.

Assume HxU: x ∈ X ∧ U = ((pickpair x) 0).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (andEL (x ∈ X) (U = ((pickpair x) 0)) HxU).

We prove the intermediate claim HUeq: U = ((pickpair x) 0).

An exact proof term for the current goal is (andER (x ∈ X) (U = ((pickpair x) 0)) HxU).

We prove the intermediate claim HUtx: U ∈ Tx.

rewrite the current goal using HUeq (from left to right).

We prove the intermediate claim HpbL: (((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0)) ∧ ((pickpair x) 1) ∈ J.

An exact proof term for the current goal is (andEL ((((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0)) ∧ ((pickpair x) 1) ∈ J) (∀j : set, j ∈ J → (((pickpair x) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair x) 0))) (HpickBad x HxX)).

We prove the intermediate claim HpbUx: ((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0).

An exact proof term for the current goal is (andEL (((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0)) (((pickpair x) 1) ∈ J) HpbL).

An exact proof term for the current goal is (andEL (((pickpair x) 0) ∈ Tx) (x ∈ ((pickpair x) 0)) HpbUx).

We prove the intermediate claim HUpow: U ∈ 𝒫 X.

An exact proof term for the current goal is (HTsub U HUtx).

An exact proof term for the current goal is (PowerE X U HUpow y Hy).

Let y be given.

Assume HyX: y ∈ X.

We will prove y ∈ ⋃ Fam.

We prove the intermediate claim HUy: y ∈ ((pickpair y) 0).

We prove the intermediate claim HpbL: (((pickpair y) 0) ∈ Tx ∧ y ∈ ((pickpair y) 0)) ∧ ((pickpair y) 1) ∈ J.

An exact proof term for the current goal is (andEL ((((pickpair y) 0) ∈ Tx ∧ y ∈ ((pickpair y) 0)) ∧ ((pickpair y) 1) ∈ J) (∀j : set, j ∈ J → (((pickpair y) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair y) 0))) (HpickBad y HyX)).

We prove the intermediate claim HpbUx: ((pickpair y) 0) ∈ Tx ∧ y ∈ ((pickpair y) 0).

An exact proof term for the current goal is (andEL (((pickpair y) 0) ∈ Tx ∧ y ∈ ((pickpair y) 0)) (((pickpair y) 1) ∈ J) HpbL).

An exact proof term for the current goal is (andER (((pickpair y) 0) ∈ Tx) (y ∈ ((pickpair y) 0)) HpbUx).

We prove the intermediate claim HUyFam: ((pickpair y) 0) ∈ Fam.

An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ ((pickpair x0) 0)) y HyX).

An exact proof term for the current goal is (UnionI Fam y ((pickpair y) 0) HUy HUyFam).

Let U be given.

Assume HU: U ∈ Fam.

We will prove U ∈ Tx.

We prove the intermediate claim Hexx: ∃x : set, x ∈ X ∧ U = ((pickpair x) 0).

An exact proof term for the current goal is (ReplE X (λx0 : set ⇒ ((pickpair x0) 0)) U HU).

Apply Hexx to the current goal.

Let x be given.

Assume HxU: x ∈ X ∧ U = ((pickpair x) 0).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (andEL (x ∈ X) (U = ((pickpair x) 0)) HxU).

We prove the intermediate claim HUeq: U = ((pickpair x) 0).

An exact proof term for the current goal is (andER (x ∈ X) (U = ((pickpair x) 0)) HxU).

rewrite the current goal using HUeq (from left to right).

We prove the intermediate claim HpbL: (((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0)) ∧ ((pickpair x) 1) ∈ J.

We prove the intermediate claim HpbUx: ((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0).

An exact proof term for the current goal is (andEL (((pickpair x) 0) ∈ Tx ∧ x ∈ ((pickpair x) 0)) (((pickpair x) 1) ∈ J) HpbL).

An exact proof term for the current goal is (andEL (((pickpair x) 0) ∈ Tx) (x ∈ ((pickpair x) 0)) HpbUx).

An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp Fam Hcover).

Assume Hfin: has_finite_subcover X Tx Fam.

Apply Hfin to the current goal.

Let G be given.

Assume HGpack: G ⊆ Fam ∧ finite G ∧ X ⊆ ⋃ G.

We prove the intermediate claim HGleft: G ⊆ Fam ∧ finite G.

An exact proof term for the current goal is (andEL (G ⊆ Fam ∧ finite G) (X ⊆ ⋃ G) HGpack).

We prove the intermediate claim HGsub: G ⊆ Fam.

An exact proof term for the current goal is (andEL (G ⊆ Fam) (finite G) HGleft).

We prove the intermediate claim HGfin: finite G.

An exact proof term for the current goal is (andER (G ⊆ Fam) (finite G) HGleft).

We prove the intermediate claim HGcov: X ⊆ ⋃ G.

An exact proof term for the current goal is (andER (G ⊆ Fam ∧ finite G) (X ⊆ ⋃ G) HGpack).

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 HdirJ).

We prove the intermediate claim Hrefl: ∀a : set, a ∈ J → (a,a) ∈ le.

An exact proof term for the current goal is (partial_order_on_refl J le Hpo).

We prove the intermediate claim Htrans: ∀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).

We prove the intermediate claim Hpickpair_prop: ∀x : set, x ∈ X → pickpair x ∈ setprod Tx J ∧ x ∈ ((pickpair x) 0) ∧ ((pickpair x) 1) ∈ J ∧ ∀j : set, j ∈ J → (((pickpair x) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair x) 0)).

Let x be given.

Assume HxX: x ∈ X.

We prove the intermediate claim HexUJ: ∃U j0 : set, Bad x U j0.

An exact proof term for the current goal is (HexBad x HxX).

Apply HexUJ to the current goal.

Let U be given.

Assume Hexj0: ∃j0 : set, Bad x U j0.

Apply Hexj0 to the current goal.

Let j0 be given.

Assume Hbad: Bad x U j0.

We prove the intermediate claim Hbadleft: (U ∈ Tx ∧ x ∈ U) ∧ j0 ∈ J.

An exact proof term for the current goal is (andEL ((U ∈ Tx ∧ x ∈ U) ∧ j0 ∈ J) (∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U)) Hbad).

We prove the intermediate claim HbadUx: U ∈ Tx ∧ x ∈ U.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (j0 ∈ J) Hbadleft).

We prove the intermediate claim HUTx: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HbadUx).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HbadUx).

We prove the intermediate claim Hj0J: j0 ∈ J.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (j0 ∈ J) Hbadleft).

We prove the intermediate claim Htail: ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U).

An exact proof term for the current goal is (andER ((U ∈ Tx ∧ x ∈ U) ∧ j0 ∈ J) (∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U)) Hbad).

We prove the intermediate claim Hp: (((U,j0) ∈ setprod Tx J ∧ x ∈ ((U,j0) 0)) ∧ ((U,j0) 1) ∈ J) ∧ ∀j : set, j ∈ J → (((U,j0) 1),j) ∈ le → ¬ (apply_fun net j ∈ ((U,j0) 0)).

Apply andI to the current goal.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Tx J U j0 HUTx Hj0J).

rewrite the current goal using (tuple_2_0_eq U j0) (from left to right).

An exact proof term for the current goal is HxU.

rewrite the current goal using (tuple_2_1_eq U j0) (from left to right).

An exact proof term for the current goal is Hj0J.

Let j be given.

Assume HjJ: j ∈ J.

Assume Hj0j: (((U,j0) 1),j) ∈ le.

We will prove ¬ (apply_fun net j ∈ ((U,j0) 0)).

We prove the intermediate claim Hj0j': (j0,j) ∈ le.

rewrite the current goal using (tuple_2_1_eq U j0) (from right to left).

An exact proof term for the current goal is Hj0j.

rewrite the current goal using (tuple_2_0_eq U j0) (from left to right).

An exact proof term for the current goal is (Htail j HjJ Hj0j').

Set P to be the term (λG0 : set ⇒ G0 ⊆ G → ∃j0 : set, j0 ∈ J ∧ ∀U : set, U ∈ G0 → ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U)).

We prove the intermediate claim HP0: P Empty.

Assume _: Empty ⊆ G.

We prove the intermediate claim HJne: J ≠ Empty.

An exact proof term for the current goal is (directed_set_nonempty J le HdirJ).

Apply (nonempty_has_element J HJne) to the current goal.

Let j0 be given.

Assume Hj0J: j0 ∈ J.

We use j0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hj0J.

Let U be given.

Assume HU: U ∈ Empty.

Apply FalseE to the current goal.

An exact proof term for the current goal is ((EmptyE U) HU).

We prove the intermediate claim HPstep: ∀X0 y : set, finite X0 → y ∉ X0 → P X0 → P (X0 ∪ {y}).

Let X0 and y be given.

Assume HX0fin: finite X0.

Assume HyX0: y ∉ X0.

Assume IH: P X0.

Assume HsubAll: (X0 ∪ {y}) ⊆ G.

We prove the intermediate claim HX0sub: X0 ⊆ G.

Let U be given.

Assume HU: U ∈ X0.

We prove the intermediate claim HUb: U ∈ (X0 ∪ {y}).

An exact proof term for the current goal is (binunionI1 X0 {y} U HU).

An exact proof term for the current goal is (HsubAll U HUb).

We prove the intermediate claim HyG: y ∈ G.

We prove the intermediate claim Hyin: y ∈ (X0 ∪ {y}).

An exact proof term for the current goal is (binunionI2 X0 {y} y (SingI y)).

An exact proof term for the current goal is (HsubAll y Hyin).

Apply (IH HX0sub) to the current goal.

Let jX be given.

Assume HjXpack: jX ∈ J ∧ ∀U : set, U ∈ X0 → ∀j : set, j ∈ J → (jX,j) ∈ le → ¬ (apply_fun net j ∈ U).

We prove the intermediate claim HjXJ: jX ∈ J.

An exact proof term for the current goal is (andEL (jX ∈ J) (∀U : set, U ∈ X0 → ∀j : set, j ∈ J → (jX,j) ∈ le → ¬ (apply_fun net j ∈ U)) HjXpack).

We prove the intermediate claim HtailX0: ∀U : set, U ∈ X0 → ∀j : set, j ∈ J → (jX,j) ∈ le → ¬ (apply_fun net j ∈ U).

An exact proof term for the current goal is (andER (jX ∈ J) (∀U : set, U ∈ X0 → ∀j : set, j ∈ J → (jX,j) ∈ le → ¬ (apply_fun net j ∈ U)) HjXpack).

We prove the intermediate claim HyFam: y ∈ Fam.

An exact proof term for the current goal is (HGsub y HyG).

We prove the intermediate claim Hexx: ∃x : set, x ∈ X ∧ y = ((pickpair x) 0).

An exact proof term for the current goal is (ReplE X (λx0 : set ⇒ ((pickpair x0) 0)) y HyFam).

Apply Hexx to the current goal.

Let xY be given.

Assume HxY: xY ∈ X ∧ y = ((pickpair xY) 0).

We prove the intermediate claim HxYin: xY ∈ X.

An exact proof term for the current goal is (andEL (xY ∈ X) (y = ((pickpair xY) 0)) HxY).

We prove the intermediate claim HyEq: y = ((pickpair xY) 0).

An exact proof term for the current goal is (andER (xY ∈ X) (y = ((pickpair xY) 0)) HxY).

Set jY to be the term ((pickpair xY) 1).

We prove the intermediate claim HjYJ: jY ∈ J.

We prove the intermediate claim Hpa: pickpair xY ∈ setprod Tx J ∧ xY ∈ ((pickpair xY) 0) ∧ jY ∈ J ∧ ∀j : set, j ∈ J → (jY,j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair xY) 0)).

An exact proof term for the current goal is (Hpickpair_prop xY HxYin).

We prove the intermediate claim HpaL: (pickpair xY ∈ setprod Tx J ∧ xY ∈ ((pickpair xY) 0)) ∧ jY ∈ J.

An exact proof term for the current goal is (andEL ((pickpair xY ∈ setprod Tx J ∧ xY ∈ ((pickpair xY) 0)) ∧ jY ∈ J) (∀j : set, j ∈ J → (jY,j) ∈ le → ¬ (apply_fun net j ∈ ((pickpair xY) 0))) Hpa).

An exact proof term for the current goal is (andER (pickpair xY ∈ setprod Tx J ∧ xY ∈ ((pickpair xY) 0)) (jY ∈ J) HpaL).

We prove the intermediate claim HtailY: ∀j : set, j ∈ J → (jY,j) ∈ le → ¬ (apply_fun net j ∈ y).

Let j be given.

Assume HjJ: j ∈ J.

Assume HjYj: (jY,j) ∈ le.

We will prove ¬ (apply_fun net j ∈ y).

rewrite the current goal using HyEq (from left to right).

We prove the intermediate claim Hpa: pickpair xY ∈ setprod Tx J ∧ xY ∈ ((pickpair xY) 0) ∧ jY ∈ J ∧ ∀j0 : set, j0 ∈ J → (jY,j0) ∈ le → ¬ (apply_fun net j0 ∈ ((pickpair xY) 0)).

An exact proof term for the current goal is (Hpickpair_prop xY HxYin).

An exact proof term for the current goal is ((andER ((pickpair xY ∈ setprod Tx J ∧ xY ∈ ((pickpair xY) 0)) ∧ jY ∈ J) (∀j0 : set, j0 ∈ J → (jY,j0) ∈ le → ¬ (apply_fun net j0 ∈ ((pickpair xY) 0))) Hpa) j HjJ HjYj).

We prove the intermediate claim Hexub: ∃j0 : set, j0 ∈ J ∧ (jX,j0) ∈ le ∧ (jY,j0) ∈ le.

An exact proof term for the current goal is (directed_set_upper_bound_property J le HdirJ jX jY HjXJ HjYJ).

Apply Hexub to the current goal.

Let j0 be given.

Assume Hj0pack: j0 ∈ J ∧ (jX,j0) ∈ le ∧ (jY,j0) ∈ le.

We prove the intermediate claim Hj0left: j0 ∈ J ∧ (jX,j0) ∈ le.

An exact proof term for the current goal is (andEL (j0 ∈ J ∧ (jX,j0) ∈ le) ((jY,j0) ∈ le) Hj0pack).

We prove the intermediate claim Hj0J: j0 ∈ J.

An exact proof term for the current goal is (andEL (j0 ∈ J) ((jX,j0) ∈ le) Hj0left).

We prove the intermediate claim HjXj0: (jX,j0) ∈ le.

An exact proof term for the current goal is (andER (j0 ∈ J) ((jX,j0) ∈ le) Hj0left).

We prove the intermediate claim HjYj0: (jY,j0) ∈ le.

An exact proof term for the current goal is (andER (j0 ∈ J ∧ (jX,j0) ∈ le) ((jY,j0) ∈ le) Hj0pack).

We use j0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hj0J.

Let U be given.

Assume HU: U ∈ (X0 ∪ {y}).

We will prove ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U).

Apply (binunionE' X0 {y} U (∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U))) to the current goal.

Assume HUx0: U ∈ X0.

Let j be given.

Assume HjJ: j ∈ J.

Assume Hj0j: (j0,j) ∈ le.

We will prove ¬ (apply_fun net j ∈ U).

We prove the intermediate claim HjXj: (jX,j) ∈ le.

An exact proof term for the current goal is (Htrans jX j0 j HjXJ Hj0J HjJ HjXj0 Hj0j).

An exact proof term for the current goal is (HtailX0 U HUx0 j HjJ HjXj).

Assume HUy: U ∈ {y}.

We prove the intermediate claim HUeq: U = y.

An exact proof term for the current goal is (SingE y U HUy).

rewrite the current goal using HUeq (from left to right).

Let j be given.

Assume HjJ: j ∈ J.

Assume Hj0j: (j0,j) ∈ le.

We will prove ¬ (apply_fun net j ∈ y).

We prove the intermediate claim HjYj: (jY,j) ∈ le.

An exact proof term for the current goal is (Htrans jY j0 j HjYJ Hj0J HjJ HjYj0 Hj0j).

An exact proof term for the current goal is (HtailY j HjJ HjYj).

An exact proof term for the current goal is HU.

We prove the intermediate claim HPG: P G.

An exact proof term for the current goal is (finite_ind P HP0 HPstep G HGfin).

We prove the intermediate claim HGsubG: G ⊆ G.

Let U be given.

Assume HU: U ∈ G.

An exact proof term for the current goal is HU.

Apply (HPG HGsubG) to the current goal.

Let j0 be given.

Assume Hj0pack: j0 ∈ J ∧ ∀U : set, U ∈ G → ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U).

We prove the intermediate claim Hj0J: j0 ∈ J.

An exact proof term for the current goal is (andEL (j0 ∈ J) (∀U : set, U ∈ G → ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U)) Hj0pack).

We prove the intermediate claim HavoidG: ∀U : set, U ∈ G → ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U).

An exact proof term for the current goal is (andER (j0 ∈ J) (∀U : set, U ∈ G → ∀j : set, j ∈ J → (j0,j) ∈ le → ¬ (apply_fun net j ∈ U)) Hj0pack).

We prove the intermediate claim HnotUnion: ¬ (apply_fun net j0 ∈ ⋃ G).

Assume Hmem: apply_fun net j0 ∈ ⋃ G.

Apply (UnionE G (apply_fun net j0) Hmem) to the current goal.

Let U be given.

Assume HU: apply_fun net j0 ∈ U ∧ U ∈ G.

We prove the intermediate claim HUin: U ∈ G.

An exact proof term for the current goal is (andER (apply_fun net j0 ∈ U) (U ∈ G) HU).

We prove the intermediate claim Hrefl0: (j0,j0) ∈ le.

An exact proof term for the current goal is (Hrefl j0 Hj0J).

An exact proof term for the current goal is ((HavoidG U HUin j0 Hj0J Hrefl0) (andEL (apply_fun net j0 ∈ U) (U ∈ G) HU)).

We prove the intermediate claim Hnetj0X: apply_fun net j0 ∈ X.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y net J X j0 Htotnet Hj0J).

An exact proof term for the current goal is (HnotUnion (HGcov (apply_fun net j0) Hnetj0X)).