Metamath Proof Explorer

Theorem cvmlift2lem10

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

Ref Expression
Hypotheses cvmlift2.b ⊢ 𝐵 = ∪ 𝐶
cvmlift2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift2.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
cvmlift2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmlift2.i ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
cvmlift2.h ⊢ 𝐻 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
cvmlift2.k ⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
cvmlift2lem10.s ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmlift2lem10.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 0 [,] 1 ) )
cvmlift2lem10.2 ⊢ ( 𝜑 → 𝑌 ∈ ( 0 [,] 1 ) )
Assertion cvmlift2lem10 ( 𝜑 → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢ 𝐵 = ∪ 𝐶
2 cvmlift2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
3 cvmlift2.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
4 cvmlift2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
5 cvmlift2.i ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
6 cvmlift2.h ⊢ 𝐻 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
7 cvmlift2.k ⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
8 cvmlift2lem10.s ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
9 cvmlift2lem10.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 0 [,] 1 ) )
10 cvmlift2lem10.2 ⊢ ( 𝜑 → 𝑌 ∈ ( 0 [,] 1 ) )
11 iitop ⊢ II ∈ Top
12 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
13 11 11 12 12 txunii ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ∪ ( II ×t II )
14 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
15 13 14 cnf ⊢ ( 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) → 𝐺 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ∪ 𝐽 )
16 3 15 syl ⊢ ( 𝜑 → 𝐺 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ∪ 𝐽 )
17 9 10 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
18 16 17 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ ∪ 𝐽 )
19 8 14 cvmcov ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ ∪ 𝐽 ) → ∃ 𝑚 ∈ 𝐽 ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ ( 𝑆 ‘ 𝑚 ) ≠ ∅ ) )
20 2 18 19 syl2anc ⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝐽 ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ ( 𝑆 ‘ 𝑚 ) ≠ ∅ ) )
21 n0 ⊢ ( ( 𝑆 ‘ 𝑚 ) ≠ ∅ ↔ ∃ 𝑡 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) )
22 eleq1 ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝑧 ∈ ( 𝑎 × 𝑏 ) ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑎 × 𝑏 ) ) )
23 opelxp ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑎 × 𝑏 ) ↔ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) )
24 22 23 bitrdi ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝑧 ∈ ( 𝑎 × 𝑏 ) ↔ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ) )
25 24 anbi1d ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( ( 𝑧 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ↔ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) )
26 25 2rexbidv ⊢ ( 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ → ( ∃ 𝑎 ∈ II ∃ 𝑏 ∈ II ( 𝑧 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ↔ ∃ 𝑎 ∈ II ∃ 𝑏 ∈ II ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) )
27 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
28 8 cvmsrcl ⊢ ( 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) → 𝑚 ∈ 𝐽 )
29 28 ad2antll ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → 𝑚 ∈ 𝐽 )
30 cnima ⊢ ( ( 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) ∧ 𝑚 ∈ 𝐽 ) → ( ◡ 𝐺 “ 𝑚 ) ∈ ( II ×t II ) )
31 27 29 30 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ( ◡ 𝐺 “ 𝑚 ) ∈ ( II ×t II ) )
32 eltx ⊢ ( ( II ∈ Top ∧ II ∈ Top ) → ( ( ◡ 𝐺 “ 𝑚 ) ∈ ( II ×t II ) ↔ ∀ 𝑧 ∈ ( ◡ 𝐺 “ 𝑚 ) ∃ 𝑎 ∈ II ∃ 𝑏 ∈ II ( 𝑧 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) )
33 11 11 32 mp2an ⊢ ( ( ◡ 𝐺 “ 𝑚 ) ∈ ( II ×t II ) ↔ ∀ 𝑧 ∈ ( ◡ 𝐺 “ 𝑚 ) ∃ 𝑎 ∈ II ∃ 𝑏 ∈ II ( 𝑧 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) )
34 31 33 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ∀ 𝑧 ∈ ( ◡ 𝐺 “ 𝑚 ) ∃ 𝑎 ∈ II ∃ 𝑏 ∈ II ( 𝑧 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) )
35 17 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
36 simprl ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 )
37 16 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → 𝐺 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ∪ 𝐽 )
38 ffn ⊢ ( 𝐺 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ∪ 𝐽 → 𝐺 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
39 elpreima ⊢ ( 𝐺 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ◡ 𝐺 “ 𝑚 ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∧ ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ) ) )
40 37 38 39 3syl ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ◡ 𝐺 “ 𝑚 ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∧ ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ) ) )
41 35 36 40 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ◡ 𝐺 “ 𝑚 ) )
42 26 34 41 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ∃ 𝑎 ∈ II ∃ 𝑏 ∈ II ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) )
43 iillysconn ⊢ II ∈ Locally SConn
44 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → 𝑎 ∈ II )
45 simprll ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → 𝑋 ∈ 𝑎 )
46 llyi ⊢ ( ( II ∈ Locally SConn ∧ 𝑎 ∈ II ∧ 𝑋 ∈ 𝑎 ) → ∃ 𝑢 ∈ II ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) )
47 43 44 45 46 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ∃ 𝑢 ∈ II ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) )
48 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → 𝑏 ∈ II )
49 simprlr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → 𝑌 ∈ 𝑏 )
50 llyi ⊢ ( ( II ∈ Locally SConn ∧ 𝑏 ∈ II ∧ 𝑌 ∈ 𝑏 ) → ∃ 𝑣 ∈ II ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) )
51 43 48 49 50 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ∃ 𝑣 ∈ II ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) )
52 reeanv ⊢ ( ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ↔ ( ∃ 𝑢 ∈ II ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ∃ 𝑣 ∈ II ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) )
53 simpl2 ⊢ ( ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → 𝑋 ∈ 𝑢 )
54 53 a1i ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ( ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → 𝑋 ∈ 𝑢 ) )
55 simpr2 ⊢ ( ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → 𝑌 ∈ 𝑣 )
56 55 a1i ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ( ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → 𝑌 ∈ 𝑣 ) )
57 simprl1 ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) ∧ ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → 𝑢 ⊆ 𝑎 )
58 simprr1 ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) ∧ ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → 𝑣 ⊆ 𝑏 )
59 xpss12 ⊢ ( ( 𝑢 ⊆ 𝑎 ∧ 𝑣 ⊆ 𝑏 ) → ( 𝑢 × 𝑣 ) ⊆ ( 𝑎 × 𝑏 ) )
60 57 58 59 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) ∧ ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → ( 𝑢 × 𝑣 ) ⊆ ( 𝑎 × 𝑏 ) )
61 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) ∧ ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) )
62 60 61 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) ∧ ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) )
63 62 ex ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ( ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) )
64 54 56 63 3jcad ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ( ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) )
65 simp3 ⊢ ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) → ( II ↾t 𝑢 ) ∈ SConn )
66 simp3 ⊢ ( ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) → ( II ↾t 𝑣 ) ∈ SConn )
67 65 66 anim12i ⊢ ( ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) )
68 64 67 jca2 ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ( ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) )
69 68 reximdv ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ( ∃ 𝑣 ∈ II ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ∃ 𝑣 ∈ II ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) )
70 69 reximdv ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ( ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) )
71 52 70 syl5bir ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ( ( ∃ 𝑢 ∈ II ( 𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ ( II ↾t 𝑢 ) ∈ SConn ) ∧ ∃ 𝑣 ∈ II ( 𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) )
72 47 51 71 mp2and ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) ∧ ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) )
73 72 ex ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑎 ∈ II ∧ 𝑏 ∈ II ) ) → ( ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) )
74 73 rexlimdvva ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ( ∃ 𝑎 ∈ II ∃ 𝑏 ∈ II ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) )
75 42 74 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) )
76 simp3l1 ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → 𝑋 ∈ 𝑢 )
77 simp3l2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → 𝑌 ∈ 𝑣 )
78 simpl1l ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝜑 )
79 78 2 syl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
80 78 3 syl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
81 78 4 syl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝑃 ∈ 𝐵 )
82 78 5 syl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
83 df-ov ⊢ ( 𝑋 𝐺 𝑌 ) = ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
84 simpl1r ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) )
85 84 simpld ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 )
86 83 85 eqeltrid ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( 𝑋 𝐺 𝑌 ) ∈ 𝑚 )
87 84 simprd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) )
88 simpl2l ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝑢 ∈ II )
89 simpl2r ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝑣 ∈ II )
90 simp3rl ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → ( II ↾t 𝑢 ) ∈ SConn )
91 90 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( II ↾t 𝑢 ) ∈ SConn )
92 sconnpconn ⊢ ( ( II ↾t 𝑢 ) ∈ SConn → ( II ↾t 𝑢 ) ∈ PConn )
93 pconnconn ⊢ ( ( II ↾t 𝑢 ) ∈ PConn → ( II ↾t 𝑢 ) ∈ Conn )
94 91 92 93 3syl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( II ↾t 𝑢 ) ∈ Conn )
95 simp3rr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → ( II ↾t 𝑣 ) ∈ SConn )
96 95 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( II ↾t 𝑣 ) ∈ SConn )
97 sconnpconn ⊢ ( ( II ↾t 𝑣 ) ∈ SConn → ( II ↾t 𝑣 ) ∈ PConn )
98 pconnconn ⊢ ( ( II ↾t 𝑣 ) ∈ PConn → ( II ↾t 𝑣 ) ∈ Conn )
99 96 97 98 3syl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( II ↾t 𝑣 ) ∈ Conn )
100 76 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝑋 ∈ 𝑢 )
101 77 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝑌 ∈ 𝑣 )
102 simp3l3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) )
103 102 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) )
104 simprl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → 𝑤 ∈ 𝑣 )
105 simprr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) )
106 eqid ⊢ ( ℩ 𝑏 ∈ 𝑡 ( 𝑋 𝐾 𝑌 ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ 𝑡 ( 𝑋 𝐾 𝑌 ) ∈ 𝑏 )
107 1 79 80 81 82 6 7 8 86 87 88 89 94 99 100 101 103 104 105 106 cvmlift2lem9 ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) ∧ ( 𝑤 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) )
108 107 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) )
109 76 77 108 3jca ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ∧ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) ) → ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) )
110 109 3expia ⊢ ( ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) → ( ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) )
111 110 reximdvva ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ( ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐺 “ 𝑚 ) ) ∧ ( ( II ↾t 𝑢 ) ∈ SConn ∧ ( II ↾t 𝑣 ) ∈ SConn ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) )
112 75 111 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) )
113 112 expr ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ) → ( 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) )
114 113 exlimdv ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ) → ( ∃ 𝑡 𝑡 ∈ ( 𝑆 ‘ 𝑚 ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) )
115 21 114 syl5bi ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ) → ( ( 𝑆 ‘ 𝑚 ) ≠ ∅ → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) )
116 115 expimpd ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ ( 𝑆 ‘ 𝑚 ) ≠ ∅ ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) )
117 116 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝐽 ( ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑚 ∧ ( 𝑆 ‘ 𝑚 ) ≠ ∅ ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) )
118 20 117 mpd ⊢ ( 𝜑 → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) )