Metamath Proof Explorer

Theorem cvmlift2lem11

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 𝐶 ) ‘ 𝑧 ) }
cvmlift2lem11.1 ⊢ ( 𝜑 → 𝑈 ∈ II )
cvmlift2lem11.2 ⊢ ( 𝜑 → 𝑉 ∈ II )
cvmlift2lem11.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
cvmlift2lem11.4 ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
cvmlift2lem11.5 ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝑉 ( 𝐾 ↾ ( 𝑈 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) Cn 𝐶 ) ) )
Assertion cvmlift2lem11 ( 𝜑 → ( ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 → ( 𝑈 × { 𝑍 } ) ⊆ 𝑀 ) )

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 cvmlift2lem11.1 ⊢ ( 𝜑 → 𝑈 ∈ II )
10 cvmlift2lem11.2 ⊢ ( 𝜑 → 𝑉 ∈ II )
11 cvmlift2lem11.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
12 cvmlift2lem11.4 ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
13 cvmlift2lem11.5 ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝑉 ( 𝐾 ↾ ( 𝑈 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑤 } ) ) Cn 𝐶 ) → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) Cn 𝐶 ) ) )
14 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝑈 ∈ II )
15 elssuni ⊢ ( 𝑈 ∈ II → 𝑈 ⊆ ∪ II )
16 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
17 15 16 sseqtrrdi ⊢ ( 𝑈 ∈ II → 𝑈 ⊆ ( 0 [,] 1 ) )
18 14 17 syl ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝑈 ⊆ ( 0 [,] 1 ) )
19 elunii ⊢ ( ( 𝑍 ∈ 𝑉 ∧ 𝑉 ∈ II ) → 𝑍 ∈ ∪ II )
20 19 16 eleqtrrdi ⊢ ( ( 𝑍 ∈ 𝑉 ∧ 𝑉 ∈ II ) → 𝑍 ∈ ( 0 [,] 1 ) )
21 12 10 20 syl2anc ⊢ ( 𝜑 → 𝑍 ∈ ( 0 [,] 1 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝑍 ∈ ( 0 [,] 1 ) )
23 22 snssd ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → { 𝑍 } ⊆ ( 0 [,] 1 ) )
24 xpss12 ⊢ ( ( 𝑈 ⊆ ( 0 [,] 1 ) ∧ { 𝑍 } ⊆ ( 0 [,] 1 ) ) → ( 𝑈 × { 𝑍 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
25 18 23 24 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑍 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
26 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝑌 ∈ 𝑉 )
27 1 2 3 4 5 6 7 cvmlift2lem5 ⊢ ( 𝜑 → 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
29 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝑉 ∈ II )
30 elssuni ⊢ ( 𝑉 ∈ II → 𝑉 ⊆ ∪ II )
31 30 16 sseqtrrdi ⊢ ( 𝑉 ∈ II → 𝑉 ⊆ ( 0 [,] 1 ) )
32 29 31 syl ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝑉 ⊆ ( 0 [,] 1 ) )
33 32 26 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝑌 ∈ ( 0 [,] 1 ) )
34 33 snssd ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → { 𝑌 } ⊆ ( 0 [,] 1 ) )
35 xpss12 ⊢ ( ( 𝑈 ⊆ ( 0 [,] 1 ) ∧ { 𝑌 } ⊆ ( 0 [,] 1 ) ) → ( 𝑈 × { 𝑌 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
36 18 34 35 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑌 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
37 28 36 fssresd ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) : ( 𝑈 × { 𝑌 } ) ⟶ 𝐵 )
38 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) ) → ( 𝑈 × { 𝑌 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
39 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) ) → 𝑧 ∈ ( 𝑈 × { 𝑌 } ) )
40 simpr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 )
41 40 8 sseqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑌 } ) ⊆ { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) } )
42 ssrab ⊢ ( ( 𝑈 × { 𝑌 } ) ⊆ { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) } ↔ ( ( 𝑈 × { 𝑌 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∧ ∀ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ) )
43 42 simprbi ⊢ ( ( 𝑈 × { 𝑌 } ) ⊆ { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) } → ∀ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) )
44 41 43 syl ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ∀ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) )
45 44 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) ) → 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) )
46 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
47 txtopon ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ) → ( II ×t II ) ∈ ( TopOn ‘ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
48 46 46 47 mp2an ⊢ ( II ×t II ) ∈ ( TopOn ‘ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
49 48 toponunii ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ∪ ( II ×t II )
50 49 cnpresti ⊢ ( ( ( 𝑈 × { 𝑌 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) ∧ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ) → ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) CnP 𝐶 ) ‘ 𝑧 ) )
51 38 39 45 50 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) ) → ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) CnP 𝐶 ) ‘ 𝑧 ) )
52 51 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ∀ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) CnP 𝐶 ) ‘ 𝑧 ) )
53 resttopon ⊢ ( ( ( II ×t II ) ∈ ( TopOn ‘ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∧ ( 𝑈 × { 𝑌 } ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) ∈ ( TopOn ‘ ( 𝑈 × { 𝑌 } ) ) )
54 48 36 53 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) ∈ ( TopOn ‘ ( 𝑈 × { 𝑌 } ) ) )
55 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
56 2 55 syl ⊢ ( 𝜑 → 𝐶 ∈ Top )
57 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝐶 ∈ Top )
58 1 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
59 57 58 sylib ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
60 cncnp ⊢ ( ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) ∈ ( TopOn ‘ ( 𝑈 × { 𝑌 } ) ) ∧ 𝐶 ∈ ( TopOn ‘ 𝐵 ) ) → ( ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) Cn 𝐶 ) ↔ ( ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) : ( 𝑈 × { 𝑌 } ) ⟶ 𝐵 ∧ ∀ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) CnP 𝐶 ) ‘ 𝑧 ) ) ) )
61 54 59 60 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) Cn 𝐶 ) ↔ ( ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) : ( 𝑈 × { 𝑌 } ) ⟶ 𝐵 ∧ ∀ 𝑧 ∈ ( 𝑈 × { 𝑌 } ) ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) CnP 𝐶 ) ‘ 𝑧 ) ) ) )
62 37 52 61 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) Cn 𝐶 ) )
63 sneq ⊢ ( 𝑤 = 𝑌 → { 𝑤 } = { 𝑌 } )
64 63 xpeq2d ⊢ ( 𝑤 = 𝑌 → ( 𝑈 × { 𝑤 } ) = ( 𝑈 × { 𝑌 } ) )
65 64 reseq2d ⊢ ( 𝑤 = 𝑌 → ( 𝐾 ↾ ( 𝑈 × { 𝑤 } ) ) = ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) )
66 64 oveq2d ⊢ ( 𝑤 = 𝑌 → ( ( II ×t II ) ↾t ( 𝑈 × { 𝑤 } ) ) = ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) )
67 66 oveq1d ⊢ ( 𝑤 = 𝑌 → ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑤 } ) ) Cn 𝐶 ) = ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) Cn 𝐶 ) )
68 65 67 eleq12d ⊢ ( 𝑤 = 𝑌 → ( ( 𝐾 ↾ ( 𝑈 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑤 } ) ) Cn 𝐶 ) ↔ ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) Cn 𝐶 ) ) )
69 68 rspcev ⊢ ( ( 𝑌 ∈ 𝑉 ∧ ( 𝐾 ↾ ( 𝑈 × { 𝑌 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑌 } ) ) Cn 𝐶 ) ) → ∃ 𝑤 ∈ 𝑉 ( 𝐾 ↾ ( 𝑈 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑤 } ) ) Cn 𝐶 ) )
70 26 62 69 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ∃ 𝑤 ∈ 𝑉 ( 𝐾 ↾ ( 𝑈 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑤 } ) ) Cn 𝐶 ) )
71 13 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑤 ∈ 𝑉 ( 𝐾 ↾ ( 𝑈 × { 𝑤 } ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × { 𝑤 } ) ) Cn 𝐶 ) ) → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) Cn 𝐶 ) )
72 70 71 syldan ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) Cn 𝐶 ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) Cn 𝐶 ) )
74 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → 𝑍 ∈ 𝑉 )
75 74 snssd ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → { 𝑍 } ⊆ 𝑉 )
76 xpss2 ⊢ ( { 𝑍 } ⊆ 𝑉 → ( 𝑈 × { 𝑍 } ) ⊆ ( 𝑈 × 𝑉 ) )
77 75 76 syl ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑍 } ) ⊆ ( 𝑈 × 𝑉 ) )
78 iitop ⊢ II ∈ Top
79 78 78 txtopi ⊢ ( II ×t II ) ∈ Top
80 xpss12 ⊢ ( ( 𝑈 ⊆ ( 0 [,] 1 ) ∧ 𝑉 ⊆ ( 0 [,] 1 ) ) → ( 𝑈 × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
81 18 32 80 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
82 49 restuni ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( 𝑈 × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( 𝑈 × 𝑉 ) = ∪ ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) )
83 79 81 82 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × 𝑉 ) = ∪ ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) )
84 77 83 sseqtrd ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑍 } ) ⊆ ∪ ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) )
85 84 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → 𝑧 ∈ ∪ ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) )
86 eqid ⊢ ∪ ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) = ∪ ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) )
87 86 cncnpi ⊢ ( ( ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) Cn 𝐶 ) ∧ 𝑧 ∈ ∪ ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) ) → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) CnP 𝐶 ) ‘ 𝑧 ) )
88 73 85 87 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) CnP 𝐶 ) ‘ 𝑧 ) )
89 79 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → ( II ×t II ) ∈ Top )
90 81 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → ( 𝑈 × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
91 78 a1i ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → II ∈ Top )
92 txopn ⊢ ( ( ( II ∈ Top ∧ II ∈ Top ) ∧ ( 𝑈 ∈ II ∧ 𝑉 ∈ II ) ) → ( 𝑈 × 𝑉 ) ∈ ( II ×t II ) )
93 91 91 14 29 92 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × 𝑉 ) ∈ ( II ×t II ) )
94 isopn3i ⊢ ( ( ( II ×t II ) ∈ Top ∧ ( 𝑈 × 𝑉 ) ∈ ( II ×t II ) ) → ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑈 × 𝑉 ) ) = ( 𝑈 × 𝑉 ) )
95 79 93 94 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑈 × 𝑉 ) ) = ( 𝑈 × 𝑉 ) )
96 77 95 sseqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑍 } ) ⊆ ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑈 × 𝑉 ) ) )
97 96 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → 𝑧 ∈ ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑈 × 𝑉 ) ) )
98 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
99 49 1 cnprest ⊢ ( ( ( ( II ×t II ) ∈ Top ∧ ( 𝑈 × 𝑉 ) ⊆ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∧ ( 𝑧 ∈ ( ( int ‘ ( II ×t II ) ) ‘ ( 𝑈 × 𝑉 ) ) ∧ 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ) ) → ( 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ↔ ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) CnP 𝐶 ) ‘ 𝑧 ) ) )
100 89 90 97 98 99 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → ( 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ↔ ( 𝐾 ↾ ( 𝑈 × 𝑉 ) ) ∈ ( ( ( ( II ×t II ) ↾t ( 𝑈 × 𝑉 ) ) CnP 𝐶 ) ‘ 𝑧 ) ) )
101 88 100 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) ∧ 𝑧 ∈ ( 𝑈 × { 𝑍 } ) ) → 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) )
102 25 101 ssrabdv ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑍 } ) ⊆ { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) } )
103 102 8 sseqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 ) → ( 𝑈 × { 𝑍 } ) ⊆ 𝑀 )
104 103 ex ⊢ ( 𝜑 → ( ( 𝑈 × { 𝑌 } ) ⊆ 𝑀 → ( 𝑈 × { 𝑍 } ) ⊆ 𝑀 ) )