Metamath Proof Explorer

Theorem cvmlift2lem12

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 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
cvmlift2.m ⊢ 𝑀 = { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) }
cvmlift2.a ⊢ 𝐴 = { 𝑎 ∈ ( 0 [,] 1 ) ∣ ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 }
cvmlift2.s ⊢ 𝑆 = { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) }
Assertion cvmlift2lem12 ( 𝜑 → 𝐾 ∈ ( ( II ×t II ) 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 cvmlift2.m ⊢ 𝑀 = { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) }
9 cvmlift2.a ⊢ 𝐴 = { 𝑎 ∈ ( 0 [,] 1 ) ∣ ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 }
10 cvmlift2.s ⊢ 𝑆 = { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) }
11 1 2 3 4 5 6 7 cvmlift2lem5 ⊢ ( 𝜑 → 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
12 iunid ⊢ ∪ 𝑎 ∈ ( 0 [,] 1 ) { 𝑎 } = ( 0 [,] 1 )
13 12 xpeq2i ⊢ ( ( 0 [,] 1 ) × ∪ 𝑎 ∈ ( 0 [,] 1 ) { 𝑎 } ) = ( ( 0 [,] 1 ) × ( 0 [,] 1 ) )
14 xpiundi ⊢ ( ( 0 [,] 1 ) × ∪ 𝑎 ∈ ( 0 [,] 1 ) { 𝑎 } ) = ∪ 𝑎 ∈ ( 0 [,] 1 ) ( ( 0 [,] 1 ) × { 𝑎 } )
15 13 14 eqtr3i ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ∪ 𝑎 ∈ ( 0 [,] 1 ) ( ( 0 [,] 1 ) × { 𝑎 } )
16 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
17 iiconn ⊢ II ∈ Conn
18 17 a1i ⊢ ( 𝜑 → II ∈ Conn )
19 inss1 ⊢ ( II ∩ ( Clsd ‘ II ) ) ⊆ II
20 iicmp ⊢ II ∈ Comp
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → II ∈ Comp )
22 iitop ⊢ II ∈ Top
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → II ∈ Top )
24 22 22 txtopi ⊢ ( II ×t II ) ∈ Top
25 16 neiss2 ⊢ ( ( II ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ) → { 𝑟 } ⊆ ( 0 [,] 1 ) )
26 22 25 mpan ⊢ ( 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) → { 𝑟 } ⊆ ( 0 [,] 1 ) )
27 vex ⊢ 𝑟 ∈ V
28 27 snss ⊢ ( 𝑟 ∈ ( 0 [,] 1 ) ↔ { 𝑟 } ⊆ ( 0 [,] 1 ) )
29 26 28 sylibr ⊢ ( 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) → 𝑟 ∈ ( 0 [,] 1 ) )
30 29 a1d ⊢ ( 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) → ( ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → 𝑟 ∈ ( 0 [,] 1 ) ) )
31 30 rexlimiv ⊢ ( ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → 𝑟 ∈ ( 0 [,] 1 ) )
32 31 adantl ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → 𝑟 ∈ ( 0 [,] 1 ) )
33 simpl ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
34 32 33 jca ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) )
35 34 ssopab2i ⊢ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) } ⊆ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) }
36 df-xp ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) }
37 35 10 36 3sstr4i ⊢ 𝑆 ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) )
38 22 22 16 16 txunii ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ∪ ( II ×t II )
39 38 ntropn ⊢ ( ( ( II ×t II ) ∈ Top ∧ 𝑆 ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ∈ ( II ×t II ) )
40 24 37 39 mp2an ⊢ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ∈ ( II ×t II )
41 40 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ∈ ( II ×t II ) )
42 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
43 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
44 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → 𝑃 ∈ 𝐵 )
45 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
46 eqid ⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
47 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → 𝑏 ∈ ( 0 [,] 1 ) )
48 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → 𝑎 ∈ ( 0 [,] 1 ) )
49 1 42 43 44 45 6 7 46 47 48 cvmlift2lem10 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) )
50 24 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → ( II ×t II ) ∈ Top )
51 37 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → 𝑆 ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
52 22 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → II ∈ Top )
53 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → 𝑢 ∈ II )
54 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → 𝑣 ∈ II )
55 txopn ⊢ ( ( ( II ∈ Top ∧ II ∈ Top ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) → ( 𝑢 × 𝑣 ) ∈ ( II ×t II ) )
56 52 52 53 54 55 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → ( 𝑢 × 𝑣 ) ∈ ( II ×t II ) )
57 simpr ⊢ ( ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) → 𝑡 ∈ 𝑣 )
58 elunii ⊢ ( ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II ) → 𝑡 ∈ ∪ II )
59 58 16 eleqtrrdi ⊢ ( ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II ) → 𝑡 ∈ ( 0 [,] 1 ) )
60 57 54 59 syl2anr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
61 22 a1i ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → II ∈ Top )
62 53 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝑢 ∈ II )
63 simprl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝑟 ∈ 𝑢 )
64 opnneip ⊢ ( ( II ∈ Top ∧ 𝑢 ∈ II ∧ 𝑟 ∈ 𝑢 ) → 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) )
65 61 62 63 64 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) )
66 42 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
67 43 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
68 44 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝑃 ∈ 𝐵 )
69 45 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
70 54 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝑣 ∈ II )
71 simplr2 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝑎 ∈ 𝑣 )
72 simprr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → 𝑡 ∈ 𝑣 )
73 sneq ⊢ ( 𝑐 = 𝑤 → { 𝑐 } = { 𝑤 } )
74 73 xpeq2d ⊢ ( 𝑐 = 𝑤 → ( 𝑢 × { 𝑐 } ) = ( 𝑢 × { 𝑤 } ) )
75 74 reseq2d ⊢ ( 𝑐 = 𝑤 → ( 𝐾 ↾ ( 𝑢 × { 𝑐 } ) ) = ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) )
76 74 oveq2d ⊢ ( 𝑐 = 𝑤 → ( ( II ×t II ) ↾t ( 𝑢 × { 𝑐 } ) ) = ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) )
77 76 oveq1d ⊢ ( 𝑐 = 𝑤 → ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑐 } ) ) Cn 𝐶 ) = ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) )
78 75 77 eleq12d ⊢ ( 𝑐 = 𝑤 → ( ( 𝐾 ↾ ( 𝑢 × { 𝑐 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑐 } ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ) )
79 78 cbvrexvw ⊢ ( ∃ 𝑐 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑐 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑐 } ) ) Cn 𝐶 ) ↔ ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) )
80 simplr3 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) )
81 79 80 syl5bi ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → ( ∃ 𝑐 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑐 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑐 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) )
82 1 66 67 68 69 6 7 8 62 70 71 72 81 cvmlift2lem11 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 → ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) )
83 1 66 67 68 69 6 7 8 62 70 72 71 81 cvmlift2lem11 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 → ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ) )
84 82 83 impbid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) )
85 rspe ⊢ ( ( 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ∧ ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) )
86 65 84 85 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) )
87 60 86 jca ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) )
88 87 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → ( ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) → ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) ) )
89 88 alrimivv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → ∀ 𝑟 ∀ 𝑡 ( ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) → ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) ) )
90 df-xp ⊢ ( 𝑢 × 𝑣 ) = { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) }
91 90 10 sseq12i ⊢ ( ( 𝑢 × 𝑣 ) ⊆ 𝑆 ↔ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) } ⊆ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) } )
92 ssopab2bw ⊢ ( { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) } ⊆ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) } ↔ ∀ 𝑟 ∀ 𝑡 ( ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) → ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) ) )
93 91 92 bitri ⊢ ( ( 𝑢 × 𝑣 ) ⊆ 𝑆 ↔ ∀ 𝑟 ∀ 𝑡 ( ( 𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣 ) → ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) ) )
94 89 93 sylibr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → ( 𝑢 × 𝑣 ) ⊆ 𝑆 )
95 38 ssntr ⊢ ( ( ( ( II ×t II ) ∈ Top ∧ 𝑆 ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∧ ( ( 𝑢 × 𝑣 ) ∈ ( II ×t II ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑆 ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
96 50 51 56 94 95 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
97 simpr1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → 𝑏 ∈ 𝑢 )
98 simpr2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → 𝑎 ∈ 𝑣 )
99 opelxpi ⊢ ( ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ) → ⟨ 𝑏 , 𝑎 ⟩ ∈ ( 𝑢 × 𝑣 ) )
100 97 98 99 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → ⟨ 𝑏 , 𝑎 ⟩ ∈ ( 𝑢 × 𝑣 ) )
101 96 100 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ) → ⟨ 𝑏 , 𝑎 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
102 101 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) → ( ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) → ⟨ 𝑏 , 𝑎 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ) )
103 102 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → ( ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) → ⟨ 𝑏 , 𝑎 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ) )
104 49 103 mpd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → ⟨ 𝑏 , 𝑎 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
105 vex ⊢ 𝑎 ∈ V
106 opeq2 ⊢ ( 𝑤 = 𝑎 → ⟨ 𝑏 , 𝑤 ⟩ = ⟨ 𝑏 , 𝑎 ⟩ )
107 106 eleq1d ⊢ ( 𝑤 = 𝑎 → ( ⟨ 𝑏 , 𝑤 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ↔ ⟨ 𝑏 , 𝑎 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ) )
108 105 107 ralsn ⊢ ( ∀ 𝑤 ∈ { 𝑎 } ⟨ 𝑏 , 𝑤 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ↔ ⟨ 𝑏 , 𝑎 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
109 104 108 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ) → ∀ 𝑤 ∈ { 𝑎 } ⟨ 𝑏 , 𝑤 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
110 109 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) → ∀ 𝑤 ∈ { 𝑎 } ⟨ 𝑏 , 𝑤 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
111 110 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → ∀ 𝑏 ∈ ( 0 [,] 1 ) ∀ 𝑤 ∈ { 𝑎 } ⟨ 𝑏 , 𝑤 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
112 dfss3 ⊢ ( ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ↔ ∀ 𝑢 ∈ ( ( 0 [,] 1 ) × { 𝑎 } ) 𝑢 ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
113 eleq1 ⊢ ( 𝑢 = ⟨ 𝑏 , 𝑤 ⟩ → ( 𝑢 ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ↔ ⟨ 𝑏 , 𝑤 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ) )
114 113 ralxp ⊢ ( ∀ 𝑢 ∈ ( ( 0 [,] 1 ) × { 𝑎 } ) 𝑢 ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ↔ ∀ 𝑏 ∈ ( 0 [,] 1 ) ∀ 𝑤 ∈ { 𝑎 } ⟨ 𝑏 , 𝑤 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
115 112 114 bitri ⊢ ( ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ↔ ∀ 𝑏 ∈ ( 0 [,] 1 ) ∀ 𝑤 ∈ { 𝑎 } ⟨ 𝑏 , 𝑤 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
116 111 115 sylibr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) )
117 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → 𝑎 ∈ ( 0 [,] 1 ) )
118 16 16 21 23 41 116 117 txtube ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → ∃ 𝑣 ∈ II ( 𝑎 ∈ 𝑣 ∧ ( ( 0 [,] 1 ) × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ) )
119 38 ntrss2 ⊢ ( ( ( II ×t II ) ∈ Top ∧ 𝑆 ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ⊆ 𝑆 )
120 24 37 119 mp2an ⊢ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ⊆ 𝑆
121 sstr ⊢ ( ( ( ( 0 [,] 1 ) × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ∧ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ⊆ 𝑆 ) → ( ( 0 [,] 1 ) × 𝑣 ) ⊆ 𝑆 )
122 120 121 mpan2 ⊢ ( ( ( 0 [,] 1 ) × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) → ( ( 0 [,] 1 ) × 𝑣 ) ⊆ 𝑆 )
123 df-xp ⊢ ( ( 0 [,] 1 ) × 𝑣 ) = { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ 𝑣 ) }
124 123 10 sseq12i ⊢ ( ( ( 0 [,] 1 ) × 𝑣 ) ⊆ 𝑆 ↔ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ 𝑣 ) } ⊆ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) } )
125 ssopab2bw ⊢ ( { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ 𝑣 ) } ⊆ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) } ↔ ∀ 𝑟 ∀ 𝑡 ( ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ 𝑣 ) → ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) ) )
126 r2al ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑡 ∈ 𝑣 ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) ↔ ∀ 𝑟 ∀ 𝑡 ( ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ 𝑣 ) → ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) ) )
127 ralcom ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑡 ∈ 𝑣 ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) ↔ ∀ 𝑡 ∈ 𝑣 ∀ 𝑟 ∈ ( 0 [,] 1 ) ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) )
128 125 126 127 3bitr2i ⊢ ( { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ 𝑣 ) } ⊆ { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) } ↔ ∀ 𝑡 ∈ 𝑣 ∀ 𝑟 ∈ ( 0 [,] 1 ) ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) )
129 124 128 bitri ⊢ ( ( ( 0 [,] 1 ) × 𝑣 ) ⊆ 𝑆 ↔ ∀ 𝑡 ∈ 𝑣 ∀ 𝑟 ∈ ( 0 [,] 1 ) ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) )
130 122 129 sylib ⊢ ( ( ( 0 [,] 1 ) × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) → ∀ 𝑡 ∈ 𝑣 ∀ 𝑟 ∈ ( 0 [,] 1 ) ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) )
131 simpr ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) )
132 131 ralimi ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → ∀ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) )
133 cvmlift2lem1 ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 → ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )
134 bicom ⊢ ( ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ↔ ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ) )
135 134 rexbii ⊢ ( ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ↔ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ) )
136 135 ralbii ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ↔ ∀ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ) )
137 cvmlift2lem1 ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 → ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ) )
138 136 137 sylbi ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 → ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ) )
139 133 138 impbid ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ↔ ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )
140 132 139 syl ⊢ ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → ( ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ↔ ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )
141 9 rabeq2i ⊢ ( 𝑎 ∈ 𝐴 ↔ ( 𝑎 ∈ ( 0 [,] 1 ) ∧ ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ) )
142 141 baib ⊢ ( 𝑎 ∈ ( 0 [,] 1 ) → ( 𝑎 ∈ 𝐴 ↔ ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ) )
143 142 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) ∧ 𝑡 ∈ 𝑣 ) → ( 𝑎 ∈ 𝐴 ↔ ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ) )
144 elssuni ⊢ ( 𝑣 ∈ II → 𝑣 ⊆ ∪ II )
145 144 16 sseqtrrdi ⊢ ( 𝑣 ∈ II → 𝑣 ⊆ ( 0 [,] 1 ) )
146 145 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) → 𝑣 ⊆ ( 0 [,] 1 ) )
147 146 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) ∧ 𝑡 ∈ 𝑣 ) → 𝑡 ∈ ( 0 [,] 1 ) )
148 sneq ⊢ ( 𝑎 = 𝑡 → { 𝑎 } = { 𝑡 } )
149 148 xpeq2d ⊢ ( 𝑎 = 𝑡 → ( ( 0 [,] 1 ) × { 𝑎 } ) = ( ( 0 [,] 1 ) × { 𝑡 } ) )
150 149 sseq1d ⊢ ( 𝑎 = 𝑡 → ( ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ↔ ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )
151 150 9 elrab2 ⊢ ( 𝑡 ∈ 𝐴 ↔ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )
152 151 baib ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → ( 𝑡 ∈ 𝐴 ↔ ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )
153 147 152 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) ∧ 𝑡 ∈ 𝑣 ) → ( 𝑡 ∈ 𝐴 ↔ ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )
154 143 153 bibi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) ∧ 𝑡 ∈ 𝑣 ) → ( ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ↔ ( ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ↔ ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) ) )
155 140 154 syl5ibr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) ∧ 𝑡 ∈ 𝑣 ) → ( ∀ 𝑟 ∈ ( 0 [,] 1 ) ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) )
156 155 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) → ( ∀ 𝑡 ∈ 𝑣 ∀ 𝑟 ∈ ( 0 [,] 1 ) ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑎 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) → ∀ 𝑡 ∈ 𝑣 ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) )
157 130 156 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) → ( ( ( 0 [,] 1 ) × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) → ∀ 𝑡 ∈ 𝑣 ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) )
158 157 anim2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) ∧ 𝑣 ∈ II ) → ( ( 𝑎 ∈ 𝑣 ∧ ( ( 0 [,] 1 ) × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ) → ( 𝑎 ∈ 𝑣 ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) ) )
159 158 reximdva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → ( ∃ 𝑣 ∈ II ( 𝑎 ∈ 𝑣 ∧ ( ( 0 [,] 1 ) × 𝑣 ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ 𝑆 ) ) → ∃ 𝑣 ∈ II ( 𝑎 ∈ 𝑣 ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) ) )
160 118 159 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 [,] 1 ) ) → ∃ 𝑣 ∈ II ( 𝑎 ∈ 𝑣 ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) )
161 160 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 0 [,] 1 ) ∃ 𝑣 ∈ II ( 𝑎 ∈ 𝑣 ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) )
162 ssrab2 ⊢ { 𝑎 ∈ ( 0 [,] 1 ) ∣ ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 } ⊆ ( 0 [,] 1 )
163 9 162 eqsstri ⊢ 𝐴 ⊆ ( 0 [,] 1 )
164 16 isclo ⊢ ( ( II ∈ Top ∧ 𝐴 ⊆ ( 0 [,] 1 ) ) → ( 𝐴 ∈ ( II ∩ ( Clsd ‘ II ) ) ↔ ∀ 𝑎 ∈ ( 0 [,] 1 ) ∃ 𝑣 ∈ II ( 𝑎 ∈ 𝑣 ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) ) )
165 22 163 164 mp2an ⊢ ( 𝐴 ∈ ( II ∩ ( Clsd ‘ II ) ) ↔ ∀ 𝑎 ∈ ( 0 [,] 1 ) ∃ 𝑣 ∈ II ( 𝑎 ∈ 𝑣 ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) )
166 161 165 sylibr ⊢ ( 𝜑 → 𝐴 ∈ ( II ∩ ( Clsd ‘ II ) ) )
167 19 166 sselid ⊢ ( 𝜑 → 𝐴 ∈ II )
168 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
169 168 a1i ⊢ ( 𝜑 → 0 ∈ ( 0 [,] 1 ) )
170 relxp ⊢ Rel ( ( 0 [,] 1 ) × { 0 } )
171 170 a1i ⊢ ( 𝜑 → Rel ( ( 0 [,] 1 ) × { 0 } ) )
172 opelxp ⊢ ( ⟨ 𝑟 , 𝑎 ⟩ ∈ ( ( 0 [,] 1 ) × { 0 } ) ↔ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑎 ∈ { 0 } ) )
173 id ⊢ ( 𝑟 ∈ ( 0 [,] 1 ) → 𝑟 ∈ ( 0 [,] 1 ) )
174 opelxpi ⊢ ( ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ⟨ 𝑟 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
175 173 169 174 syl2anr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → ⟨ 𝑟 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
176 2 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
177 3 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
178 4 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → 𝑃 ∈ 𝐵 )
179 5 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
180 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → 𝑟 ∈ ( 0 [,] 1 ) )
181 168 a1i ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → 0 ∈ ( 0 [,] 1 ) )
182 1 176 177 178 179 6 7 46 180 181 cvmlift2lem10 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) )
183 df-3an ⊢ ( ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) ↔ ( ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) )
184 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 0 ∈ 𝑣 )
185 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
186 185 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝐾 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
187 fnov ⊢ ( 𝐾 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ↔ 𝐾 = ( 𝑏 ∈ ( 0 [,] 1 ) , 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑏 𝐾 𝑤 ) ) )
188 186 187 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝐾 = ( 𝑏 ∈ ( 0 [,] 1 ) , 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑏 𝐾 𝑤 ) ) )
189 188 reseq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝐾 ↾ ( 𝑢 × { 0 } ) ) = ( ( 𝑏 ∈ ( 0 [,] 1 ) , 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑏 𝐾 𝑤 ) ) ↾ ( 𝑢 × { 0 } ) ) )
190 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝑢 ∈ II )
191 elssuni ⊢ ( 𝑢 ∈ II → 𝑢 ⊆ ∪ II )
192 191 16 sseqtrrdi ⊢ ( 𝑢 ∈ II → 𝑢 ⊆ ( 0 [,] 1 ) )
193 190 192 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝑢 ⊆ ( 0 [,] 1 ) )
194 169 snssd ⊢ ( 𝜑 → { 0 } ⊆ ( 0 [,] 1 ) )
195 194 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → { 0 } ⊆ ( 0 [,] 1 ) )
196 resmpo ⊢ ( ( 𝑢 ⊆ ( 0 [,] 1 ) ∧ { 0 } ⊆ ( 0 [,] 1 ) ) → ( ( 𝑏 ∈ ( 0 [,] 1 ) , 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑏 𝐾 𝑤 ) ) ↾ ( 𝑢 × { 0 } ) ) = ( 𝑏 ∈ 𝑢 , 𝑤 ∈ { 0 } ↦ ( 𝑏 𝐾 𝑤 ) ) )
197 193 195 196 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( ( 𝑏 ∈ ( 0 [,] 1 ) , 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑏 𝐾 𝑤 ) ) ↾ ( 𝑢 × { 0 } ) ) = ( 𝑏 ∈ 𝑢 , 𝑤 ∈ { 0 } ↦ ( 𝑏 𝐾 𝑤 ) ) )
198 193 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) ∧ 𝑏 ∈ 𝑢 ) → 𝑏 ∈ ( 0 [,] 1 ) )
199 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝜑 )
200 1 2 3 4 5 6 7 cvmlift2lem8 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 0 [,] 1 ) ) → ( 𝑏 𝐾 0 ) = ( 𝐻 ‘ 𝑏 ) )
201 199 200 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) → ( 𝑏 𝐾 0 ) = ( 𝐻 ‘ 𝑏 ) )
202 198 201 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) ∧ 𝑏 ∈ 𝑢 ) → ( 𝑏 𝐾 0 ) = ( 𝐻 ‘ 𝑏 ) )
203 elsni ⊢ ( 𝑤 ∈ { 0 } → 𝑤 = 0 )
204 203 oveq2d ⊢ ( 𝑤 ∈ { 0 } → ( 𝑏 𝐾 𝑤 ) = ( 𝑏 𝐾 0 ) )
205 204 eqeq1d ⊢ ( 𝑤 ∈ { 0 } → ( ( 𝑏 𝐾 𝑤 ) = ( 𝐻 ‘ 𝑏 ) ↔ ( 𝑏 𝐾 0 ) = ( 𝐻 ‘ 𝑏 ) ) )
206 202 205 syl5ibrcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) ∧ 𝑏 ∈ 𝑢 ) → ( 𝑤 ∈ { 0 } → ( 𝑏 𝐾 𝑤 ) = ( 𝐻 ‘ 𝑏 ) ) )
207 206 3impia ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) ∧ 𝑏 ∈ 𝑢 ∧ 𝑤 ∈ { 0 } ) → ( 𝑏 𝐾 𝑤 ) = ( 𝐻 ‘ 𝑏 ) )
208 207 mpoeq3dva ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝑏 ∈ 𝑢 , 𝑤 ∈ { 0 } ↦ ( 𝑏 𝐾 𝑤 ) ) = ( 𝑏 ∈ 𝑢 , 𝑤 ∈ { 0 } ↦ ( 𝐻 ‘ 𝑏 ) ) )
209 189 197 208 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝐾 ↾ ( 𝑢 × { 0 } ) ) = ( 𝑏 ∈ 𝑢 , 𝑤 ∈ { 0 } ↦ ( 𝐻 ‘ 𝑏 ) ) )
210 eqid ⊢ ( II ↾t 𝑢 ) = ( II ↾t 𝑢 )
211 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
212 211 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
213 eqid ⊢ ( II ↾t { 0 } ) = ( II ↾t { 0 } )
214 212 212 cnmpt1st ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝑏 ∈ ( 0 [,] 1 ) , 𝑤 ∈ ( 0 [,] 1 ) ↦ 𝑏 ) ∈ ( ( II ×t II ) Cn II ) )
215 1 2 3 4 5 6 cvmlift2lem2 ⊢ ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) )
216 215 simp1d ⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐶 ) )
217 199 216 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝐻 ∈ ( II Cn 𝐶 ) )
218 212 212 214 217 cnmpt21f ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝑏 ∈ ( 0 [,] 1 ) , 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝐻 ‘ 𝑏 ) ) ∈ ( ( II ×t II ) Cn 𝐶 ) )
219 210 212 193 213 212 195 218 cnmpt2res ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝑏 ∈ 𝑢 , 𝑤 ∈ { 0 } ↦ ( 𝐻 ‘ 𝑏 ) ) ∈ ( ( ( II ↾t 𝑢 ) ×t ( II ↾t { 0 } ) ) Cn 𝐶 ) )
220 vex ⊢ 𝑢 ∈ V
221 snex ⊢ { 0 } ∈ V
222 txrest ⊢ ( ( ( II ∈ Top ∧ II ∈ Top ) ∧ ( 𝑢 ∈ V ∧ { 0 } ∈ V ) ) → ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) = ( ( II ↾t 𝑢 ) ×t ( II ↾t { 0 } ) ) )
223 22 22 220 221 222 mp4an ⊢ ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) = ( ( II ↾t 𝑢 ) ×t ( II ↾t { 0 } ) )
224 223 oveq1i ⊢ ( ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) Cn 𝐶 ) = ( ( ( II ↾t 𝑢 ) ×t ( II ↾t { 0 } ) ) Cn 𝐶 )
225 219 224 eleqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝑏 ∈ 𝑢 , 𝑤 ∈ { 0 } ↦ ( 𝐻 ‘ 𝑏 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) Cn 𝐶 ) )
226 209 225 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝐾 ↾ ( 𝑢 × { 0 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) Cn 𝐶 ) )
227 sneq ⊢ ( 𝑤 = 0 → { 𝑤 } = { 0 } )
228 227 xpeq2d ⊢ ( 𝑤 = 0 → ( 𝑢 × { 𝑤 } ) = ( 𝑢 × { 0 } ) )
229 228 reseq2d ⊢ ( 𝑤 = 0 → ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) = ( 𝐾 ↾ ( 𝑢 × { 0 } ) ) )
230 228 oveq2d ⊢ ( 𝑤 = 0 → ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) = ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) )
231 230 oveq1d ⊢ ( 𝑤 = 0 → ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) = ( ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) Cn 𝐶 ) )
232 229 231 eleq12d ⊢ ( 𝑤 = 0 → ( ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( 𝑢 × { 0 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) Cn 𝐶 ) ) )
233 232 rspcev ⊢ ( ( 0 ∈ 𝑣 ∧ ( 𝐾 ↾ ( 𝑢 × { 0 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 0 } ) ) Cn 𝐶 ) ) → ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) )
234 184 226 233 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) )
235 opelxpi ⊢ ( ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) → ⟨ 𝑟 , 0 ⟩ ∈ ( 𝑢 × 𝑣 ) )
236 235 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ⟨ 𝑟 , 0 ⟩ ∈ ( 𝑢 × 𝑣 ) )
237 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝑣 ∈ II )
238 237 145 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → 𝑣 ⊆ ( 0 [,] 1 ) )
239 xpss12 ⊢ ( ( 𝑢 ⊆ ( 0 [,] 1 ) ∧ 𝑣 ⊆ ( 0 [,] 1 ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
240 193 238 239 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝑢 × 𝑣 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
241 38 restuni ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( 𝑢 × 𝑣 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( 𝑢 × 𝑣 ) = ∪ ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) )
242 24 240 241 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝑢 × 𝑣 ) = ∪ ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) )
243 236 242 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ⟨ 𝑟 , 0 ⟩ ∈ ∪ ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) )
244 eqid ⊢ ∪ ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) = ∪ ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) )
245 244 cncnpi ⊢ ( ( ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ∧ ⟨ 𝑟 , 0 ⟩ ∈ ∪ ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) )
246 245 expcom ⊢ ( ⟨ 𝑟 , 0 ⟩ ∈ ∪ ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) → ( ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
247 243 246 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
248 24 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( II ×t II ) ∈ Top )
249 22 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → II ∈ Top )
250 249 249 190 237 55 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝑢 × 𝑣 ) ∈ ( II ×t II ) )
251 isopn3i ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( 𝑢 × 𝑣 ) ∈ ( II ×t II ) ) → ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑢 × 𝑣 ) ) = ( 𝑢 × 𝑣 ) )
252 24 250 251 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑢 × 𝑣 ) ) = ( 𝑢 × 𝑣 ) )
253 236 252 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ⟨ 𝑟 , 0 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑢 × 𝑣 ) ) )
254 38 1 cnprest ⊢ ( ( ( ( II ×t II ) ∈ Top ∧ ( 𝑢 × 𝑣 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∧ ( ⟨ 𝑟 , 0 ⟩ ∈ ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑢 × 𝑣 ) ) ∧ 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ) ) → ( 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ↔ ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
255 248 240 253 185 254 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ↔ ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
256 247 255 sylibrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) → 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
257 234 256 embantd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) ∧ ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ) → ( ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) → 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
258 257 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) → ( ( ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ) ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) → 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
259 183 258 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 ∈ II ∧ 𝑣 ∈ II ) ) → ( ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) → 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
260 259 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → ( ∃ 𝑢 ∈ II ∃ 𝑣 ∈ II ( 𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ ( ∃ 𝑤 ∈ 𝑣 ( 𝐾 ↾ ( 𝑢 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑢 × 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑢 × 𝑣 ) ) Cn 𝐶 ) ) ) → 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
261 182 260 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) )
262 fveq2 ⊢ ( 𝑧 = ⟨ 𝑟 , 0 ⟩ → ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) = ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) )
263 262 eleq2d ⊢ ( 𝑧 = ⟨ 𝑟 , 0 ⟩ → ( 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ↔ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
264 263 8 elrab2 ⊢ ( ⟨ 𝑟 , 0 ⟩ ∈ 𝑀 ↔ ( ⟨ 𝑟 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∧ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ ⟨ 𝑟 , 0 ⟩ ) ) )
265 175 261 264 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → ⟨ 𝑟 , 0 ⟩ ∈ 𝑀 )
266 elsni ⊢ ( 𝑎 ∈ { 0 } → 𝑎 = 0 )
267 266 opeq2d ⊢ ( 𝑎 ∈ { 0 } → ⟨ 𝑟 , 𝑎 ⟩ = ⟨ 𝑟 , 0 ⟩ )
268 267 eleq1d ⊢ ( 𝑎 ∈ { 0 } → ( ⟨ 𝑟 , 𝑎 ⟩ ∈ 𝑀 ↔ ⟨ 𝑟 , 0 ⟩ ∈ 𝑀 ) )
269 265 268 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → ( 𝑎 ∈ { 0 } → ⟨ 𝑟 , 𝑎 ⟩ ∈ 𝑀 ) )
270 269 expimpd ⊢ ( 𝜑 → ( ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑎 ∈ { 0 } ) → ⟨ 𝑟 , 𝑎 ⟩ ∈ 𝑀 ) )
271 172 270 syl5bi ⊢ ( 𝜑 → ( ⟨ 𝑟 , 𝑎 ⟩ ∈ ( ( 0 [,] 1 ) × { 0 } ) → ⟨ 𝑟 , 𝑎 ⟩ ∈ 𝑀 ) )
272 171 271 relssdv ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { 0 } ) ⊆ 𝑀 )
273 sneq ⊢ ( 𝑎 = 0 → { 𝑎 } = { 0 } )
274 273 xpeq2d ⊢ ( 𝑎 = 0 → ( ( 0 [,] 1 ) × { 𝑎 } ) = ( ( 0 [,] 1 ) × { 0 } ) )
275 274 sseq1d ⊢ ( 𝑎 = 0 → ( ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ↔ ( ( 0 [,] 1 ) × { 0 } ) ⊆ 𝑀 ) )
276 275 9 elrab2 ⊢ ( 0 ∈ 𝐴 ↔ ( 0 ∈ ( 0 [,] 1 ) ∧ ( ( 0 [,] 1 ) × { 0 } ) ⊆ 𝑀 ) )
277 169 272 276 sylanbrc ⊢ ( 𝜑 → 0 ∈ 𝐴 )
278 277 ne0d ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
279 inss2 ⊢ ( II ∩ ( Clsd ‘ II ) ) ⊆ ( Clsd ‘ II )
280 279 166 sselid ⊢ ( 𝜑 → 𝐴 ∈ ( Clsd ‘ II ) )
281 16 18 167 278 280 connclo ⊢ ( 𝜑 → 𝐴 = ( 0 [,] 1 ) )
282 281 9 eqtr3di ⊢ ( 𝜑 → ( 0 [,] 1 ) = { 𝑎 ∈ ( 0 [,] 1 ) ∣ ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 } )
283 rabid2 ⊢ ( ( 0 [,] 1 ) = { 𝑎 ∈ ( 0 [,] 1 ) ∣ ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 } ↔ ∀ 𝑎 ∈ ( 0 [,] 1 ) ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 )
284 282 283 sylib ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 0 [,] 1 ) ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 )
285 iunss ⊢ ( ∪ 𝑎 ∈ ( 0 [,] 1 ) ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 ↔ ∀ 𝑎 ∈ ( 0 [,] 1 ) ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 )
286 284 285 sylibr ⊢ ( 𝜑 → ∪ 𝑎 ∈ ( 0 [,] 1 ) ( ( 0 [,] 1 ) × { 𝑎 } ) ⊆ 𝑀 )
287 15 286 eqsstrid ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ 𝑀 )
288 287 8 sseqtrdi ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) } )
289 ssrab ⊢ ( ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) } ↔ ( ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∧ ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ) )
290 289 simprbi ⊢ ( ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) } → ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) )
291 288 290 syl ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) )
292 txtopon ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ) → ( II ×t II ) ∈ ( TopOn ‘ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
293 211 211 292 mp2an ⊢ ( II ×t II ) ∈ ( TopOn ‘ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
294 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
295 2 294 syl ⊢ ( 𝜑 → 𝐶 ∈ Top )
296 1 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
297 295 296 sylib ⊢ ( 𝜑 → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
298 cncnp ⊢ ( ( ( II ×t II ) ∈ ( TopOn ‘ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∧ 𝐶 ∈ ( TopOn ‘ 𝐵 ) ) → ( 𝐾 ∈ ( ( II ×t II ) Cn 𝐶 ) ↔ ( 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ) ) )
299 293 297 298 sylancr ⊢ ( 𝜑 → ( 𝐾 ∈ ( ( II ×t II ) Cn 𝐶 ) ↔ ( 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ) ) )
300 11 291 299 mpbir2and ⊢ ( 𝜑 → 𝐾 ∈ ( ( II ×t II ) Cn 𝐶 ) )