Let X, S, net, J, le and x be given.
Assume HS: subbasis_on X S.
Assume Hdir: directed_set J le.
Assume Htot: total_function_on net J X.
Assume Hgraph: functional_graph net.
Assume Hdom: graph_domain_subset net J.
Assume HxX: x ∈ X.
Assume HevS: ∀s : set, s ∈ S → x ∈ s → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ s.
Set T to be the term generated_topology_from_subbasis X S.
We prove the intermediate claim HTtop: topology_on X T.
An exact proof term for the current goal is (topology_from_subbasis_is_topology X S HS).
We will prove net_converges_on X T net J le x.
We will prove topology_on X T ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X ∧ ∀U : set, U ∈ T → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
Apply (and7I (topology_on X T) (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) (x ∈ X) (∀U : set, U ∈ T → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U)) to the current goal.
An exact proof term for the current goal is HTtop.
An exact proof term for the current goal is Hdir.
An exact proof term for the current goal is Htot.
An exact proof term for the current goal is Hgraph.
An exact proof term for the current goal is Hdom.
An exact proof term for the current goal is HxX.
Let U be given.
Assume HU: U ∈ T.
Assume HxU: x ∈ U.
We prove the intermediate claim HexF: ∃F : set, F ∈ finite_subcollections S ∧ x ∈ intersection_of_family X F ∧ intersection_of_family X F ⊆ U.
An exact proof term for the current goal is (generated_topology_from_subbasis_finite_neighborhood X S U x HS HU HxU).
Apply HexF to the current goal.
Let F be given.
Assume HFpack.
We prove the intermediate claim HF12: F ∈ finite_subcollections S ∧ x ∈ intersection_of_family X F.
An exact proof term for the current goal is (andEL (F ∈ finite_subcollections S ∧ x ∈ intersection_of_family X F) (intersection_of_family X F ⊆ U) HFpack).
We prove the intermediate claim HFfin: F ∈ finite_subcollections S.
An exact proof term for the current goal is (andEL (F ∈ finite_subcollections S) (x ∈ intersection_of_family X F) HF12).
We prove the intermediate claim HxInt: x ∈ intersection_of_family X F.
An exact proof term for the current goal is (andER (F ∈ finite_subcollections S) (x ∈ intersection_of_family X F) HF12).
We prove the intermediate claim HintSubU: intersection_of_family X F ⊆ U.
An exact proof term for the current goal is (andER (F ∈ finite_subcollections S ∧ x ∈ intersection_of_family X F) (intersection_of_family X F ⊆ U) HFpack).
Set p to be the term (λA : set ⇒ A ⊆ S → x ∈ intersection_of_family X A → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ intersection_of_family X A).
We prove the intermediate claim HpEmpty: p Empty.
Assume Hsub0: Empty ⊆ S.
Assume HxI0: x ∈ intersection_of_family X Empty.
We will prove ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ intersection_of_family X Empty.
We prove the intermediate claim HJne: J ≠ Empty.
An exact proof term for the current goal is (directed_set_nonempty J le Hdir).
Apply (nonempty_has_element J HJne) to the current goal.
Let i0 be given.
Assume Hi0J: i0 ∈ J.
We use i0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0J.
Let i be given.
Assume HiJ: i ∈ J.
Assume Hi0i: (i0,i) ∈ le.
We will prove apply_fun net i ∈ intersection_of_family X Empty.
rewrite the current goal using (intersection_of_family_empty_eq X) (from left to right).
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y net J X i Htot HiJ).
We prove the intermediate claim HpStep: ∀A y : set, finite A → y ∉ A → p A → p (A ∪ {y}).
Let A and y be given.
Assume HAfin: finite A.
Assume HynA: y ∉ A.
Assume HpA: p A.
Assume HsubAy: A ∪ {y} ⊆ S.
Assume HxIay: x ∈ intersection_of_family X (A ∪ {y}).
We will prove ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ intersection_of_family X (A ∪ {y}).
We prove the intermediate claim HsubA: A ⊆ S.
An exact proof term for the current goal is (Subq_tra A (A ∪ {y}) S (binunion_Subq_1 A {y}) HsubAy).
We prove the intermediate claim HyIn: y ∈ A ∪ {y}.
An exact proof term for the current goal is (binunionI2 A {y} y (SingI y)).
We prove the intermediate claim HyS: y ∈ S.
An exact proof term for the current goal is (HsubAy y HyIn).
We prove the intermediate claim HxIay2: x ∈ (intersection_of_family X A) ∩ y.
rewrite the current goal using (intersection_of_family_adjoin X A y) (from right to left).
An exact proof term for the current goal is HxIay.
We prove the intermediate claim HxIA: x ∈ intersection_of_family X A.
An exact proof term for the current goal is (binintersectE1 (intersection_of_family X A) y x HxIay2).
We prove the intermediate claim Hxy: x ∈ y.
An exact proof term for the current goal is (binintersectE2 (intersection_of_family X A) y x HxIay2).
Apply (HpA HsubA HxIA) to the current goal.
Let iA be given.
Assume HiApair.
Apply HiApair to the current goal.
Assume HiAJ HafterA.
Apply (HevS y HyS Hxy) to the current goal.
Let iy be given.
Assume Hiypair.
Apply Hiypair to the current goal.
Assume HiyJ HafterY.
Apply (directed_set_upper_bound_property J le Hdir iA iy HiAJ HiyJ) to the current goal.
Let i0 be given.
Assume Hi0pack.
We prove the intermediate claim Hi0AB: i0 ∈ J ∧ (iA,i0) ∈ le.
An exact proof term for the current goal is (andEL (i0 ∈ J ∧ (iA,i0) ∈ le) ((iy,i0) ∈ le) Hi0pack).
We prove the intermediate claim Hi0J: i0 ∈ J.
An exact proof term for the current goal is (andEL (i0 ∈ J) ((iA,i0) ∈ le) Hi0AB).
We prove the intermediate claim HiAi0: (iA,i0) ∈ le.
An exact proof term for the current goal is (andER (i0 ∈ J) ((iA,i0) ∈ le) Hi0AB).
We prove the intermediate claim Hiyi0: (iy,i0) ∈ le.
An exact proof term for the current goal is (andER (i0 ∈ J ∧ (iA,i0) ∈ le) ((iy,i0) ∈ le) Hi0pack).
We use i0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0J.
Let i be given.
Assume HiJ: i ∈ J.
Assume Hi0i: (i0,i) ∈ le.
We will prove apply_fun net i ∈ intersection_of_family X (A ∪ {y}).
We prove the intermediate claim HiAi: (iA,i) ∈ le.
An exact proof term for the current goal is (directed_set_trans J le Hdir iA i0 i HiAJ Hi0J HiJ HiAi0 Hi0i).
We prove the intermediate claim Hiyi: (iy,i) ∈ le.
An exact proof term for the current goal is (directed_set_trans J le Hdir iy i0 i HiyJ Hi0J HiJ Hiyi0 Hi0i).
We prove the intermediate claim HnetA: apply_fun net i ∈ intersection_of_family X A.
An exact proof term for the current goal is (HafterA i HiJ HiAi).
We prove the intermediate claim Hnety: apply_fun net i ∈ y.
An exact proof term for the current goal is (HafterY i HiJ Hiyi).
rewrite the current goal using (intersection_of_family_adjoin X A y) (from left to right).
An exact proof term for the current goal is (binintersectI (intersection_of_family X A) y (apply_fun net i) HnetA Hnety).
We prove the intermediate claim Hall: ∀A : set, finite A → p A.
An exact proof term for the current goal is (finite_ind (λA0 : set ⇒ p A0) HpEmpty HpStep).
We prove the intermediate claim HFpow: F ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) F HFfin).
We prove the intermediate claim HFset: F ⊆ S.
An exact proof term for the current goal is (PowerE S F HFpow).
We prove the intermediate claim HFf: finite F.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) F HFfin).
Apply (Hall F HFf HFset HxInt) to the current goal.
Let i0 be given.
Assume Hi0pair.
Apply Hi0pair to the current goal.
Assume Hi0J HafterInt.
We use i0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0J.
Let i be given.
Assume HiJ: i ∈ J.
Assume Hi0i: (i0,i) ∈ le.
We will prove apply_fun net i ∈ U.
Apply HintSubU to the current goal.
An exact proof term for the current goal is (HafterInt i HiJ Hi0i).
∎