Let X, Tx, net, x, J and le be given.
Assume Hacc_on: accumulation_point_of_net_on X Tx net J le x.
We will prove ∃K leK phi sub : set, subnet_of_witness net sub J le K leK X phi ∧ net_converges_on X Tx sub K leK x.
Apply Hacc_on to the current goal.
Assume Hcore Hfreq.
Apply Hcore to the current goal.
Assume Hcore5 HxX.
Apply Hcore5 to the current goal.
Assume Hcore4 Hdomnet.
Apply Hcore4 to the current goal.
Assume Hcore3 Hgraphnet.
Apply Hcore3 to the current goal.
Assume Hcore2 Htotnet.
Apply Hcore2 to the current goal.
Assume HTx HdirJ.
We prove the intermediate claim Hfunnet: function_on net J X.
An exact proof term for the current goal is (total_function_on_function_on net J X Htotnet).
We prove the intermediate claim Hrefl: ∀j0 : set, j0 ∈ J → (j0,j0) ∈ le.
Let j0 be given.
Assume Hj0: j0 ∈ J.
An exact proof term for the current goal is (directed_set_refl J le HdirJ j0 Hj0).
Set N to be the term {U ∈ Tx|x ∈ U}.
Set K to be the term {p ∈ setprod N J|apply_fun net (p 1) ∈ p 0}.
Set leK to be the term {q ∈ setprod K K|(q 1) 0 ⊆ (q 0) 0 ∧ ((q 0) 1,(q 1) 1) ∈ le}.
Set phi to be the term graph K (λk : set ⇒ k 1).
Set sub to be the term graph K (λk : set ⇒ apply_fun net (k 1)).
We prove the intermediate claim HdirK: directed_set K leK.
We will prove directed_set K leK.
We prove the intermediate claim HJpack: J ≠ Empty ∧ partial_order_on J le.
An exact proof term for the current goal is (andEL (J ≠ Empty ∧ partial_order_on J le) (∀a b : set, a ∈ J → b ∈ J → ∃c : set, c ∈ J ∧ (a,c) ∈ le ∧ (b,c) ∈ le) HdirJ).
We prove the intermediate claim HJpo: partial_order_on J le.
An exact proof term for the current goal is (andER (J ≠ Empty) (partial_order_on J le) HJpack).
We prove the intermediate claim HantisymJ: ∀a b : set, a ∈ J → b ∈ J → (a,b) ∈ le → (b,a) ∈ le → a = b.
An exact proof term for the current goal is (partial_order_on_antisym J le HJpo).
We prove the intermediate claim HtransJ: ∀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 HJpo).
We will prove (K ≠ Empty ∧ partial_order_on K leK) ∧ ∀a b : set, a ∈ K → b ∈ K → ∃c : set, c ∈ K ∧ (a,c) ∈ leK ∧ (b,c) ∈ leK.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HJne: J ≠ Empty.
An exact proof term for the current goal is (andEL (J ≠ Empty) (partial_order_on J le) HJpack).
We prove the intermediate claim Hexj0: ∃j0 : set, j0 ∈ J.
An exact proof term for the current goal is (nonempty_has_element J HJne).
Apply Hexj0 to the current goal.
Let j0 be given.
Assume Hj0: j0 ∈ J.
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HXN: X ∈ N.
An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ x ∈ U0) X HXTx HxX).
We prove the intermediate claim Hnetj0X: apply_fun net j0 ∈ X.
An exact proof term for the current goal is (Hfunnet j0 Hj0).
We prove the intermediate claim HpProd: (X,j0) ∈ setprod N J.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma N J X j0 HXN Hj0).
We prove the intermediate claim Hp_in: apply_fun net ((X,j0) 1) ∈ (X,j0) 0.
rewrite the current goal using (tuple_2_1_eq X j0) (from left to right).
rewrite the current goal using (tuple_2_0_eq X j0) (from left to right).
An exact proof term for the current goal is Hnetj0X.
We prove the intermediate claim HpK: (X,j0) ∈ K.
An exact proof term for the current goal is (SepI (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) (X,j0) HpProd Hp_in).
An exact proof term for the current goal is (elem_implies_nonempty K (X,j0) HpK).
We will prove partial_order_on K leK.
We will prove relation_on leK K ∧ (∀a : set, a ∈ K → (a,a) ∈ leK) ∧ (∀a b : set, a ∈ K → b ∈ K → (a,b) ∈ leK → (b,a) ∈ leK → a = b) ∧ (∀a b c : set, a ∈ K → b ∈ K → c ∈ K → (a,b) ∈ leK → (b,c) ∈ leK → (a,c) ∈ leK).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove relation_on leK K.
Let a and b be given.
Assume Hab: (a,b) ∈ leK.
We will prove a ∈ K ∧ b ∈ K.
We prove the intermediate claim Hprod: (a,b) ∈ setprod K K.
An exact proof term for the current goal is (SepE1 (setprod K K) (λq : set ⇒ (q 1) 0 ⊆ (q 0) 0 ∧ ((q 0) 1,(q 1) 1) ∈ le) (a,b) Hab).
We prove the intermediate claim HaK: (a,b) 0 ∈ K.
An exact proof term for the current goal is (ap0_Sigma K (λ_ : set ⇒ K) (a,b) Hprod).
We prove the intermediate claim HbK: (a,b) 1 ∈ K.
An exact proof term for the current goal is (ap1_Sigma K (λ_ : set ⇒ K) (a,b) Hprod).
Apply andI to the current goal.
rewrite the current goal using (tuple_2_0_eq a b) (from right to left).
An exact proof term for the current goal is HaK.
rewrite the current goal using (tuple_2_1_eq a b) (from right to left).
An exact proof term for the current goal is HbK.
Let a be given.
Assume HaK: a ∈ K.
We will prove (a,a) ∈ leK.
Apply (SepI (setprod K K) (λq : set ⇒ (q 1) 0 ⊆ (q 0) 0 ∧ ((q 0) 1,(q 1) 1) ∈ le) (a,a)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K K a a HaK HaK).
Apply andI to the current goal.
rewrite the current goal using (tuple_2_1_eq a a) (from left to right).
rewrite the current goal using (tuple_2_0_eq a a) (from left to right).
An exact proof term for the current goal is (Subq_ref (a 0)).
We prove the intermediate claim HaProd: a ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) a HaK).
We prove the intermediate claim Ha1J: a 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) a HaProd).
rewrite the current goal using (tuple_2_0_eq a a) (from left to right).
rewrite the current goal using (tuple_2_1_eq a a) (from left to right).
An exact proof term for the current goal is (Hrefl (a 1) Ha1J).
Let a and b be given.
Assume HaK: a ∈ K.
Assume HbK: b ∈ K.
Assume Hab: (a,b) ∈ leK.
Assume Hba: (b,a) ∈ leK.
We will prove a = b.
We prove the intermediate claim Habp: (b 0) ⊆ (a 0) ∧ ((a 1),(b 1)) ∈ le.
An exact proof term for the current goal is (pair_order_pred K le a b Hab).
We prove the intermediate claim Hbabp: (a 0) ⊆ (b 0) ∧ ((b 1),(a 1)) ∈ le.
An exact proof term for the current goal is (pair_order_pred K le b a Hba).
We prove the intermediate claim Hb0suba0: (b 0) ⊆ (a 0).
An exact proof term for the current goal is (andEL ((b 0) ⊆ (a 0)) (((a 1),(b 1)) ∈ le) Habp).
We prove the intermediate claim Ha0subb0: (a 0) ⊆ (b 0).
An exact proof term for the current goal is (andEL ((a 0) ⊆ (b 0)) (((b 1),(a 1)) ∈ le) Hbabp).
We prove the intermediate claim Ha0eq: (a 0) = (b 0).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ (a 0).
An exact proof term for the current goal is (Ha0subb0 y Hy).
Let y be given.
Assume Hy: y ∈ (b 0).
An exact proof term for the current goal is (Hb0suba0 y Hy).
We prove the intermediate claim Hab1: ((a 1),(b 1)) ∈ le.
An exact proof term for the current goal is (andER ((b 0) ⊆ (a 0)) (((a 1),(b 1)) ∈ le) Habp).
We prove the intermediate claim Hba1: ((b 1),(a 1)) ∈ le.
An exact proof term for the current goal is (andER ((a 0) ⊆ (b 0)) (((b 1),(a 1)) ∈ le) Hbabp).
We prove the intermediate claim HaProd: a ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) a HaK).
We prove the intermediate claim HbProd: b ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) b HbK).
We prove the intermediate claim Ha1J: a 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) a HaProd).
We prove the intermediate claim Hb1J: b 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) b HbProd).
We prove the intermediate claim Ha1eq: (a 1) = (b 1).
An exact proof term for the current goal is (HantisymJ (a 1) (b 1) Ha1J Hb1J Hab1 Hba1).
We prove the intermediate claim Haeta: a = (a 0,a 1).
An exact proof term for the current goal is (setprod_eta N J a HaProd).
We prove the intermediate claim Hbeta: b = (b 0,b 1).
An exact proof term for the current goal is (setprod_eta N J b HbProd).
rewrite the current goal using Haeta (from left to right).
rewrite the current goal using Hbeta (from left to right).
An exact proof term for the current goal is (coords_eq_tuple (a 0) (a 1) (b 0) (b 1) Ha0eq Ha1eq).
Let a, b and c be given.
Assume HaK: a ∈ K.
Assume HbK: b ∈ K.
Assume HcK: c ∈ K.
Assume Hab: (a,b) ∈ leK.
Assume Hbc: (b,c) ∈ leK.
We will prove (a,c) ∈ leK.
Apply (SepI (setprod K K) (λq : set ⇒ (q 1) 0 ⊆ (q 0) 0 ∧ ((q 0) 1,(q 1) 1) ∈ le) (a,c)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K K a c HaK HcK).
We prove the intermediate claim Habp: (b 0) ⊆ (a 0) ∧ ((a 1),(b 1)) ∈ le.
An exact proof term for the current goal is (pair_order_pred K le a b Hab).
We prove the intermediate claim Hbcp: (c 0) ⊆ (b 0) ∧ ((b 1),(c 1)) ∈ le.
An exact proof term for the current goal is (pair_order_pred K le b c Hbc).
We prove the intermediate claim Hc0subb0: (c 0) ⊆ (b 0).
An exact proof term for the current goal is (andEL ((c 0) ⊆ (b 0)) (((b 1),(c 1)) ∈ le) Hbcp).
We prove the intermediate claim Hb0suba0: (b 0) ⊆ (a 0).
An exact proof term for the current goal is (andEL ((b 0) ⊆ (a 0)) (((a 1),(b 1)) ∈ le) Habp).
We prove the intermediate claim Hc0suba0: (c 0) ⊆ (a 0).
An exact proof term for the current goal is (Subq_tra (c 0) (b 0) (a 0) Hc0subb0 Hb0suba0).
We prove the intermediate claim Hab1: ((a 1),(b 1)) ∈ le.
An exact proof term for the current goal is (andER ((b 0) ⊆ (a 0)) (((a 1),(b 1)) ∈ le) Habp).
We prove the intermediate claim Hbc1: ((b 1),(c 1)) ∈ le.
An exact proof term for the current goal is (andER ((c 0) ⊆ (b 0)) (((b 1),(c 1)) ∈ le) Hbcp).
We prove the intermediate claim HaProd: a ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) a HaK).
We prove the intermediate claim HbProd: b ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) b HbK).
We prove the intermediate claim HcProd: c ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) c HcK).
We prove the intermediate claim Ha1J: a 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) a HaProd).
We prove the intermediate claim Hb1J: b 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) b HbProd).
We prove the intermediate claim Hc1J: c 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) c HcProd).
We prove the intermediate claim Hac1: ((a 1),(c 1)) ∈ le.
An exact proof term for the current goal is (HtransJ (a 1) (b 1) (c 1) Ha1J Hb1J Hc1J Hab1 Hbc1).
Apply andI to the current goal.
rewrite the current goal using (tuple_2_1_eq a c) (from left to right).
rewrite the current goal using (tuple_2_0_eq a c) (from left to right).
An exact proof term for the current goal is Hc0suba0.
rewrite the current goal using (tuple_2_0_eq a c) (from left to right).
rewrite the current goal using (tuple_2_1_eq a c) (from left to right).
An exact proof term for the current goal is Hac1.
Let a and b be given.
Assume HaK: a ∈ K.
Assume HbK: b ∈ K.
We will prove ∃c : set, c ∈ K ∧ (a,c) ∈ leK ∧ (b,c) ∈ leK.
We prove the intermediate claim HaProd: a ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) a HaK).
We prove the intermediate claim HbProd: b ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) b HbK).
We prove the intermediate claim Ha0N: a 0 ∈ N.
An exact proof term for the current goal is (ap0_Sigma N (λ_ : set ⇒ J) a HaProd).
We prove the intermediate claim Hb0N: b 0 ∈ N.
An exact proof term for the current goal is (ap0_Sigma N (λ_ : set ⇒ J) b HbProd).
We prove the intermediate claim Ha1J: a 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) a HaProd).
We prove the intermediate claim Hb1J: b 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) b HbProd).
We prove the intermediate claim Ha0Tx: a 0 ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ x ∈ U0) (a 0) Ha0N).
We prove the intermediate claim Hb0Tx: b 0 ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ x ∈ U0) (b 0) Hb0N).
We prove the intermediate claim Hxa0: x ∈ (a 0).
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ x ∈ U0) (a 0) Ha0N).
We prove the intermediate claim Hxb0: x ∈ (b 0).
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ x ∈ U0) (b 0) Hb0N).
We prove the intermediate claim HWTx: (a 0) ∩ (b 0) ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx (a 0) (b 0) HTx Ha0Tx Hb0Tx).
We prove the intermediate claim HxW: x ∈ (a 0) ∩ (b 0).
An exact proof term for the current goal is (binintersectI (a 0) (b 0) x Hxa0 Hxb0).
We prove the intermediate claim HWN: (a 0) ∩ (b 0) ∈ N.
An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ x ∈ U0) ((a 0) ∩ (b 0)) HWTx HxW).
We prove the intermediate claim Hexm: ∃m : set, m ∈ J ∧ (a 1,m) ∈ le ∧ (b 1,m) ∈ le.
An exact proof term for the current goal is (directed_set_upper_bound_property J le HdirJ (a 1) (b 1) Ha1J Hb1J).
Apply Hexm to the current goal.
Let m be given.
Assume HmPack: m ∈ J ∧ (a 1,m) ∈ le ∧ (b 1,m) ∈ le.
We prove the intermediate claim Hm_left: m ∈ J ∧ (a 1,m) ∈ le.
An exact proof term for the current goal is (andEL (m ∈ J ∧ (a 1,m) ∈ le) ((b 1,m) ∈ le) HmPack).
We prove the intermediate claim HmJ: m ∈ J.
An exact proof term for the current goal is (andEL (m ∈ J) ((a 1,m) ∈ le) Hm_left).
We prove the intermediate claim Ham: (a 1,m) ∈ le.
An exact proof term for the current goal is (andER (m ∈ J) ((a 1,m) ∈ le) Hm_left).
We prove the intermediate claim Hbm: (b 1,m) ∈ le.
An exact proof term for the current goal is (andER (m ∈ J ∧ (a 1,m) ∈ le) ((b 1,m) ∈ le) HmPack).
We prove the intermediate claim Hexj: ∃j : set, j ∈ J ∧ (m,j) ∈ le ∧ apply_fun net j ∈ ((a 0) ∩ (b 0)).
An exact proof term for the current goal is (Hfreq ((a 0) ∩ (b 0)) HWTx HxW m HmJ).
Apply Hexj to the current goal.
Let j be given.
Assume HjPack: j ∈ J ∧ (m,j) ∈ le ∧ apply_fun net j ∈ ((a 0) ∩ (b 0)).
We prove the intermediate claim Hj_left: j ∈ J ∧ (m,j) ∈ le.
An exact proof term for the current goal is (andEL (j ∈ J ∧ (m,j) ∈ le) (apply_fun net j ∈ ((a 0) ∩ (b 0))) HjPack).
We prove the intermediate claim HjJ: j ∈ J.
An exact proof term for the current goal is (andEL (j ∈ J) ((m,j) ∈ le) Hj_left).
We prove the intermediate claim Hmj: (m,j) ∈ le.
An exact proof term for the current goal is (andER (j ∈ J) ((m,j) ∈ le) Hj_left).
We prove the intermediate claim HnetjW: apply_fun net j ∈ ((a 0) ∩ (b 0)).
An exact proof term for the current goal is (andER (j ∈ J ∧ (m,j) ∈ le) (apply_fun net j ∈ ((a 0) ∩ (b 0))) HjPack).
We prove the intermediate claim HcProd: (((a 0) ∩ (b 0)),j) ∈ setprod N J.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma N J ((a 0) ∩ (b 0)) j HWN HjJ).
We prove the intermediate claim Hc_in: apply_fun net ((((a 0) ∩ (b 0)),j) 1) ∈ (((a 0) ∩ (b 0)),j) 0.
rewrite the current goal using (tuple_2_1_eq ((a 0) ∩ (b 0)) j) (from left to right).
rewrite the current goal using (tuple_2_0_eq ((a 0) ∩ (b 0)) j) (from left to right).
An exact proof term for the current goal is HnetjW.
We prove the intermediate claim HcK: (((a 0) ∩ (b 0)),j) ∈ K.
An exact proof term for the current goal is (SepI (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) (((a 0) ∩ (b 0)),j) HcProd Hc_in).
We use (((a 0) ∩ (b 0)),j) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HcK.
Apply (SepI (setprod K K) (λq : set ⇒ (q 1) 0 ⊆ (q 0) 0 ∧ ((q 0) 1,(q 1) 1) ∈ le) (a,(((a 0) ∩ (b 0)),j))) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K K a (((a 0) ∩ (b 0)),j) HaK HcK).
Apply andI to the current goal.
rewrite the current goal using (tuple_2_1_eq a (((a 0) ∩ (b 0)),j)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_0_eq ((a 0) ∩ (b 0)) j) (from left to right) at position 1.
rewrite the current goal using (tuple_2_0_eq a (((a 0) ∩ (b 0)),j)) (from left to right) at position 1.
An exact proof term for the current goal is (binintersect_Subq_1 (a 0) (b 0)).
We prove the intermediate claim Haj: (a 1,j) ∈ le.
An exact proof term for the current goal is (HtransJ (a 1) m j Ha1J HmJ HjJ Ham Hmj).
rewrite the current goal using (tuple_2_0_eq a (((a 0) ∩ (b 0)),j)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq a (((a 0) ∩ (b 0)),j)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq ((a 0) ∩ (b 0)) j) (from left to right) at position 1.
An exact proof term for the current goal is Haj.
Apply (SepI (setprod K K) (λq : set ⇒ (q 1) 0 ⊆ (q 0) 0 ∧ ((q 0) 1,(q 1) 1) ∈ le) (b,(((a 0) ∩ (b 0)),j))) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K K b (((a 0) ∩ (b 0)),j) HbK HcK).
Apply andI to the current goal.
rewrite the current goal using (tuple_2_1_eq b (((a 0) ∩ (b 0)),j)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_0_eq ((a 0) ∩ (b 0)) j) (from left to right) at position 1.
rewrite the current goal using (tuple_2_0_eq b (((a 0) ∩ (b 0)),j)) (from left to right) at position 1.
An exact proof term for the current goal is (binintersect_Subq_2 (a 0) (b 0)).
We prove the intermediate claim Hbj: (b 1,j) ∈ le.
An exact proof term for the current goal is (HtransJ (b 1) m j Hb1J HmJ HjJ Hbm Hmj).
rewrite the current goal using (tuple_2_0_eq b (((a 0) ∩ (b 0)),j)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq b (((a 0) ∩ (b 0)),j)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq ((a 0) ∩ (b 0)) j) (from left to right) at position 1.
An exact proof term for the current goal is Hbj.
We prove the intermediate claim Htotsub: total_function_on sub K X.
We prove the intermediate claim Hgsub: ∀k : set, k ∈ K → (λk0 : set ⇒ apply_fun net (k0 1)) k ∈ X.
Let k be given.
Assume HkK: k ∈ K.
We prove the intermediate claim HkProd: k ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) k HkK).
We prove the intermediate claim Hk1J: k 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) k HkProd).
An exact proof term for the current goal is (Hfunnet (k 1) Hk1J).
An exact proof term for the current goal is (total_function_on_graph K X (λk0 : set ⇒ apply_fun net (k0 1)) Hgsub).
We prove the intermediate claim Hgraphsub: functional_graph sub.
An exact proof term for the current goal is (functional_graph_graph K (λk0 : set ⇒ apply_fun net (k0 1))).
We prove the intermediate claim Hdomsub: graph_domain_subset sub K.
An exact proof term for the current goal is (graph_domain_subset_graph K (λk0 : set ⇒ apply_fun net (k0 1))).
We prove the intermediate claim Htotphi: total_function_on phi K J.
We prove the intermediate claim Hgphi: ∀k : set, k ∈ K → (λk0 : set ⇒ k0 1) k ∈ J.
Let k be given.
Assume HkK: k ∈ K.
We prove the intermediate claim HkProd: k ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) k HkK).
An exact proof term for the current goal is (ap1_Sigma N (λ_ : set ⇒ J) k HkProd).
An exact proof term for the current goal is (total_function_on_graph K J (λk0 : set ⇒ k0 1) Hgphi).
We prove the intermediate claim Hgraphphi: functional_graph phi.
An exact proof term for the current goal is (functional_graph_graph K (λk0 : set ⇒ k0 1)).
We prove the intermediate claim Hdomphi: graph_domain_subset phi K.
An exact proof term for the current goal is (graph_domain_subset_graph K (λk0 : set ⇒ k0 1)).
We prove the intermediate claim Hmono: ∀i j : set, i ∈ K → j ∈ K → (i,j) ∈ leK → (apply_fun phi i,apply_fun phi j) ∈ le.
Let i and j be given.
Assume HiK: i ∈ K.
Assume HjK: j ∈ K.
Assume Hij: (i,j) ∈ leK.
We prove the intermediate claim Hle: ((i 1),(j 1)) ∈ le.
An exact proof term for the current goal is (andER ((j 0) ⊆ (i 0)) (((i 1),(j 1)) ∈ le) (pair_order_pred K le i j Hij)).
rewrite the current goal using (apply_fun_graph K (λk0 : set ⇒ k0 1) i HiK) (from left to right).
rewrite the current goal using (apply_fun_graph K (λk0 : set ⇒ k0 1) j HjK) (from left to right).
An exact proof term for the current goal is Hle.
We prove the intermediate claim Hcofinal: ∀j0 : set, j0 ∈ J → ∃k : set, k ∈ K ∧ (j0,apply_fun phi k) ∈ le.
Let j0 be given.
Assume Hj0: j0 ∈ J.
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HXN: X ∈ N.
An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ x ∈ U0) X HXTx HxX).
We prove the intermediate claim Hnetj0X: apply_fun net j0 ∈ X.
An exact proof term for the current goal is (Hfunnet j0 Hj0).
We prove the intermediate claim HkProd: (X,j0) ∈ setprod N J.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma N J X j0 HXN Hj0).
We prove the intermediate claim Hk_in: apply_fun net ((X,j0) 1) ∈ (X,j0) 0.
rewrite the current goal using (tuple_2_1_eq X j0) (from left to right).
rewrite the current goal using (tuple_2_0_eq X j0) (from left to right).
An exact proof term for the current goal is Hnetj0X.
We prove the intermediate claim HkK: (X,j0) ∈ K.
An exact proof term for the current goal is (SepI (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) (X,j0) HkProd Hk_in).
We use (X,j0) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HkK.
rewrite the current goal using (apply_fun_graph K (λk0 : set ⇒ k0 1) (X,j0) HkK) (from left to right).
rewrite the current goal using (tuple_2_1_eq X j0) (from left to right).
An exact proof term for the current goal is (Hrefl j0 Hj0).
We prove the intermediate claim Hvals: ∀k : set, k ∈ K → apply_fun sub k = apply_fun net (apply_fun phi k).
Let k be given.
Assume HkK: k ∈ K.
rewrite the current goal using (apply_fun_graph K (λk0 : set ⇒ apply_fun net (k0 1)) k HkK) (from left to right).
rewrite the current goal using (apply_fun_graph K (λk0 : set ⇒ k0 1) k HkK) (from left to right).
Use reflexivity.
We use K to witness the existential quantifier.
We use leK to witness the existential quantifier.
We use phi to witness the existential quantifier.
We use sub to witness the existential quantifier.
Apply andI to the current goal.
We will prove subnet_of_witness net sub J le K leK X phi.
An exact proof term for the current goal is (and14I (directed_set J le) (directed_set K leK) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) (total_function_on sub K X) (functional_graph sub) (graph_domain_subset sub K) (total_function_on phi K J) (functional_graph phi) (graph_domain_subset phi K) (∀i j : set, i ∈ K → j ∈ K → (i,j) ∈ leK → (apply_fun phi i,apply_fun phi j) ∈ le) (∀j : set, j ∈ J → ∃k : set, k ∈ K ∧ (j,apply_fun phi k) ∈ le) (∀k : set, k ∈ K → apply_fun sub k = apply_fun net (apply_fun phi k)) HdirJ HdirK Htotnet Hgraphnet Hdomnet Htotsub Hgraphsub Hdomsub Htotphi Hgraphphi Hdomphi Hmono Hcofinal Hvals).
We will prove net_converges_on X Tx sub K leK x.
We prove the intermediate claim Htail: ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun sub i ∈ U.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun sub i ∈ U.
We prove the intermediate claim HJne: J ≠ Empty.
An exact proof term for the current goal is (directed_set_nonempty J le HdirJ).
We prove the intermediate claim Hexj0: ∃j0 : set, j0 ∈ J.
An exact proof term for the current goal is (nonempty_has_element J HJne).
Apply Hexj0 to the current goal.
Let j0 be given.
Assume Hj0: j0 ∈ J.
We prove the intermediate claim Hexj: ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U.
An exact proof term for the current goal is (Hfreq U HU HxU j0 Hj0).
Apply Hexj to the current goal.
Let j be given.
Assume HjPack: j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U.
We prove the intermediate claim Hj_left: j ∈ J ∧ (j0,j) ∈ le.
An exact proof term for the current goal is (andEL (j ∈ J ∧ (j0,j) ∈ le) (apply_fun net j ∈ U) HjPack).
We prove the intermediate claim HjJ: j ∈ J.
An exact proof term for the current goal is (andEL (j ∈ J) ((j0,j) ∈ le) Hj_left).
We prove the intermediate claim HnetjU: apply_fun net j ∈ U.
An exact proof term for the current goal is (andER (j ∈ J ∧ (j0,j) ∈ le) (apply_fun net j ∈ U) HjPack).
We prove the intermediate claim HUN: U ∈ N.
An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ x ∈ U0) U HU HxU).
We prove the intermediate claim Hi0Prod: (U,j) ∈ setprod N J.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma N J U j HUN HjJ).
We prove the intermediate claim Hi0_in: apply_fun net ((U,j) 1) ∈ (U,j) 0.
rewrite the current goal using (tuple_2_1_eq U j) (from left to right).
rewrite the current goal using (tuple_2_0_eq U j) (from left to right).
An exact proof term for the current goal is HnetjU.
We prove the intermediate claim Hi0K: (U,j) ∈ K.
An exact proof term for the current goal is (SepI (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) (U,j) Hi0Prod Hi0_in).
We use (U,j) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0K.
Let i be given.
Assume HiK: i ∈ K.
Assume Hi0i: ((U,j),i) ∈ leK.
We will prove apply_fun sub i ∈ U.
We prove the intermediate claim Hiprod: i ∈ setprod N J.
An exact proof term for the current goal is (SepE1 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) i HiK).
We prove the intermediate claim Hinet: apply_fun net (i 1) ∈ i 0.
An exact proof term for the current goal is (SepE2 (setprod N J) (λp : set ⇒ apply_fun net (p 1) ∈ p 0) i HiK).
We prove the intermediate claim HsubU: (i 0) ⊆ ((U,j) 0).
An exact proof term for the current goal is (andEL ((i 0) ⊆ ((U,j) 0)) (((U,j) 1,(i 1)) ∈ le) (pair_order_pred K le (U,j) i Hi0i)).
We prove the intermediate claim HinetU: apply_fun net (i 1) ∈ ((U,j) 0).
An exact proof term for the current goal is (HsubU (apply_fun net (i 1)) Hinet).
rewrite the current goal using (apply_fun_graph K (λk0 : set ⇒ apply_fun net (k0 1)) i HiK) (from left to right).
rewrite the current goal using (tuple_2_0_eq U j) (from right to left).
An exact proof term for the current goal is HinetU.
An exact proof term for the current goal is (and7I (topology_on X Tx) (directed_set K leK) (total_function_on sub K X) (functional_graph sub) (graph_domain_subset sub K) (x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun sub i ∈ U) HTx HdirK Htotsub Hgraphsub Hdomsub HxX Htail).
∎