# Metamath Proof Explorer

## Theorem cvmlift2lem10

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-2015)

Ref Expression
Hypotheses cvmlift2.b ${⊢}{B}=\bigcup {C}$
cvmlift2.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
cvmlift2.g ${⊢}{\phi }\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
cvmlift2.p ${⊢}{\phi }\to {P}\in {B}$
cvmlift2.i ${⊢}{\phi }\to {F}\left({P}\right)=0{G}0$
cvmlift2.h ${⊢}{H}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {f}\left(0\right)={P}\right)\right)$
cvmlift2.k ${⊢}{K}=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({x}\right)\right)\right)\left({y}\right)\right)$
cvmlift2lem10.s ${⊢}{S}=\left({k}\in {J}⟼\left\{{s}\in \left(𝒫{C}\setminus \left\{\varnothing \right\}\right)|\left(\bigcup {s}={{F}}^{-1}\left[{k}\right]\wedge \forall {c}\in {s}\phantom{\rule{.4em}{0ex}}\left(\forall {d}\in \left({s}\setminus \left\{{c}\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\cap {d}=\varnothing \wedge {{F}↾}_{{c}}\in \left(\left({C}{↾}_{𝑡}{c}\right)\mathrm{Homeo}\left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)\right\}\right)$
cvmlift2lem10.1 ${⊢}{\phi }\to {X}\in \left[0,1\right]$
cvmlift2lem10.2 ${⊢}{\phi }\to {Y}\in \left[0,1\right]$
Assertion cvmlift2lem10 ${⊢}{\phi }\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 cvmlift2.b ${⊢}{B}=\bigcup {C}$
2 cvmlift2.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
3 cvmlift2.g ${⊢}{\phi }\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
4 cvmlift2.p ${⊢}{\phi }\to {P}\in {B}$
5 cvmlift2.i ${⊢}{\phi }\to {F}\left({P}\right)=0{G}0$
6 cvmlift2.h ${⊢}{H}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {f}\left(0\right)={P}\right)\right)$
7 cvmlift2.k ${⊢}{K}=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({x}\right)\right)\right)\left({y}\right)\right)$
8 cvmlift2lem10.s ${⊢}{S}=\left({k}\in {J}⟼\left\{{s}\in \left(𝒫{C}\setminus \left\{\varnothing \right\}\right)|\left(\bigcup {s}={{F}}^{-1}\left[{k}\right]\wedge \forall {c}\in {s}\phantom{\rule{.4em}{0ex}}\left(\forall {d}\in \left({s}\setminus \left\{{c}\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\cap {d}=\varnothing \wedge {{F}↾}_{{c}}\in \left(\left({C}{↾}_{𝑡}{c}\right)\mathrm{Homeo}\left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)\right\}\right)$
9 cvmlift2lem10.1 ${⊢}{\phi }\to {X}\in \left[0,1\right]$
10 cvmlift2lem10.2 ${⊢}{\phi }\to {Y}\in \left[0,1\right]$
11 iitop ${⊢}\mathrm{II}\in \mathrm{Top}$
12 iiuni ${⊢}\left[0,1\right]=\bigcup \mathrm{II}$
13 11 11 12 12 txunii ${⊢}\left[0,1\right]×\left[0,1\right]=\bigcup \left(\mathrm{II}{×}_{t}\mathrm{II}\right)$
14 eqid ${⊢}\bigcup {J}=\bigcup {J}$
15 13 14 cnf ${⊢}{G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)\to {G}:\left[0,1\right]×\left[0,1\right]⟶\bigcup {J}$
16 3 15 syl ${⊢}{\phi }\to {G}:\left[0,1\right]×\left[0,1\right]⟶\bigcup {J}$
17 9 10 opelxpd ${⊢}{\phi }\to ⟨{X},{Y}⟩\in \left(\left[0,1\right]×\left[0,1\right]\right)$
18 16 17 ffvelrnd ${⊢}{\phi }\to {G}\left(⟨{X},{Y}⟩\right)\in \bigcup {J}$
19 8 14 cvmcov ${⊢}\left({F}\in \left({C}\mathrm{CovMap}{J}\right)\wedge {G}\left(⟨{X},{Y}⟩\right)\in \bigcup {J}\right)\to \exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {S}\left({m}\right)\ne \varnothing \right)$
20 2 18 19 syl2anc ${⊢}{\phi }\to \exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {S}\left({m}\right)\ne \varnothing \right)$
21 n0 ${⊢}{S}\left({m}\right)\ne \varnothing ↔\exists {t}\phantom{\rule{.4em}{0ex}}{t}\in {S}\left({m}\right)$
22 eleq1 ${⊢}{z}=⟨{X},{Y}⟩\to \left({z}\in \left({a}×{b}\right)↔⟨{X},{Y}⟩\in \left({a}×{b}\right)\right)$
23 opelxp ${⊢}⟨{X},{Y}⟩\in \left({a}×{b}\right)↔\left({X}\in {a}\wedge {Y}\in {b}\right)$
24 22 23 syl6bb ${⊢}{z}=⟨{X},{Y}⟩\to \left({z}\in \left({a}×{b}\right)↔\left({X}\in {a}\wedge {Y}\in {b}\right)\right)$
25 24 anbi1d ${⊢}{z}=⟨{X},{Y}⟩\to \left(\left({z}\in \left({a}×{b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)↔\left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)$
26 25 2rexbidv ${⊢}{z}=⟨{X},{Y}⟩\to \left(\exists {a}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({a}×{b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)↔\exists {a}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)$
27 3 adantr ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
28 8 cvmsrcl ${⊢}{t}\in {S}\left({m}\right)\to {m}\in {J}$
29 28 ad2antll ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to {m}\in {J}$
30 cnima ${⊢}\left({G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)\wedge {m}\in {J}\right)\to {{G}}^{-1}\left[{m}\right]\in \left(\mathrm{II}{×}_{t}\mathrm{II}\right)$
31 27 29 30 syl2anc ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to {{G}}^{-1}\left[{m}\right]\in \left(\mathrm{II}{×}_{t}\mathrm{II}\right)$
32 eltx ${⊢}\left(\mathrm{II}\in \mathrm{Top}\wedge \mathrm{II}\in \mathrm{Top}\right)\to \left({{G}}^{-1}\left[{m}\right]\in \left(\mathrm{II}{×}_{t}\mathrm{II}\right)↔\forall {z}\in {{G}}^{-1}\left[{m}\right]\phantom{\rule{.4em}{0ex}}\exists {a}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({a}×{b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)$
33 11 11 32 mp2an ${⊢}{{G}}^{-1}\left[{m}\right]\in \left(\mathrm{II}{×}_{t}\mathrm{II}\right)↔\forall {z}\in {{G}}^{-1}\left[{m}\right]\phantom{\rule{.4em}{0ex}}\exists {a}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({a}×{b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)$
34 31 33 sylib ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to \forall {z}\in {{G}}^{-1}\left[{m}\right]\phantom{\rule{.4em}{0ex}}\exists {a}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({a}×{b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)$
35 17 adantr ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to ⟨{X},{Y}⟩\in \left(\left[0,1\right]×\left[0,1\right]\right)$
36 simprl ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to {G}\left(⟨{X},{Y}⟩\right)\in {m}$
37 16 adantr ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to {G}:\left[0,1\right]×\left[0,1\right]⟶\bigcup {J}$
38 ffn ${⊢}{G}:\left[0,1\right]×\left[0,1\right]⟶\bigcup {J}\to {G}Fn\left(\left[0,1\right]×\left[0,1\right]\right)$
39 elpreima ${⊢}{G}Fn\left(\left[0,1\right]×\left[0,1\right]\right)\to \left(⟨{X},{Y}⟩\in {{G}}^{-1}\left[{m}\right]↔\left(⟨{X},{Y}⟩\in \left(\left[0,1\right]×\left[0,1\right]\right)\wedge {G}\left(⟨{X},{Y}⟩\right)\in {m}\right)\right)$
40 37 38 39 3syl ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to \left(⟨{X},{Y}⟩\in {{G}}^{-1}\left[{m}\right]↔\left(⟨{X},{Y}⟩\in \left(\left[0,1\right]×\left[0,1\right]\right)\wedge {G}\left(⟨{X},{Y}⟩\right)\in {m}\right)\right)$
41 35 36 40 mpbir2and ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to ⟨{X},{Y}⟩\in {{G}}^{-1}\left[{m}\right]$
42 26 34 41 rspcdva ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to \exists {a}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)$
43 iillysconn ${⊢}\mathrm{II}\in Locally\mathrm{SConn}$
44 simplrl ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to {a}\in \mathrm{II}$
45 simprll ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to {X}\in {a}$
46 llyi ${⊢}\left(\mathrm{II}\in Locally\mathrm{SConn}\wedge {a}\in \mathrm{II}\wedge {X}\in {a}\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\right)$
47 43 44 45 46 mp3an2i ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)$
48 simplrr ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to {b}\in \mathrm{II}$
49 simprlr ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to {Y}\in {b}$
50 llyi ${⊢}\left(\mathrm{II}\in Locally\mathrm{SConn}\wedge {b}\in \mathrm{II}\wedge {Y}\in {b}\to \exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\right)$
51 43 48 49 50 mp3an2i ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)$
52 reeanv ${⊢}\exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)↔\left(\exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)$
53 simpl2 ${⊢}\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to {X}\in {u}$
54 53 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \left(\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to {X}\in {u}\right)$
55 simpr2 ${⊢}\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to {Y}\in {v}$
56 55 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \left(\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to {Y}\in {v}\right)$
57 simprl1 ${⊢}\left(\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\wedge \left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to {u}\subseteq {a}$
58 simprr1 ${⊢}\left(\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\wedge \left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to {v}\subseteq {b}$
59 xpss12 ${⊢}\left({u}\subseteq {a}\wedge {v}\subseteq {b}\right)\to {u}×{v}\subseteq {a}×{b}$
60 57 58 59 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\wedge \left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to {u}×{v}\subseteq {a}×{b}$
61 simplrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\wedge \left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]$
62 60 61 sstrd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\wedge \left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]$
63 62 ex ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \left(\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)$
64 54 56 63 3jcad ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \left(\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to \left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)$
65 simp3 ${⊢}\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\to \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}$
66 simp3 ${⊢}\left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\to \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}$
67 65 66 anim12i ${⊢}\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)$
68 64 67 jca2 ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \left(\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)$
69 68 reximdv ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \left(\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to \exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)$
70 69 reximdv ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \left(\exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)$
71 52 70 syl5bir ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \left(\left(\exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {a}\wedge {X}\in {u}\wedge \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\right)\wedge \exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {b}\wedge {Y}\in {v}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)$
72 47 51 71 mp2and ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\wedge \left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)$
73 72 ex ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({a}\in \mathrm{II}\wedge {b}\in \mathrm{II}\right)\right)\to \left(\left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)$
74 73 rexlimdvva ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to \left(\exists {a}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {a}\wedge {Y}\in {b}\right)\wedge {a}×{b}\subseteq {{G}}^{-1}\left[{m}\right]\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)$
75 42 74 mpd ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)$
76 simp3l1 ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to {X}\in {u}$
77 simp3l2 ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to {Y}\in {v}$
78 simpl1l ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {\phi }$
79 78 2 syl ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
80 78 3 syl ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
81 78 4 syl ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {P}\in {B}$
82 78 5 syl ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {F}\left({P}\right)=0{G}0$
83 df-ov ${⊢}{X}{G}{Y}={G}\left(⟨{X},{Y}⟩\right)$
84 simpl1r ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)$
85 84 simpld ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {G}\left(⟨{X},{Y}⟩\right)\in {m}$
86 83 85 eqeltrid ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {X}{G}{Y}\in {m}$
87 84 simprd ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {t}\in {S}\left({m}\right)$
88 simpl2l ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {u}\in \mathrm{II}$
89 simpl2r ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {v}\in \mathrm{II}$
90 simp3rl ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}$
91 90 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}$
92 sconnpconn ${⊢}\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\to \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{PConn}$
93 pconnconn ${⊢}\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{PConn}\to \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{Conn}$
94 91 92 93 3syl ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to \mathrm{II}{↾}_{𝑡}{u}\in \mathrm{Conn}$
95 simp3rr ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}$
96 95 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}$
97 sconnpconn ${⊢}\mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\to \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{PConn}$
98 pconnconn ${⊢}\mathrm{II}{↾}_{𝑡}{v}\in \mathrm{PConn}\to \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{Conn}$
99 96 97 98 3syl ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{Conn}$
100 76 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {X}\in {u}$
101 77 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {Y}\in {v}$
102 simp3l3 ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]$
103 102 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]$
104 simprl ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {w}\in {v}$
105 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)$
106 eqid ${⊢}\left(\iota {b}\in {t}|{X}{K}{Y}\in {b}\right)=\left(\iota {b}\in {t}|{X}{K}{Y}\in {b}\right)$
107 1 79 80 81 82 6 7 8 86 87 88 89 94 99 100 101 103 104 105 106 cvmlift2lem9 ${⊢}\left(\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\wedge \left({w}\in {v}\wedge {{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)$
108 107 rexlimdvaa ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)$
109 76 77 108 3jca ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\wedge \left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\right)\to \left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)$
110 109 3expia ${⊢}\left(\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\wedge \left({u}\in \mathrm{II}\wedge {v}\in \mathrm{II}\right)\right)\to \left(\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to \left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\right)$
111 110 reximdvva ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to \left(\exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {u}\wedge {Y}\in {v}\wedge {u}×{v}\subseteq {{G}}^{-1}\left[{m}\right]\right)\wedge \left(\mathrm{II}{↾}_{𝑡}{u}\in \mathrm{SConn}\wedge \mathrm{II}{↾}_{𝑡}{v}\in \mathrm{SConn}\right)\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\right)$
112 75 111 mpd ${⊢}\left({\phi }\wedge \left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {t}\in {S}\left({m}\right)\right)\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)$
113 112 expr ${⊢}\left({\phi }\wedge {G}\left(⟨{X},{Y}⟩\right)\in {m}\right)\to \left({t}\in {S}\left({m}\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\right)$
114 113 exlimdv ${⊢}\left({\phi }\wedge {G}\left(⟨{X},{Y}⟩\right)\in {m}\right)\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}{t}\in {S}\left({m}\right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\right)$
115 21 114 syl5bi ${⊢}\left({\phi }\wedge {G}\left(⟨{X},{Y}⟩\right)\in {m}\right)\to \left({S}\left({m}\right)\ne \varnothing \to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\right)$
116 115 expimpd ${⊢}{\phi }\to \left(\left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {S}\left({m}\right)\ne \varnothing \right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\right)$
117 116 rexlimdvw ${⊢}{\phi }\to \left(\exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({G}\left(⟨{X},{Y}⟩\right)\in {m}\wedge {S}\left({m}\right)\ne \varnothing \right)\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)\right)$
118 20 117 mpd ${⊢}{\phi }\to \exists {u}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{II}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge {Y}\in {v}\wedge \left(\exists {w}\in {v}\phantom{\rule{.4em}{0ex}}{{K}↾}_{\left({u}×\left\{{w}\right\}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×\left\{{w}\right\}\right)\right)\mathrm{Cn}{C}\right)\to {{K}↾}_{\left({u}×{v}\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left({u}×{v}\right)\right)\mathrm{Cn}{C}\right)\right)\right)$