Metamath Proof Explorer

Theorem cvmlift2lem9

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 𝑘 ) ) ) ) } )
cvmlift2lem9.1 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) ∈ 𝑀 )
cvmlift2lem9.2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑆 ‘ 𝑀 ) )
cvmlift2lem9.3 ⊢ ( 𝜑 → 𝑈 ∈ II )
cvmlift2lem9.4 ⊢ ( 𝜑 → 𝑉 ∈ II )
cvmlift2lem9.5 ⊢ ( 𝜑 → ( II ↾t 𝑈 ) ∈ Conn )
cvmlift2lem9.6 ⊢ ( 𝜑 → ( II ↾t 𝑉 ) ∈ Conn )
cvmlift2lem9.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
cvmlift2lem9.8 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
cvmlift2lem9.9 ⊢ ( 𝜑 → ( 𝑈 × 𝑉 ) ⊆ ( ◡ 𝐺 “ 𝑀 ) )
cvmlift2lem9.10 ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
cvmlift2lem9.11 ⊢ ( 𝜑 → ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) Cn 𝐶 ) )
cvmlift2lem9.w ⊢ 𝑊 = ( ℩ 𝑏 ∈ 𝑇 ( 𝑋 𝐾 𝑌 ) ∈ 𝑏 )
Assertion cvmlift2lem9 ( 𝜑 → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( 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 cvmlift2lem9.1 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) ∈ 𝑀 )
10 cvmlift2lem9.2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑆 ‘ 𝑀 ) )
11 cvmlift2lem9.3 ⊢ ( 𝜑 → 𝑈 ∈ II )
12 cvmlift2lem9.4 ⊢ ( 𝜑 → 𝑉 ∈ II )
13 cvmlift2lem9.5 ⊢ ( 𝜑 → ( II ↾t 𝑈 ) ∈ Conn )
14 cvmlift2lem9.6 ⊢ ( 𝜑 → ( II ↾t 𝑉 ) ∈ Conn )
15 cvmlift2lem9.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
16 cvmlift2lem9.8 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
17 cvmlift2lem9.9 ⊢ ( 𝜑 → ( 𝑈 × 𝑉 ) ⊆ ( ◡ 𝐺 “ 𝑀 ) )
18 cvmlift2lem9.10 ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
19 cvmlift2lem9.11 ⊢ ( 𝜑 → ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) Cn 𝐶 ) )
20 cvmlift2lem9.w ⊢ 𝑊 = ( ℩ 𝑏 ∈ 𝑇 ( 𝑋 𝐾 𝑌 ) ∈ 𝑏 )
21 iitop ⊢ II ∈ Top
22 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
23 21 21 22 22 txunii ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ∪ ( II ×t II )
24 1 2 3 4 5 6 7 cvmlift2lem5 ⊢ ( 𝜑 → 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
25 1 2 3 4 5 6 7 cvmlift2lem7 ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐾 ) = 𝐺 )
26 25 3 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐾 ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
27 21 21 txtopi ⊢ ( II ×t II ) ∈ Top
28 27 a1i ⊢ ( 𝜑 → ( II ×t II ) ∈ Top )
29 elssuni ⊢ ( 𝑈 ∈ II → 𝑈 ⊆ ∪ II )
30 29 22 sseqtrrdi ⊢ ( 𝑈 ∈ II → 𝑈 ⊆ ( 0 [,] 1 ) )
31 11 30 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( 0 [,] 1 ) )
32 31 15 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( 0 [,] 1 ) )
33 elssuni ⊢ ( 𝑉 ∈ II → 𝑉 ⊆ ∪ II )
34 33 22 sseqtrrdi ⊢ ( 𝑉 ∈ II → 𝑉 ⊆ ( 0 [,] 1 ) )
35 12 34 syl ⊢ ( 𝜑 → 𝑉 ⊆ ( 0 [,] 1 ) )
36 35 16 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ( 0 [,] 1 ) )
37 opelxpi ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 ∈ ( 0 [,] 1 ) ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
38 32 36 37 syl2anc ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
39 24 32 36 fovrnd ⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) ∈ 𝐵 )
40 fvco3 ⊢ ( ( 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( ( 𝐹 ∘ 𝐾 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝐹 ‘ ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
41 24 38 40 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐾 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝐹 ‘ ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
42 25 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐾 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
43 41 42 eqtr3d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
44 df-ov ⊢ ( 𝑋 𝐾 𝑌 ) = ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
45 44 fveq2i ⊢ ( 𝐹 ‘ ( 𝑋 𝐾 𝑌 ) ) = ( 𝐹 ‘ ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
46 df-ov ⊢ ( 𝑋 𝐺 𝑌 ) = ( 𝐺 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
47 43 45 46 3eqtr4g ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 𝐾 𝑌 ) ) = ( 𝑋 𝐺 𝑌 ) )
48 47 9 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 𝐾 𝑌 ) ) ∈ 𝑀 )
49 8 1 20 cvmsiota ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑀 ) ∧ ( 𝑋 𝐾 𝑌 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝑋 𝐾 𝑌 ) ) ∈ 𝑀 ) ) → ( 𝑊 ∈ 𝑇 ∧ ( 𝑋 𝐾 𝑌 ) ∈ 𝑊 ) )
50 2 10 39 48 49 syl13anc ⊢ ( 𝜑 → ( 𝑊 ∈ 𝑇 ∧ ( 𝑋 𝐾 𝑌 ) ∈ 𝑊 ) )
51 44 eleq1i ⊢ ( ( 𝑋 𝐾 𝑌 ) ∈ 𝑊 ↔ ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑊 )
52 51 anbi2i ⊢ ( ( 𝑊 ∈ 𝑇 ∧ ( 𝑋 𝐾 𝑌 ) ∈ 𝑊 ) ↔ ( 𝑊 ∈ 𝑇 ∧ ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑊 ) )
53 50 52 sylib ⊢ ( 𝜑 → ( 𝑊 ∈ 𝑇 ∧ ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑊 ) )
54 xpss12 ⊢ ( ( 𝑈 ⊆ ( 0 [,] 1 ) ∧ 𝑉 ⊆ ( 0 [,] 1 ) ) → ( 𝑈 × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
55 31 35 54 syl2anc ⊢ ( 𝜑 → ( 𝑈 × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
56 snidg ⊢ ( 𝑚 ∈ 𝑈 → 𝑚 ∈ { 𝑚 } )
57 56 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑚 ∈ { 𝑚 } )
58 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑛 ∈ 𝑉 )
59 ovres ⊢ ( ( 𝑚 ∈ { 𝑚 } ∧ 𝑛 ∈ 𝑉 ) → ( 𝑚 ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) 𝑛 ) = ( 𝑚 𝐾 𝑛 ) )
60 57 58 59 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝑚 ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) 𝑛 ) = ( 𝑚 𝐾 𝑛 ) )
61 eqid ⊢ ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) = ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) )
62 21 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → II ∈ Top )
63 snex ⊢ { 𝑚 } ∈ V
64 63 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → { 𝑚 } ∈ V )
65 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑉 ∈ II )
66 txrest ⊢ ( ( ( II ∈ Top ∧ II ∈ Top ) ∧ ( { 𝑚 } ∈ V ∧ 𝑉 ∈ II ) ) → ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) = ( ( II ↾t { 𝑚 } ) ×t ( II ↾t 𝑉 ) ) )
67 62 62 64 65 66 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) = ( ( II ↾t { 𝑚 } ) ×t ( II ↾t 𝑉 ) ) )
68 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
69 31 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑈 ) → 𝑚 ∈ ( 0 [,] 1 ) )
70 69 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑚 ∈ ( 0 [,] 1 ) )
71 restsn2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝑚 ∈ ( 0 [,] 1 ) ) → ( II ↾t { 𝑚 } ) = 𝒫 { 𝑚 } )
72 68 70 71 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( II ↾t { 𝑚 } ) = 𝒫 { 𝑚 } )
73 pwsn ⊢ 𝒫 { 𝑚 } = { ∅ , { 𝑚 } }
74 indisconn ⊢ { ∅ , { 𝑚 } } ∈ Conn
75 73 74 eqeltri ⊢ 𝒫 { 𝑚 } ∈ Conn
76 72 75 eqeltrdi ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( II ↾t { 𝑚 } ) ∈ Conn )
77 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( II ↾t 𝑉 ) ∈ Conn )
78 txconn ⊢ ( ( ( II ↾t { 𝑚 } ) ∈ Conn ∧ ( II ↾t 𝑉 ) ∈ Conn ) → ( ( II ↾t { 𝑚 } ) ×t ( II ↾t 𝑉 ) ) ∈ Conn )
79 76 77 78 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( II ↾t { 𝑚 } ) ×t ( II ↾t 𝑉 ) ) ∈ Conn )
80 67 79 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) ∈ Conn )
81 1 2 3 4 5 6 7 cvmlift2lem6 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ↾ ( { 𝑚 } × ( 0 [,] 1 ) ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) )
82 70 81 syldan ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 ↾ ( { 𝑚 } × ( 0 [,] 1 ) ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) )
83 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑉 ⊆ ( 0 [,] 1 ) )
84 xpss2 ⊢ ( 𝑉 ⊆ ( 0 [,] 1 ) → ( { 𝑚 } × 𝑉 ) ⊆ ( { 𝑚 } × ( 0 [,] 1 ) ) )
85 83 84 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑚 } × 𝑉 ) ⊆ ( { 𝑚 } × ( 0 [,] 1 ) ) )
86 70 snssd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → { 𝑚 } ⊆ ( 0 [,] 1 ) )
87 xpss1 ⊢ ( { 𝑚 } ⊆ ( 0 [,] 1 ) → ( { 𝑚 } × ( 0 [,] 1 ) ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
88 86 87 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑚 } × ( 0 [,] 1 ) ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
89 23 restuni ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( { 𝑚 } × ( 0 [,] 1 ) ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( { 𝑚 } × ( 0 [,] 1 ) ) = ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) )
90 27 88 89 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑚 } × ( 0 [,] 1 ) ) = ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) )
91 85 90 sseqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑚 } × 𝑉 ) ⊆ ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) )
92 eqid ⊢ ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) = ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) )
93 92 cnrest ⊢ ( ( ( 𝐾 ↾ ( { 𝑚 } × ( 0 [,] 1 ) ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) ∧ ( { 𝑚 } × 𝑉 ) ⊆ ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) ) → ( ( 𝐾 ↾ ( { 𝑚 } × ( 0 [,] 1 ) ) ) ↾ ( { 𝑚 } × 𝑉 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn 𝐶 ) )
94 82 91 93 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( 𝐾 ↾ ( { 𝑚 } × ( 0 [,] 1 ) ) ) ↾ ( { 𝑚 } × 𝑉 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn 𝐶 ) )
95 85 resabs1d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( 𝐾 ↾ ( { 𝑚 } × ( 0 [,] 1 ) ) ) ↾ ( { 𝑚 } × 𝑉 ) ) = ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) )
96 27 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( II ×t II ) ∈ Top )
97 ovex ⊢ ( 0 [,] 1 ) ∈ V
98 63 97 xpex ⊢ ( { 𝑚 } × ( 0 [,] 1 ) ) ∈ V
99 98 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑚 } × ( 0 [,] 1 ) ) ∈ V )
100 restabs ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( { 𝑚 } × 𝑉 ) ⊆ ( { 𝑚 } × ( 0 [,] 1 ) ) ∧ ( { 𝑚 } × ( 0 [,] 1 ) ) ∈ V ) → ( ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑚 } × 𝑉 ) ) = ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) )
101 96 85 99 100 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑚 } × 𝑉 ) ) = ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) )
102 101 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( ( ( II ×t II ) ↾t ( { 𝑚 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn 𝐶 ) = ( ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn 𝐶 ) )
103 94 95 102 3eltr3d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn 𝐶 ) )
104 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
105 2 104 syl ⊢ ( 𝜑 → 𝐶 ∈ Top )
106 105 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝐶 ∈ Top )
107 1 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
108 106 107 sylib ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
109 df-ima ⊢ ( 𝐾 “ ( { 𝑚 } × 𝑉 ) ) = ran ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) )
110 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑚 ∈ 𝑈 )
111 110 snssd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → { 𝑚 } ⊆ 𝑈 )
112 xpss1 ⊢ ( { 𝑚 } ⊆ 𝑈 → ( { 𝑚 } × 𝑉 ) ⊆ ( 𝑈 × 𝑉 ) )
113 imass2 ⊢ ( ( { 𝑚 } × 𝑉 ) ⊆ ( 𝑈 × 𝑉 ) → ( 𝐾 “ ( { 𝑚 } × 𝑉 ) ) ⊆ ( 𝐾 “ ( 𝑈 × 𝑉 ) ) )
114 111 112 113 3syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 “ ( { 𝑚 } × 𝑉 ) ) ⊆ ( 𝐾 “ ( 𝑈 × 𝑉 ) ) )
115 imaco ⊢ ( ( ◡ 𝐾 ∘ ◡ 𝐹 ) “ 𝑀 ) = ( ◡ 𝐾 “ ( ◡ 𝐹 “ 𝑀 ) )
116 cnvco ⊢ ◡ ( 𝐹 ∘ 𝐾 ) = ( ◡ 𝐾 ∘ ◡ 𝐹 )
117 25 cnveqd ⊢ ( 𝜑 → ◡ ( 𝐹 ∘ 𝐾 ) = ◡ 𝐺 )
118 116 117 eqtr3id ⊢ ( 𝜑 → ( ◡ 𝐾 ∘ ◡ 𝐹 ) = ◡ 𝐺 )
119 118 imaeq1d ⊢ ( 𝜑 → ( ( ◡ 𝐾 ∘ ◡ 𝐹 ) “ 𝑀 ) = ( ◡ 𝐺 “ 𝑀 ) )
120 115 119 eqtr3id ⊢ ( 𝜑 → ( ◡ 𝐾 “ ( ◡ 𝐹 “ 𝑀 ) ) = ( ◡ 𝐺 “ 𝑀 ) )
121 17 120 sseqtrrd ⊢ ( 𝜑 → ( 𝑈 × 𝑉 ) ⊆ ( ◡ 𝐾 “ ( ◡ 𝐹 “ 𝑀 ) ) )
122 24 ffund ⊢ ( 𝜑 → Fun 𝐾 )
123 24 fdmd ⊢ ( 𝜑 → dom 𝐾 = ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
124 55 123 sseqtrrd ⊢ ( 𝜑 → ( 𝑈 × 𝑉 ) ⊆ dom 𝐾 )
125 funimass3 ⊢ ( ( Fun 𝐾 ∧ ( 𝑈 × 𝑉 ) ⊆ dom 𝐾 ) → ( ( 𝐾 “ ( 𝑈 × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) ↔ ( 𝑈 × 𝑉 ) ⊆ ( ◡ 𝐾 “ ( ◡ 𝐹 “ 𝑀 ) ) ) )
126 122 124 125 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 “ ( 𝑈 × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) ↔ ( 𝑈 × 𝑉 ) ⊆ ( ◡ 𝐾 “ ( ◡ 𝐹 “ 𝑀 ) ) ) )
127 121 126 mpbird ⊢ ( 𝜑 → ( 𝐾 “ ( 𝑈 × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) )
128 127 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 “ ( 𝑈 × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) )
129 114 128 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 “ ( { 𝑚 } × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) )
130 109 129 eqsstrrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ran ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) )
131 cnvimass ⊢ ( ◡ 𝐹 “ 𝑀 ) ⊆ dom 𝐹
132 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
133 2 132 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
134 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
135 1 134 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
136 fdm ⊢ ( 𝐹 : 𝐵 ⟶ ∪ 𝐽 → dom 𝐹 = 𝐵 )
137 133 135 136 3syl ⊢ ( 𝜑 → dom 𝐹 = 𝐵 )
138 131 137 sseqtrid ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑀 ) ⊆ 𝐵 )
139 138 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ◡ 𝐹 “ 𝑀 ) ⊆ 𝐵 )
140 cnrest2 ⊢ ( ( 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ ran ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) ∧ ( ◡ 𝐹 “ 𝑀 ) ⊆ 𝐵 ) → ( ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) ) )
141 108 130 139 140 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) ) )
142 103 141 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) )
143 8 cvmsss ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑀 ) → 𝑇 ⊆ 𝐶 )
144 10 143 syl ⊢ ( 𝜑 → 𝑇 ⊆ 𝐶 )
145 50 simpld ⊢ ( 𝜑 → 𝑊 ∈ 𝑇 )
146 144 145 sseldd ⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
147 elssuni ⊢ ( 𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇 )
148 145 147 syl ⊢ ( 𝜑 → 𝑊 ⊆ ∪ 𝑇 )
149 8 cvmsuni ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑀 ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑀 ) )
150 10 149 syl ⊢ ( 𝜑 → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑀 ) )
151 148 150 sseqtrd ⊢ ( 𝜑 → 𝑊 ⊆ ( ◡ 𝐹 “ 𝑀 ) )
152 8 cvmsrcl ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑀 ) → 𝑀 ∈ 𝐽 )
153 10 152 syl ⊢ ( 𝜑 → 𝑀 ∈ 𝐽 )
154 cnima ⊢ ( ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ 𝑀 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝑀 ) ∈ 𝐶 )
155 133 153 154 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑀 ) ∈ 𝐶 )
156 restopn2 ⊢ ( ( 𝐶 ∈ Top ∧ ( ◡ 𝐹 “ 𝑀 ) ∈ 𝐶 ) → ( 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ↔ ( 𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ ( ◡ 𝐹 “ 𝑀 ) ) ) )
157 105 155 156 syl2anc ⊢ ( 𝜑 → ( 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ↔ ( 𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ ( ◡ 𝐹 “ 𝑀 ) ) ) )
158 146 151 157 mpbir2and ⊢ ( 𝜑 → 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) )
159 158 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) )
160 8 cvmscld ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑀 ) ∧ 𝑊 ∈ 𝑇 ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) )
161 2 10 145 160 syl3anc ⊢ ( 𝜑 → 𝑊 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) )
162 161 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) )
163 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑍 ∈ 𝑉 )
164 opelxpi ⊢ ( ( 𝑚 ∈ { 𝑚 } ∧ 𝑍 ∈ 𝑉 ) → ⟨ 𝑚 , 𝑍 ⟩ ∈ ( { 𝑚 } × 𝑉 ) )
165 57 163 164 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ⟨ 𝑚 , 𝑍 ⟩ ∈ ( { 𝑚 } × 𝑉 ) )
166 85 88 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑚 } × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
167 23 restuni ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( { 𝑚 } × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( { 𝑚 } × 𝑉 ) = ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) )
168 27 166 167 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑚 } × 𝑉 ) = ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) )
169 165 168 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ⟨ 𝑚 , 𝑍 ⟩ ∈ ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) )
170 df-ov ⊢ ( 𝑚 ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) 𝑍 ) = ( ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ‘ ⟨ 𝑚 , 𝑍 ⟩ )
171 ovres ⊢ ( ( 𝑚 ∈ { 𝑚 } ∧ 𝑍 ∈ 𝑉 ) → ( 𝑚 ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) 𝑍 ) = ( 𝑚 𝐾 𝑍 ) )
172 57 163 171 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝑚 ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) 𝑍 ) = ( 𝑚 𝐾 𝑍 ) )
173 snidg ⊢ ( 𝑍 ∈ 𝑉 → 𝑍 ∈ { 𝑍 } )
174 18 173 syl ⊢ ( 𝜑 → 𝑍 ∈ { 𝑍 } )
175 174 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑍 ∈ { 𝑍 } )
176 ovres ⊢ ( ( 𝑚 ∈ 𝑈 ∧ 𝑍 ∈ { 𝑍 } ) → ( 𝑚 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) = ( 𝑚 𝐾 𝑍 ) )
177 110 175 176 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝑚 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) = ( 𝑚 𝐾 𝑍 ) )
178 172 177 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝑚 ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) 𝑍 ) = ( 𝑚 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) )
179 170 178 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ‘ ⟨ 𝑚 , 𝑍 ⟩ ) = ( 𝑚 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) )
180 eqid ⊢ ∪ ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) = ∪ ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) )
181 21 a1i ⊢ ( 𝜑 → II ∈ Top )
182 snex ⊢ { 𝑍 } ∈ V
183 182 a1i ⊢ ( 𝜑 → { 𝑍 } ∈ V )
184 txrest ⊢ ( ( ( II ∈ Top ∧ II ∈ Top ) ∧ ( 𝑈 ∈ II ∧ { 𝑍 } ∈ V ) ) → ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) = ( ( II ↾t 𝑈 ) ×t ( II ↾t { 𝑍 } ) ) )
185 181 181 11 183 184 syl22anc ⊢ ( 𝜑 → ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) = ( ( II ↾t 𝑈 ) ×t ( II ↾t { 𝑍 } ) ) )
186 35 18 sseldd ⊢ ( 𝜑 → 𝑍 ∈ ( 0 [,] 1 ) )
187 restsn2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝑍 ∈ ( 0 [,] 1 ) ) → ( II ↾t { 𝑍 } ) = 𝒫 { 𝑍 } )
188 68 186 187 sylancr ⊢ ( 𝜑 → ( II ↾t { 𝑍 } ) = 𝒫 { 𝑍 } )
189 pwsn ⊢ 𝒫 { 𝑍 } = { ∅ , { 𝑍 } }
190 indisconn ⊢ { ∅ , { 𝑍 } } ∈ Conn
191 189 190 eqeltri ⊢ 𝒫 { 𝑍 } ∈ Conn
192 188 191 eqeltrdi ⊢ ( 𝜑 → ( II ↾t { 𝑍 } ) ∈ Conn )
193 txconn ⊢ ( ( ( II ↾t 𝑈 ) ∈ Conn ∧ ( II ↾t { 𝑍 } ) ∈ Conn ) → ( ( II ↾t 𝑈 ) ×t ( II ↾t { 𝑍 } ) ) ∈ Conn )
194 13 192 193 syl2anc ⊢ ( 𝜑 → ( ( II ↾t 𝑈 ) ×t ( II ↾t { 𝑍 } ) ) ∈ Conn )
195 185 194 eqeltrd ⊢ ( 𝜑 → ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) ∈ Conn )
196 105 107 sylib ⊢ ( 𝜑 → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
197 df-ima ⊢ ( 𝐾 “ ( 𝑈 × { 𝑍 } ) ) = ran ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) )
198 18 snssd ⊢ ( 𝜑 → { 𝑍 } ⊆ 𝑉 )
199 xpss2 ⊢ ( { 𝑍 } ⊆ 𝑉 → ( 𝑈 × { 𝑍 } ) ⊆ ( 𝑈 × 𝑉 ) )
200 imass2 ⊢ ( ( 𝑈 × { 𝑍 } ) ⊆ ( 𝑈 × 𝑉 ) → ( 𝐾 “ ( 𝑈 × { 𝑍 } ) ) ⊆ ( 𝐾 “ ( 𝑈 × 𝑉 ) ) )
201 198 199 200 3syl ⊢ ( 𝜑 → ( 𝐾 “ ( 𝑈 × { 𝑍 } ) ) ⊆ ( 𝐾 “ ( 𝑈 × 𝑉 ) ) )
202 201 127 sstrd ⊢ ( 𝜑 → ( 𝐾 “ ( 𝑈 × { 𝑍 } ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) )
203 197 202 eqsstrrid ⊢ ( 𝜑 → ran ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) )
204 cnrest2 ⊢ ( ( 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ ran ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) ∧ ( ◡ 𝐹 “ 𝑀 ) ⊆ 𝐵 ) → ( ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) ) )
205 196 203 138 204 syl3anc ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) ) )
206 19 205 mpbid ⊢ ( 𝜑 → ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) )
207 opelxpi ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ { 𝑍 } ) → ⟨ 𝑋 , 𝑍 ⟩ ∈ ( 𝑈 × { 𝑍 } ) )
208 15 174 207 syl2anc ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑍 ⟩ ∈ ( 𝑈 × { 𝑍 } ) )
209 186 snssd ⊢ ( 𝜑 → { 𝑍 } ⊆ ( 0 [,] 1 ) )
210 xpss12 ⊢ ( ( 𝑈 ⊆ ( 0 [,] 1 ) ∧ { 𝑍 } ⊆ ( 0 [,] 1 ) ) → ( 𝑈 × { 𝑍 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
211 31 209 210 syl2anc ⊢ ( 𝜑 → ( 𝑈 × { 𝑍 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
212 23 restuni ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( 𝑈 × { 𝑍 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( 𝑈 × { 𝑍 } ) = ∪ ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) )
213 27 211 212 sylancr ⊢ ( 𝜑 → ( 𝑈 × { 𝑍 } ) = ∪ ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) )
214 208 213 eleqtrd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑍 ⟩ ∈ ∪ ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) )
215 df-ov ⊢ ( 𝑋 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) = ( ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ‘ ⟨ 𝑋 , 𝑍 ⟩ )
216 ovres ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ { 𝑍 } ) → ( 𝑋 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) = ( 𝑋 𝐾 𝑍 ) )
217 15 174 216 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) = ( 𝑋 𝐾 𝑍 ) )
218 snidg ⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ { 𝑋 } )
219 15 218 syl ⊢ ( 𝜑 → 𝑋 ∈ { 𝑋 } )
220 ovres ⊢ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑍 ∈ 𝑉 ) → ( 𝑋 ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) 𝑍 ) = ( 𝑋 𝐾 𝑍 ) )
221 219 18 220 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) 𝑍 ) = ( 𝑋 𝐾 𝑍 ) )
222 217 221 eqtr4d ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) = ( 𝑋 ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) 𝑍 ) )
223 215 222 eqtr3id ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ‘ ⟨ 𝑋 , 𝑍 ⟩ ) = ( 𝑋 ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) 𝑍 ) )
224 eqid ⊢ ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) = ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) )
225 snex ⊢ { 𝑋 } ∈ V
226 225 a1i ⊢ ( 𝜑 → { 𝑋 } ∈ V )
227 txrest ⊢ ( ( ( II ∈ Top ∧ II ∈ Top ) ∧ ( { 𝑋 } ∈ V ∧ 𝑉 ∈ II ) ) → ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) = ( ( II ↾t { 𝑋 } ) ×t ( II ↾t 𝑉 ) ) )
228 181 181 226 12 227 syl22anc ⊢ ( 𝜑 → ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) = ( ( II ↾t { 𝑋 } ) ×t ( II ↾t 𝑉 ) ) )
229 restsn2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( II ↾t { 𝑋 } ) = 𝒫 { 𝑋 } )
230 68 32 229 sylancr ⊢ ( 𝜑 → ( II ↾t { 𝑋 } ) = 𝒫 { 𝑋 } )
231 pwsn ⊢ 𝒫 { 𝑋 } = { ∅ , { 𝑋 } }
232 indisconn ⊢ { ∅ , { 𝑋 } } ∈ Conn
233 231 232 eqeltri ⊢ 𝒫 { 𝑋 } ∈ Conn
234 230 233 eqeltrdi ⊢ ( 𝜑 → ( II ↾t { 𝑋 } ) ∈ Conn )
235 txconn ⊢ ( ( ( II ↾t { 𝑋 } ) ∈ Conn ∧ ( II ↾t 𝑉 ) ∈ Conn ) → ( ( II ↾t { 𝑋 } ) ×t ( II ↾t 𝑉 ) ) ∈ Conn )
236 234 14 235 syl2anc ⊢ ( 𝜑 → ( ( II ↾t { 𝑋 } ) ×t ( II ↾t 𝑉 ) ) ∈ Conn )
237 228 236 eqeltrd ⊢ ( 𝜑 → ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) ∈ Conn )
238 1 2 3 4 5 6 7 cvmlift2lem6 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) )
239 32 238 mpdan ⊢ ( 𝜑 → ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) )
240 xpss2 ⊢ ( 𝑉 ⊆ ( 0 [,] 1 ) → ( { 𝑋 } × 𝑉 ) ⊆ ( { 𝑋 } × ( 0 [,] 1 ) ) )
241 12 34 240 3syl ⊢ ( 𝜑 → ( { 𝑋 } × 𝑉 ) ⊆ ( { 𝑋 } × ( 0 [,] 1 ) ) )
242 32 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ ( 0 [,] 1 ) )
243 xpss1 ⊢ ( { 𝑋 } ⊆ ( 0 [,] 1 ) → ( { 𝑋 } × ( 0 [,] 1 ) ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
244 242 243 syl ⊢ ( 𝜑 → ( { 𝑋 } × ( 0 [,] 1 ) ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
245 23 restuni ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( { 𝑋 } × ( 0 [,] 1 ) ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( { 𝑋 } × ( 0 [,] 1 ) ) = ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) )
246 27 244 245 sylancr ⊢ ( 𝜑 → ( { 𝑋 } × ( 0 [,] 1 ) ) = ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) )
247 241 246 sseqtrd ⊢ ( 𝜑 → ( { 𝑋 } × 𝑉 ) ⊆ ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) )
248 eqid ⊢ ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) = ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) )
249 248 cnrest ⊢ ( ( ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) ∧ ( { 𝑋 } × 𝑉 ) ⊆ ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) ) → ( ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) ↾ ( { 𝑋 } × 𝑉 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn 𝐶 ) )
250 239 247 249 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) ↾ ( { 𝑋 } × 𝑉 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn 𝐶 ) )
251 241 resabs1d ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) ↾ ( { 𝑋 } × 𝑉 ) ) = ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) )
252 225 97 xpex ⊢ ( { 𝑋 } × ( 0 [,] 1 ) ) ∈ V
253 252 a1i ⊢ ( 𝜑 → ( { 𝑋 } × ( 0 [,] 1 ) ) ∈ V )
254 restabs ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( { 𝑋 } × 𝑉 ) ⊆ ( { 𝑋 } × ( 0 [,] 1 ) ) ∧ ( { 𝑋 } × ( 0 [,] 1 ) ) ∈ V ) → ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑋 } × 𝑉 ) ) = ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) )
255 28 241 253 254 syl3anc ⊢ ( 𝜑 → ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑋 } × 𝑉 ) ) = ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) )
256 255 oveq1d ⊢ ( 𝜑 → ( ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn 𝐶 ) = ( ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn 𝐶 ) )
257 250 251 256 3eltr3d ⊢ ( 𝜑 → ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn 𝐶 ) )
258 df-ima ⊢ ( 𝐾 “ ( { 𝑋 } × 𝑉 ) ) = ran ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) )
259 15 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑈 )
260 xpss1 ⊢ ( { 𝑋 } ⊆ 𝑈 → ( { 𝑋 } × 𝑉 ) ⊆ ( 𝑈 × 𝑉 ) )
261 imass2 ⊢ ( ( { 𝑋 } × 𝑉 ) ⊆ ( 𝑈 × 𝑉 ) → ( 𝐾 “ ( { 𝑋 } × 𝑉 ) ) ⊆ ( 𝐾 “ ( 𝑈 × 𝑉 ) ) )
262 259 260 261 3syl ⊢ ( 𝜑 → ( 𝐾 “ ( { 𝑋 } × 𝑉 ) ) ⊆ ( 𝐾 “ ( 𝑈 × 𝑉 ) ) )
263 262 127 sstrd ⊢ ( 𝜑 → ( 𝐾 “ ( { 𝑋 } × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) )
264 258 263 eqsstrrid ⊢ ( 𝜑 → ran ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) )
265 cnrest2 ⊢ ( ( 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ ran ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑀 ) ∧ ( ◡ 𝐹 “ 𝑀 ) ⊆ 𝐵 ) → ( ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) ) )
266 196 264 138 265 syl3anc ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) ) )
267 257 266 mpbid ⊢ ( 𝜑 → ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑀 ) ) ) )
268 opelxpi ⊢ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝑉 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 𝑋 } × 𝑉 ) )
269 219 16 268 syl2anc ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 𝑋 } × 𝑉 ) )
270 259 260 syl ⊢ ( 𝜑 → ( { 𝑋 } × 𝑉 ) ⊆ ( 𝑈 × 𝑉 ) )
271 270 55 sstrd ⊢ ( 𝜑 → ( { 𝑋 } × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
272 23 restuni ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( { 𝑋 } × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( { 𝑋 } × 𝑉 ) = ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) )
273 27 271 272 sylancr ⊢ ( 𝜑 → ( { 𝑋 } × 𝑉 ) = ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) )
274 269 273 eleqtrd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) )
275 df-ov ⊢ ( 𝑋 ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) 𝑌 ) = ( ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
276 ovres ⊢ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) 𝑌 ) = ( 𝑋 𝐾 𝑌 ) )
277 219 16 276 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) 𝑌 ) = ( 𝑋 𝐾 𝑌 ) )
278 275 277 eqtr3id ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝑋 𝐾 𝑌 ) )
279 50 simprd ⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) ∈ 𝑊 )
280 278 279 eqeltrd ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ∈ 𝑊 )
281 224 237 267 158 161 274 280 conncn ⊢ ( 𝜑 → ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) : ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) ⟶ 𝑊 )
282 273 feq2d ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) : ( { 𝑋 } × 𝑉 ) ⟶ 𝑊 ↔ ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) : ∪ ( ( II ×t II ) ↾t ( { 𝑋 } × 𝑉 ) ) ⟶ 𝑊 ) )
283 281 282 mpbird ⊢ ( 𝜑 → ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) : ( { 𝑋 } × 𝑉 ) ⟶ 𝑊 )
284 283 219 18 fovrnd ⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ↾ ( { 𝑋 } × 𝑉 ) ) 𝑍 ) ∈ 𝑊 )
285 223 284 eqeltrd ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) ‘ ⟨ 𝑋 , 𝑍 ⟩ ) ∈ 𝑊 )
286 180 195 206 158 161 214 285 conncn ⊢ ( 𝜑 → ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) : ∪ ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) ⟶ 𝑊 )
287 213 feq2d ⊢ ( 𝜑 → ( ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) : ( 𝑈 × { 𝑍 } ) ⟶ 𝑊 ↔ ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) : ∪ ( ( II ×t II ) ↾t ( 𝑈 × { 𝑍 } ) ) ⟶ 𝑊 ) )
288 286 287 mpbird ⊢ ( 𝜑 → ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) : ( 𝑈 × { 𝑍 } ) ⟶ 𝑊 )
289 288 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) : ( 𝑈 × { 𝑍 } ) ⟶ 𝑊 )
290 289 110 175 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝑚 ( 𝐾 ↾ ( 𝑈 × { 𝑍 } ) ) 𝑍 ) ∈ 𝑊 )
291 179 290 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) ‘ ⟨ 𝑚 , 𝑍 ⟩ ) ∈ 𝑊 )
292 61 80 142 159 162 169 291 conncn ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) : ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) ⟶ 𝑊 )
293 168 feq2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) : ( { 𝑚 } × 𝑉 ) ⟶ 𝑊 ↔ ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) : ∪ ( ( II ×t II ) ↾t ( { 𝑚 } × 𝑉 ) ) ⟶ 𝑊 ) )
294 292 293 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) : ( { 𝑚 } × 𝑉 ) ⟶ 𝑊 )
295 294 57 58 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝑚 ( 𝐾 ↾ ( { 𝑚 } × 𝑉 ) ) 𝑛 ) ∈ 𝑊 )
296 60 295 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝑚 𝐾 𝑛 ) ∈ 𝑊 )
297 296 ralrimivva ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑈 ∀ 𝑛 ∈ 𝑉 ( 𝑚 𝐾 𝑛 ) ∈ 𝑊 )
298 funimassov ⊢ ( ( Fun 𝐾 ∧ ( 𝑈 × 𝑉 ) ⊆ dom 𝐾 ) → ( ( 𝐾 “ ( 𝑈 × 𝑉 ) ) ⊆ 𝑊 ↔ ∀ 𝑚 ∈ 𝑈 ∀ 𝑛 ∈ 𝑉 ( 𝑚 𝐾 𝑛 ) ∈ 𝑊 ) )
299 122 124 298 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 “ ( 𝑈 × 𝑉 ) ) ⊆ 𝑊 ↔ ∀ 𝑚 ∈ 𝑈 ∀ 𝑛 ∈ 𝑉 ( 𝑚 𝐾 𝑛 ) ∈ 𝑊 ) )
300 297 299 mpbird ⊢ ( 𝜑 → ( 𝐾 “ ( 𝑈 × 𝑉 ) ) ⊆ 𝑊 )
301 1 23 8 2 24 26 28 38 10 53 55 300 cvmlift2lem9a ⊢ ( 𝜑 → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) Cn 𝐶 ) )