Proof of Theorem cvmlift2lem11
Step | Hyp | Ref
| Expression |
1 | | cvmlift2lem11.1 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ II) |
2 | 1 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑈 ∈ II) |
3 | | elssuni 4828 |
. . . . . . 7
⊢ (𝑈 ∈ II → 𝑈 ⊆ ∪ II) |
4 | | iiuni 23633 |
. . . . . . 7
⊢ (0[,]1) =
∪ II |
5 | 3, 4 | sseqtrrdi 3928 |
. . . . . 6
⊢ (𝑈 ∈ II → 𝑈 ⊆
(0[,]1)) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑈 ⊆ (0[,]1)) |
7 | | cvmlift2lem11.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
8 | | cvmlift2lem11.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ II) |
9 | | elunii 4801 |
. . . . . . . . 9
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑉 ∈ II) → 𝑍 ∈ ∪
II) |
10 | 9, 4 | eleqtrrdi 2844 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑉 ∈ II) → 𝑍 ∈ (0[,]1)) |
11 | 7, 8, 10 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (0[,]1)) |
12 | 11 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑍 ∈ (0[,]1)) |
13 | 12 | snssd 4697 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → {𝑍} ⊆ (0[,]1)) |
14 | | xpss12 5540 |
. . . . 5
⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) ×
(0[,]1))) |
15 | 6, 13, 14 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ ((0[,]1) ×
(0[,]1))) |
16 | | cvmlift2lem11.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
17 | 16 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑌 ∈ 𝑉) |
18 | | cvmlift2.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = ∪
𝐶 |
19 | | cvmlift2.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
20 | | cvmlift2.g |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
21 | | cvmlift2.p |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
22 | | cvmlift2.i |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0)) |
23 | | cvmlift2.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃)) |
24 | | cvmlift2.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦)) |
25 | 18, 19, 20, 21, 22, 23, 24 | cvmlift2lem5 32840 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
26 | 25 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
27 | 8 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑉 ∈ II) |
28 | | elssuni 4828 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ II → 𝑉 ⊆ ∪ II) |
29 | 28, 4 | sseqtrrdi 3928 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ II → 𝑉 ⊆
(0[,]1)) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑉 ⊆ (0[,]1)) |
31 | 30, 17 | sseldd 3878 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑌 ∈ (0[,]1)) |
32 | 31 | snssd 4697 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → {𝑌} ⊆ (0[,]1)) |
33 | | xpss12 5540 |
. . . . . . . . . . . 12
⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑌} ⊆ (0[,]1)) → (𝑈 × {𝑌}) ⊆ ((0[,]1) ×
(0[,]1))) |
34 | 6, 32, 33 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑌}) ⊆ ((0[,]1) ×
(0[,]1))) |
35 | 26, 34 | fssresd 6545 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝐾 ↾ (𝑈 × {𝑌})):(𝑈 × {𝑌})⟶𝐵) |
36 | 34 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑌})) → (𝑈 × {𝑌}) ⊆ ((0[,]1) ×
(0[,]1))) |
37 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑌})) → 𝑧 ∈ (𝑈 × {𝑌})) |
38 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑌}) ⊆ 𝑀) |
39 | | cvmlift2.m |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)} |
40 | 38, 39 | sseqtrdi 3927 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑌}) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)}) |
41 | | ssrab 3962 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 × {𝑌}) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)} ↔ ((𝑈 × {𝑌}) ⊆ ((0[,]1) × (0[,]1)) ∧
∀𝑧 ∈ (𝑈 × {𝑌})𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧))) |
42 | 41 | simprbi 500 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 × {𝑌}) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)} → ∀𝑧 ∈ (𝑈 × {𝑌})𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)) |
43 | 40, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ∀𝑧 ∈ (𝑈 × {𝑌})𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)) |
44 | 43 | r19.21bi 3121 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑌})) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)) |
45 | | iitopon 23631 |
. . . . . . . . . . . . . . 15
⊢ II ∈
(TopOn‘(0[,]1)) |
46 | | txtopon 22342 |
. . . . . . . . . . . . . . 15
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II
×t II) ∈ (TopOn‘((0[,]1) ×
(0[,]1)))) |
47 | 45, 45, 46 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (II
×t II) ∈ (TopOn‘((0[,]1) ×
(0[,]1))) |
48 | 47 | toponunii 21667 |
. . . . . . . . . . . . 13
⊢ ((0[,]1)
× (0[,]1)) = ∪ (II ×t
II) |
49 | 48 | cnpresti 22039 |
. . . . . . . . . . . 12
⊢ (((𝑈 × {𝑌}) ⊆ ((0[,]1) × (0[,]1)) ∧
𝑧 ∈ (𝑈 × {𝑌}) ∧ 𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)) → (𝐾 ↾ (𝑈 × {𝑌})) ∈ ((((II ×t II)
↾t (𝑈
× {𝑌})) CnP 𝐶)‘𝑧)) |
50 | 36, 37, 44, 49 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑌})) → (𝐾 ↾ (𝑈 × {𝑌})) ∈ ((((II ×t II)
↾t (𝑈
× {𝑌})) CnP 𝐶)‘𝑧)) |
51 | 50 | ralrimiva 3096 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ∀𝑧 ∈ (𝑈 × {𝑌})(𝐾 ↾ (𝑈 × {𝑌})) ∈ ((((II ×t II)
↾t (𝑈
× {𝑌})) CnP 𝐶)‘𝑧)) |
52 | | resttopon 21912 |
. . . . . . . . . . . 12
⊢ (((II
×t II) ∈ (TopOn‘((0[,]1) × (0[,]1))) ∧
(𝑈 × {𝑌}) ⊆ ((0[,]1) ×
(0[,]1))) → ((II ×t II) ↾t (𝑈 × {𝑌})) ∈ (TopOn‘(𝑈 × {𝑌}))) |
53 | 47, 34, 52 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ((II ×t II)
↾t (𝑈
× {𝑌})) ∈
(TopOn‘(𝑈 ×
{𝑌}))) |
54 | | cvmtop1 32793 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
55 | 19, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ Top) |
56 | 55 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝐶 ∈ Top) |
57 | 18 | toptopon 21668 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
58 | 56, 57 | sylib 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝐶 ∈ (TopOn‘𝐵)) |
59 | | cncnp 22031 |
. . . . . . . . . . 11
⊢ ((((II
×t II) ↾t (𝑈 × {𝑌})) ∈ (TopOn‘(𝑈 × {𝑌})) ∧ 𝐶 ∈ (TopOn‘𝐵)) → ((𝐾 ↾ (𝑈 × {𝑌})) ∈ (((II ×t II)
↾t (𝑈
× {𝑌})) Cn 𝐶) ↔ ((𝐾 ↾ (𝑈 × {𝑌})):(𝑈 × {𝑌})⟶𝐵 ∧ ∀𝑧 ∈ (𝑈 × {𝑌})(𝐾 ↾ (𝑈 × {𝑌})) ∈ ((((II ×t II)
↾t (𝑈
× {𝑌})) CnP 𝐶)‘𝑧)))) |
60 | 53, 58, 59 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ((𝐾 ↾ (𝑈 × {𝑌})) ∈ (((II ×t II)
↾t (𝑈
× {𝑌})) Cn 𝐶) ↔ ((𝐾 ↾ (𝑈 × {𝑌})):(𝑈 × {𝑌})⟶𝐵 ∧ ∀𝑧 ∈ (𝑈 × {𝑌})(𝐾 ↾ (𝑈 × {𝑌})) ∈ ((((II ×t II)
↾t (𝑈
× {𝑌})) CnP 𝐶)‘𝑧)))) |
61 | 35, 51, 60 | mpbir2and 713 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝐾 ↾ (𝑈 × {𝑌})) ∈ (((II ×t II)
↾t (𝑈
× {𝑌})) Cn 𝐶)) |
62 | | sneq 4526 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑌 → {𝑤} = {𝑌}) |
63 | 62 | xpeq2d 5555 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑌 → (𝑈 × {𝑤}) = (𝑈 × {𝑌})) |
64 | 63 | reseq2d 5825 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑌 → (𝐾 ↾ (𝑈 × {𝑤})) = (𝐾 ↾ (𝑈 × {𝑌}))) |
65 | 63 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑌 → ((II ×t II)
↾t (𝑈
× {𝑤})) = ((II
×t II) ↾t (𝑈 × {𝑌}))) |
66 | 65 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑌 → (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶) = (((II ×t
II) ↾t (𝑈
× {𝑌})) Cn 𝐶)) |
67 | 64, 66 | eleq12d 2827 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑌 → ((𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑌})) ∈ (((II ×t II)
↾t (𝑈
× {𝑌})) Cn 𝐶))) |
68 | 67 | rspcev 3526 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝑉 ∧ (𝐾 ↾ (𝑈 × {𝑌})) ∈ (((II ×t II)
↾t (𝑈
× {𝑌})) Cn 𝐶)) → ∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶)) |
69 | 17, 61, 68 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶)) |
70 | | cvmlift2lem11.5 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶))) |
71 | 70 | imp 410 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶)) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶)) |
72 | 69, 71 | syldan 594 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶)) |
73 | 72 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶)) |
74 | 7 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑍 ∈ 𝑉) |
75 | 74 | snssd 4697 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → {𝑍} ⊆ 𝑉) |
76 | | xpss2 5545 |
. . . . . . . . 9
⊢ ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉)) |
77 | 75, 76 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉)) |
78 | | iitop 23632 |
. . . . . . . . . 10
⊢ II ∈
Top |
79 | 78, 78 | txtopi 22341 |
. . . . . . . . 9
⊢ (II
×t II) ∈ Top |
80 | | xpss12 5540 |
. . . . . . . . . 10
⊢ ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) |
81 | 6, 30, 80 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) |
82 | 48 | restuni 21913 |
. . . . . . . . 9
⊢ (((II
×t II) ∈ Top ∧ (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1))) →
(𝑈 × 𝑉) = ∪
((II ×t II) ↾t (𝑈 × 𝑉))) |
83 | 79, 81, 82 | sylancr 590 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × 𝑉) = ∪ ((II
×t II) ↾t (𝑈 × 𝑉))) |
84 | 77, 83 | sseqtrd 3917 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ ∪ ((II
×t II) ↾t (𝑈 × 𝑉))) |
85 | 84 | sselda 3877 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → 𝑧 ∈ ∪ ((II
×t II) ↾t (𝑈 × 𝑉))) |
86 | | eqid 2738 |
. . . . . . 7
⊢ ∪ ((II ×t II) ↾t (𝑈 × 𝑉)) = ∪ ((II
×t II) ↾t (𝑈 × 𝑉)) |
87 | 86 | cncnpi 22029 |
. . . . . 6
⊢ (((𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶) ∧ 𝑧 ∈ ∪ ((II
×t II) ↾t (𝑈 × 𝑉))) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ ((((II ×t II)
↾t (𝑈
× 𝑉)) CnP 𝐶)‘𝑧)) |
88 | 73, 85, 87 | syl2anc 587 |
. . . . 5
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ ((((II ×t II)
↾t (𝑈
× 𝑉)) CnP 𝐶)‘𝑧)) |
89 | 79 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (II ×t II)
∈ Top) |
90 | 81 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (𝑈 × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) |
91 | 78 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → II ∈ Top) |
92 | | txopn 22353 |
. . . . . . . . . 10
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ (𝑈 ∈ II ∧ 𝑉 ∈ II)) → (𝑈 × 𝑉) ∈ (II ×t
II)) |
93 | 91, 91, 2, 27, 92 | syl22anc 838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × 𝑉) ∈ (II ×t
II)) |
94 | | isopn3i 21833 |
. . . . . . . . 9
⊢ (((II
×t II) ∈ Top ∧ (𝑈 × 𝑉) ∈ (II ×t II)) →
((int‘(II ×t II))‘(𝑈 × 𝑉)) = (𝑈 × 𝑉)) |
95 | 79, 93, 94 | sylancr 590 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ((int‘(II ×t
II))‘(𝑈 × 𝑉)) = (𝑈 × 𝑉)) |
96 | 77, 95 | sseqtrrd 3918 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ ((int‘(II
×t II))‘(𝑈 × 𝑉))) |
97 | 96 | sselda 3877 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → 𝑧 ∈ ((int‘(II ×t
II))‘(𝑈 × 𝑉))) |
98 | 25 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
99 | 48, 18 | cnprest 22040 |
. . . . . 6
⊢ ((((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 838 |
. . . . 5
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧) ↔ (𝐾 ↾ (𝑈 × 𝑉)) ∈ ((((II ×t II)
↾t (𝑈
× 𝑉)) CnP 𝐶)‘𝑧))) |
101 | 88, 100 | mpbird 260 |
. . . 4
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)) |
102 | 15, 101 | ssrabdv 3963 |
. . 3
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)}) |
103 | 102, 39 | sseqtrrdi 3928 |
. 2
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ 𝑀) |
104 | 103 | ex 416 |
1
⊢ (𝜑 → ((𝑈 × {𝑌}) ⊆ 𝑀 → (𝑈 × {𝑍}) ⊆ 𝑀)) |