Let X, Tx, N, S and x be given.
Assume HNspace: net_pack_in_space X N.
Assume HSspace: net_pack_in_space X S.
Assume Hsub: subnet_pack_of_in X N S.
Assume HconvN: net_pack_converges X Tx N x.
We will prove net_pack_converges X Tx S x.
Apply HconvN to the current goal.
Let J be given.
Assume Hexle: ∃le net : set, N = net_pack J le net ∧ net_converges_on X Tx net J le x.
Apply Hexle to the current goal.
Let le be given.
Assume Hexnet: ∃net : set, N = net_pack J le net ∧ net_converges_on X Tx net J le x.
Apply Hexnet to the current goal.
Let net be given.
Assume Hpair: N = net_pack J le net ∧ net_converges_on X Tx net J le x.
We prove the intermediate claim HNdef: N = net_pack J le net.
An exact proof term for the current goal is (andEL (N = net_pack J le net) (net_converges_on X Tx net J le x) Hpair).
We prove the intermediate claim HNconv: net_converges_on X Tx net J le x.
An exact proof term for the current goal is (andER (N = net_pack J le net) (net_converges_on X Tx net J le x) Hpair).
We prove the intermediate claim HNconvSel: net_converges_on X Tx (net_pack_fun N) (net_pack_index N) (net_pack_le N) x.
rewrite the current goal using HNdef (from left to right).
rewrite the current goal using (net_pack_fun_eq J le net) (from left to right).
rewrite the current goal using (net_pack_index_eq J le net) (from left to right).
rewrite the current goal using (net_pack_le_eq J le net) (from left to right).
An exact proof term for the current goal is HNconv.
We prove the intermediate claim HSconvSel: net_converges_on X Tx (net_pack_fun S) (net_pack_index S) (net_pack_le S) x.
An exact proof term for the current goal is (subnet_pack_of_in_preserves_net_converges_on X Tx N S x Hsub HNconvSel).
Apply HSspace to the current goal.
Let K be given.
Assume HexleS: ∃leS netS : set, S = net_pack K leS netS ∧ directed_set K leS ∧ total_function_on netS K X ∧ functional_graph netS ∧ graph_domain_subset netS K.
Apply HexleS to the current goal.
Let leS be given.
Assume HexnetS: ∃netS : set, S = net_pack K leS netS ∧ directed_set K leS ∧ total_function_on netS K X ∧ functional_graph netS ∧ graph_domain_subset netS K.
Apply HexnetS to the current goal.
Let netS be given.
Assume HSdata: S = net_pack K leS netS ∧ directed_set K leS ∧ total_function_on netS K X ∧ functional_graph netS ∧ graph_domain_subset netS K.
We prove the intermediate claim HSdef: S = net_pack K leS netS.
Apply (and5E (S = net_pack K leS netS) (directed_set K leS) (total_function_on netS K X) (functional_graph netS) (graph_domain_subset netS K) HSdata) to the current goal.
Assume HSdef0 HdirK HtotS HgraphS HdomS.
An exact proof term for the current goal is HSdef0.
We prove the intermediate claim HSconvDef: net_pack_converges X Tx S x = ∃J le net : set, S = net_pack J le net ∧ net_converges_on X Tx net J le x.
Use reflexivity.
rewrite the current goal using HSconvDef (from left to right).
We use K to witness the existential quantifier.
We use leS to witness the existential quantifier.
We use netS to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HSdef.
We prove the intermediate claim HSfun: net_pack_fun S = netS.
rewrite the current goal using HSdef (from left to right).
An exact proof term for the current goal is (net_pack_fun_eq K leS netS).
We prove the intermediate claim HSidx: net_pack_index S = K.
rewrite the current goal using HSdef (from left to right).
An exact proof term for the current goal is (net_pack_index_eq K leS netS).
We prove the intermediate claim HSle: net_pack_le S = leS.
rewrite the current goal using HSdef (from left to right).
An exact proof term for the current goal is (net_pack_le_eq K leS netS).
rewrite the current goal using HSfun (from right to left) at position 1.
rewrite the current goal using HSidx (from right to left) at position 1.
rewrite the current goal using HSle (from right to left) at position 1.
An exact proof term for the current goal is HSconvSel.
∎