Proof of Theorem cvmlift2lem11
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cvmlift2lem11.1 | . . . . . . 7
⊢ (𝜑 → 𝑈 ∈ II) | 
| 2 | 1 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑈 ∈ II) | 
| 3 |  | elssuni 4936 | . . . . . . 7
⊢ (𝑈 ∈ II → 𝑈 ⊆ ∪ II) | 
| 4 |  | iiuni 24908 | . . . . . . 7
⊢ (0[,]1) =
∪ II | 
| 5 | 3, 4 | sseqtrrdi 4024 | . . . . . 6
⊢ (𝑈 ∈ II → 𝑈 ⊆
(0[,]1)) | 
| 6 | 2, 5 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑈 ⊆ (0[,]1)) | 
| 7 |  | cvmlift2lem11.4 | . . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ 𝑉) | 
| 8 |  | cvmlift2lem11.2 | . . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ II) | 
| 9 |  | elunii 4911 | . . . . . . . . 9
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑉 ∈ II) → 𝑍 ∈ ∪
II) | 
| 10 | 9, 4 | eleqtrrdi 2851 | . . . . . . . 8
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑉 ∈ II) → 𝑍 ∈ (0[,]1)) | 
| 11 | 7, 8, 10 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (0[,]1)) | 
| 12 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑍 ∈ (0[,]1)) | 
| 13 | 12 | snssd 4808 | . . . . 5
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → {𝑍} ⊆ (0[,]1)) | 
| 14 |  | xpss12 5699 | . . . . 5
⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) ×
(0[,]1))) | 
| 15 | 6, 13, 14 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ ((0[,]1) ×
(0[,]1))) | 
| 16 |  | cvmlift2lem11.3 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝑉) | 
| 17 | 16 | adantr 480 | . . . . . . . . 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 35313 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) | 
| 26 | 25 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) | 
| 27 | 8 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑉 ∈ II) | 
| 28 |  | elssuni 4936 | . . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ II → 𝑉 ⊆ ∪ II) | 
| 29 | 28, 4 | sseqtrrdi 4024 | . . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ II → 𝑉 ⊆
(0[,]1)) | 
| 30 | 27, 29 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑉 ⊆ (0[,]1)) | 
| 31 | 30, 17 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑌 ∈ (0[,]1)) | 
| 32 | 31 | snssd 4808 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → {𝑌} ⊆ (0[,]1)) | 
| 33 |  | xpss12 5699 | . . . . . . . . . . . 12
⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑌} ⊆ (0[,]1)) → (𝑈 × {𝑌}) ⊆ ((0[,]1) ×
(0[,]1))) | 
| 34 | 6, 32, 33 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑌}) ⊆ ((0[,]1) ×
(0[,]1))) | 
| 35 | 26, 34 | fssresd 6774 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝐾 ↾ (𝑈 × {𝑌})):(𝑈 × {𝑌})⟶𝐵) | 
| 36 | 34 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑌})) → (𝑈 × {𝑌}) ⊆ ((0[,]1) ×
(0[,]1))) | 
| 37 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑌})) → 𝑧 ∈ (𝑈 × {𝑌})) | 
| 38 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑌}) ⊆ 𝑀) | 
| 39 |  | cvmlift2.m | . . . . . . . . . . . . . . 15
⊢ 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)} | 
| 40 | 38, 39 | sseqtrdi 4023 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑌}) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)}) | 
| 41 |  | ssrab 4072 | . . . . . . . . . . . . . . 15
⊢ ((𝑈 × {𝑌}) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)} ↔ ((𝑈 × {𝑌}) ⊆ ((0[,]1) × (0[,]1)) ∧
∀𝑧 ∈ (𝑈 × {𝑌})𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧))) | 
| 42 | 41 | simprbi 496 | . . . . . . . . . . . . . 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 3250 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑌})) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)) | 
| 45 |  | iitopon 24906 | . . . . . . . . . . . . . . 15
⊢ II ∈
(TopOn‘(0[,]1)) | 
| 46 |  | txtopon 23600 | . . . . . . . . . . . . . . 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 22923 | . . . . . . . . . . . . 13
⊢ ((0[,]1)
× (0[,]1)) = ∪ (II ×t
II) | 
| 49 | 48 | cnpresti 23297 | . . . . . . . . . . . 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 3145 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ∀𝑧 ∈ (𝑈 × {𝑌})(𝐾 ↾ (𝑈 × {𝑌})) ∈ ((((II ×t II)
↾t (𝑈
× {𝑌})) CnP 𝐶)‘𝑧)) | 
| 52 |  | resttopon 23170 | . . . . . . . . . . . 12
⊢ (((II
×t II) ∈ (TopOn‘((0[,]1) × (0[,]1))) ∧
(𝑈 × {𝑌}) ⊆ ((0[,]1) ×
(0[,]1))) → ((II ×t II) ↾t (𝑈 × {𝑌})) ∈ (TopOn‘(𝑈 × {𝑌}))) | 
| 53 | 47, 34, 52 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ((II ×t II)
↾t (𝑈
× {𝑌})) ∈
(TopOn‘(𝑈 ×
{𝑌}))) | 
| 54 |  | cvmtop1 35266 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) | 
| 55 | 19, 54 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ Top) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝐶 ∈ Top) | 
| 57 | 18 | toptopon 22924 | . . . . . . . . . . . 12
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) | 
| 58 | 56, 57 | sylib 218 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝐶 ∈ (TopOn‘𝐵)) | 
| 59 |  | cncnp 23289 | . . . . . . . . . . 11
⊢ ((((II
×t II) ↾t (𝑈 × {𝑌})) ∈ (TopOn‘(𝑈 × {𝑌})) ∧ 𝐶 ∈ (TopOn‘𝐵)) → ((𝐾 ↾ (𝑈 × {𝑌})) ∈ (((II ×t II)
↾t (𝑈
× {𝑌})) Cn 𝐶) ↔ ((𝐾 ↾ (𝑈 × {𝑌})):(𝑈 × {𝑌})⟶𝐵 ∧ ∀𝑧 ∈ (𝑈 × {𝑌})(𝐾 ↾ (𝑈 × {𝑌})) ∈ ((((II ×t II)
↾t (𝑈
× {𝑌})) CnP 𝐶)‘𝑧)))) | 
| 60 | 53, 58, 59 | syl2anc 584 | . . . . . . . . . 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 4635 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑌 → {𝑤} = {𝑌}) | 
| 63 | 62 | xpeq2d 5714 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑌 → (𝑈 × {𝑤}) = (𝑈 × {𝑌})) | 
| 64 | 63 | reseq2d 5996 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑌 → (𝐾 ↾ (𝑈 × {𝑤})) = (𝐾 ↾ (𝑈 × {𝑌}))) | 
| 65 | 63 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑌 → ((II ×t II)
↾t (𝑈
× {𝑤})) = ((II
×t II) ↾t (𝑈 × {𝑌}))) | 
| 66 | 65 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑌 → (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶) = (((II ×t
II) ↾t (𝑈
× {𝑌})) Cn 𝐶)) | 
| 67 | 64, 66 | eleq12d 2834 | . . . . . . . . . 10
⊢ (𝑤 = 𝑌 → ((𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑌})) ∈ (((II ×t II)
↾t (𝑈
× {𝑌})) Cn 𝐶))) | 
| 68 | 67 | rspcev 3621 | . . . . . . . . 9
⊢ ((𝑌 ∈ 𝑉 ∧ (𝐾 ↾ (𝑈 × {𝑌})) ∈ (((II ×t II)
↾t (𝑈
× {𝑌})) Cn 𝐶)) → ∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶)) | 
| 69 | 17, 61, 68 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶)) | 
| 70 |  | cvmlift2lem11.5 | . . . . . . . . 9
⊢ (𝜑 → (∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶))) | 
| 71 | 70 | imp 406 | . . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II)
↾t (𝑈
× {𝑤})) Cn 𝐶)) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶)) | 
| 72 | 69, 71 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶)) | 
| 73 | 72 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶)) | 
| 74 | 7 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → 𝑍 ∈ 𝑉) | 
| 75 | 74 | snssd 4808 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → {𝑍} ⊆ 𝑉) | 
| 76 |  | xpss2 5704 | . . . . . . . . 9
⊢ ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉)) | 
| 77 | 75, 76 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉)) | 
| 78 |  | iitop 24907 | . . . . . . . . . 10
⊢ II ∈
Top | 
| 79 | 78, 78 | txtopi 23599 | . . . . . . . . 9
⊢ (II
×t II) ∈ Top | 
| 80 |  | xpss12 5699 | . . . . . . . . . 10
⊢ ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) | 
| 81 | 6, 30, 80 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) | 
| 82 | 48 | restuni 23171 | . . . . . . . . 9
⊢ (((II
×t II) ∈ Top ∧ (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1))) →
(𝑈 × 𝑉) = ∪
((II ×t II) ↾t (𝑈 × 𝑉))) | 
| 83 | 79, 81, 82 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × 𝑉) = ∪ ((II
×t II) ↾t (𝑈 × 𝑉))) | 
| 84 | 77, 83 | sseqtrd 4019 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ ∪ ((II
×t II) ↾t (𝑈 × 𝑉))) | 
| 85 | 84 | sselda 3982 | . . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → 𝑧 ∈ ∪ ((II
×t II) ↾t (𝑈 × 𝑉))) | 
| 86 |  | eqid 2736 | . . . . . . 7
⊢ ∪ ((II ×t II) ↾t (𝑈 × 𝑉)) = ∪ ((II
×t II) ↾t (𝑈 × 𝑉)) | 
| 87 | 86 | cncnpi 23287 | . . . . . 6
⊢ (((𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶) ∧ 𝑧 ∈ ∪ ((II
×t II) ↾t (𝑈 × 𝑉))) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ ((((II ×t II)
↾t (𝑈
× 𝑉)) CnP 𝐶)‘𝑧)) | 
| 88 | 73, 85, 87 | syl2anc 584 | . . . . 5
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ ((((II ×t II)
↾t (𝑈
× 𝑉)) CnP 𝐶)‘𝑧)) | 
| 89 | 79 | a1i 11 | . . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (II ×t II)
∈ Top) | 
| 90 | 81 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → (𝑈 × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) | 
| 91 | 78 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → II ∈ Top) | 
| 92 |  | txopn 23611 | . . . . . . . . . 10
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ (𝑈 ∈ II ∧ 𝑉 ∈ II)) → (𝑈 × 𝑉) ∈ (II ×t
II)) | 
| 93 | 91, 91, 2, 27, 92 | syl22anc 838 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × 𝑉) ∈ (II ×t
II)) | 
| 94 |  | isopn3i 23091 | . . . . . . . . 9
⊢ (((II
×t II) ∈ Top ∧ (𝑈 × 𝑉) ∈ (II ×t II)) →
((int‘(II ×t II))‘(𝑈 × 𝑉)) = (𝑈 × 𝑉)) | 
| 95 | 79, 93, 94 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → ((int‘(II ×t
II))‘(𝑈 × 𝑉)) = (𝑈 × 𝑉)) | 
| 96 | 77, 95 | sseqtrrd 4020 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ ((int‘(II
×t II))‘(𝑈 × 𝑉))) | 
| 97 | 96 | sselda 3982 | . . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → 𝑧 ∈ ((int‘(II ×t
II))‘(𝑈 × 𝑉))) | 
| 98 | 25 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) | 
| 99 | 48, 18 | cnprest 23298 | . . . . . 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 257 | . . . 4
⊢ (((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) ∧ 𝑧 ∈ (𝑈 × {𝑍})) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)) | 
| 102 | 15, 101 | ssrabdv 4073 | . . 3
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)}) | 
| 103 | 102, 39 | sseqtrrdi 4024 | . 2
⊢ ((𝜑 ∧ (𝑈 × {𝑌}) ⊆ 𝑀) → (𝑈 × {𝑍}) ⊆ 𝑀) | 
| 104 | 103 | ex 412 | 1
⊢ (𝜑 → ((𝑈 × {𝑌}) ⊆ 𝑀 → (𝑈 × {𝑍}) ⊆ 𝑀)) |