| Step | Hyp | Ref
| Expression |
| 1 | | cvmlift2.b |
. . 3
⊢ 𝐵 = ∪
𝐶 |
| 2 | | cvmlift2.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 3 | | cvmlift2.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
| 4 | | cvmlift2.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
| 5 | | cvmlift2.i |
. . 3
⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0)) |
| 6 | | cvmlift2.h |
. . 3
⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃)) |
| 7 | | cvmlift2.k |
. . 3
⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦)) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem5 35312 |
. 2
⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
| 9 | | iunid 5060 |
. . . . . . 7
⊢ ∪ 𝑎 ∈ (0[,]1){𝑎} = (0[,]1) |
| 10 | 9 | xpeq2i 5712 |
. . . . . 6
⊢ ((0[,]1)
× ∪ 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) ×
(0[,]1)) |
| 11 | | xpiundi 5756 |
. . . . . 6
⊢ ((0[,]1)
× ∪ 𝑎 ∈ (0[,]1){𝑎}) = ∪
𝑎 ∈ (0[,]1)((0[,]1)
× {𝑎}) |
| 12 | 10, 11 | eqtr3i 2767 |
. . . . 5
⊢ ((0[,]1)
× (0[,]1)) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) |
| 13 | | iiuni 24907 |
. . . . . . . . 9
⊢ (0[,]1) =
∪ II |
| 14 | | iiconn 24913 |
. . . . . . . . . 10
⊢ II ∈
Conn |
| 15 | 14 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → II ∈
Conn) |
| 16 | | inss1 4237 |
. . . . . . . . . 10
⊢ (II ∩
(Clsd‘II)) ⊆ II |
| 17 | | iicmp 24912 |
. . . . . . . . . . . . . . 15
⊢ II ∈
Comp |
| 18 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈
Comp) |
| 19 | | iitop 24906 |
. . . . . . . . . . . . . . 15
⊢ II ∈
Top |
| 20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈
Top) |
| 21 | 19, 19 | txtopi 23598 |
. . . . . . . . . . . . . . . 16
⊢ (II
×t II) ∈ Top |
| 22 | 13 | neiss2 23109 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((II
∈ Top ∧ 𝑢 ∈
((nei‘II)‘{𝑟}))
→ {𝑟} ⊆
(0[,]1)) |
| 23 | 19, 22 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈
((nei‘II)‘{𝑟})
→ {𝑟} ⊆
(0[,]1)) |
| 24 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑟 ∈ V |
| 25 | 24 | snss 4785 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑟 ∈ (0[,]1) ↔ {𝑟} ⊆
(0[,]1)) |
| 26 | 23, 25 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈
((nei‘II)‘{𝑟})
→ 𝑟 ∈
(0[,]1)) |
| 27 | 26 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈
((nei‘II)‘{𝑟})
→ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1))) |
| 28 | 27 | rexlimiv 3148 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1)) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑟 ∈ (0[,]1)) |
| 30 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑡 ∈ (0[,]1)) |
| 31 | 29, 30 | jca 511 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) |
| 32 | 31 | ssopab2i 5555 |
. . . . . . . . . . . . . . . . 17
⊢
{〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))} |
| 33 | | cvmlift2.s |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} |
| 34 | | df-xp 5691 |
. . . . . . . . . . . . . . . . 17
⊢ ((0[,]1)
× (0[,]1)) = {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))} |
| 35 | 32, 33, 34 | 3sstr4i 4035 |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 ⊆ ((0[,]1) ×
(0[,]1)) |
| 36 | 19, 19, 13, 13 | txunii 23601 |
. . . . . . . . . . . . . . . . 17
⊢ ((0[,]1)
× (0[,]1)) = ∪ (II ×t
II) |
| 37 | 36 | ntropn 23057 |
. . . . . . . . . . . . . . . 16
⊢ (((II
×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) →
((int‘(II ×t II))‘𝑆) ∈ (II ×t
II)) |
| 38 | 21, 35, 37 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢
((int‘(II ×t II))‘𝑆) ∈ (II ×t
II) |
| 39 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((int‘(II
×t II))‘𝑆) ∈ (II ×t
II)) |
| 40 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 41 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
| 42 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑃 ∈ 𝐵) |
| 43 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (𝐹‘𝑃) = (0𝐺0)) |
| 44 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
| 45 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑏 ∈ (0[,]1)) |
| 46 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑎 ∈ (0[,]1)) |
| 47 | 1, 40, 41, 42, 43, 6, 7, 44, 45, 46 | cvmlift2lem10 35317 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) |
| 48 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → (II
×t II) ∈ Top) |
| 49 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑆 ⊆ ((0[,]1) ×
(0[,]1))) |
| 50 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → II ∈
Top) |
| 51 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑢 ∈ II) |
| 52 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑣 ∈ II) |
| 53 | | txopn 23610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (𝑢 × 𝑣) ∈ (II ×t
II)) |
| 54 | 50, 50, 51, 52, 53 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ∈ (II ×t
II)) |
| 55 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ 𝑣) |
| 56 | | elunii 4912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ ∪
II) |
| 57 | 56, 13 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ (0[,]1)) |
| 58 | 55, 52, 57 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ (0[,]1)) |
| 59 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → II ∈ Top) |
| 60 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ II) |
| 61 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑟 ∈ 𝑢) |
| 62 | | opnneip 23127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((II
∈ Top ∧ 𝑢 ∈
II ∧ 𝑟 ∈ 𝑢) → 𝑢 ∈ ((nei‘II)‘{𝑟})) |
| 63 | 59, 60, 61, 62 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ ((nei‘II)‘{𝑟})) |
| 64 | 40 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 65 | 41 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
| 66 | 42 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑃 ∈ 𝐵) |
| 67 | 43 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝐹‘𝑃) = (0𝐺0)) |
| 68 | | cvmlift2.m |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)} |
| 69 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑣 ∈ II) |
| 70 | | simplr2 1217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑎 ∈ 𝑣) |
| 71 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ 𝑣) |
| 72 | | sneq 4636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑐 = 𝑤 → {𝑐} = {𝑤}) |
| 73 | 72 | xpeq2d 5715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤})) |
| 74 | 73 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤}))) |
| 75 | 73 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 = 𝑤 → ((II ×t II)
↾t (𝑢
× {𝑐})) = ((II
×t II) ↾t (𝑢 × {𝑤}))) |
| 76 | 75 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 = 𝑤 → (((II ×t II)
↾t (𝑢
× {𝑐})) Cn 𝐶) = (((II ×t
II) ↾t (𝑢
× {𝑤})) Cn 𝐶)) |
| 77 | 74, 76 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×t II)
↾t (𝑢
× {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) |
| 78 | 77 | cbvrexvw 3238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑐 ∈
𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×t II)
↾t (𝑢
× {𝑐})) Cn 𝐶) ↔ ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶)) |
| 79 | | simplr3 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑎 ∈ (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 𝐶))) |
| 80 | 78, 79 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (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 | 1, 64, 65, 66, 67, 6, 7, 68, 60, 69, 70, 71, 80 | cvmlift2lem11 35318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀)) |
| 82 | 1, 64, 65, 66, 67, 6, 7, 68, 60, 69, 71, 70, 80 | cvmlift2lem11 35318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑡}) ⊆ 𝑀 → (𝑢 × {𝑎}) ⊆ 𝑀)) |
| 83 | 81, 82 | impbid 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
| 84 | | rspe 3249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑢 ∈
((nei‘II)‘{𝑟})
∧ ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
| 85 | 63, 83, 84 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
| 86 | 58, 85 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
| 87 | 86 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
| 88 | 87 | alrimivv 1928 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
| 89 | | df-xp 5691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 × 𝑣) = {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} |
| 90 | 89, 33 | sseq12i 4014 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}) |
| 91 | | ssopab2bw 5552 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
({〈𝑟, 𝑡〉 ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
| 92 | 90, 91 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
| 93 | 88, 92 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ 𝑆) |
| 94 | 36 | ssntr 23066 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((II
×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) ∧
((𝑢 × 𝑣) ∈ (II ×t
II) ∧ (𝑢 × 𝑣) ⊆ 𝑆)) → (𝑢 × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆)) |
| 95 | 48, 49, 54, 93, 94 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆)) |
| 96 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑏 ∈ 𝑢) |
| 97 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑎 ∈ 𝑣) |
| 98 | | opelxpi 5722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣) → 〈𝑏, 𝑎〉 ∈ (𝑢 × 𝑣)) |
| 99 | 96, 97, 98 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 〈𝑏, 𝑎〉 ∈ (𝑢 × 𝑣)) |
| 100 | 95, 99 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆)) |
| 101 | 100 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆))) |
| 102 | 101 | rexlimdvva 3213 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆))) |
| 103 | 47, 102 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆)) |
| 104 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑎 ∈ V |
| 105 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑎 → 〈𝑏, 𝑤〉 = 〈𝑏, 𝑎〉) |
| 106 | 105 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑎 → (〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆) ↔ 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆))) |
| 107 | 104, 106 | ralsn 4681 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑤 ∈
{𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆) ↔ 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆)) |
| 108 | 103, 107 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
| 109 | 108 | anassrs 467 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑏 ∈ (0[,]1)) → ∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
| 110 | 109 | ralrimiva 3146 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
| 111 | | dfss3 3972 |
. . . . . . . . . . . . . . . 16
⊢ (((0[,]1)
× {𝑎}) ⊆
((int‘(II ×t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×t
II))‘𝑆)) |
| 112 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 〈𝑏, 𝑤〉 → (𝑢 ∈ ((int‘(II ×t
II))‘𝑆) ↔
〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆))) |
| 113 | 112 | ralxp 5852 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑢 ∈
((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II
×t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
| 114 | 111, 113 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢ (((0[,]1)
× {𝑎}) ⊆
((int‘(II ×t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
| 115 | 110, 114 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((0[,]1) ×
{𝑎}) ⊆
((int‘(II ×t II))‘𝑆)) |
| 116 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → 𝑎 ∈ (0[,]1)) |
| 117 | 13, 13, 18, 20, 39, 115, 116 | txtube 23648 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆))) |
| 118 | 36 | ntrss2 23065 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((II
×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) →
((int‘(II ×t II))‘𝑆) ⊆ 𝑆) |
| 119 | 21, 35, 118 | mp2an 692 |
. . . . . . . . . . . . . . . . . 18
⊢
((int‘(II ×t II))‘𝑆) ⊆ 𝑆 |
| 120 | | sstr 3992 |
. . . . . . . . . . . . . . . . . 18
⊢
((((0[,]1) × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆) ∧
((int‘(II ×t II))‘𝑆) ⊆ 𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆) |
| 121 | 119, 120 | mpan2 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((0[,]1)
× 𝑣) ⊆
((int‘(II ×t II))‘𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆) |
| 122 | | df-xp 5691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0[,]1)
× 𝑣) = {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} |
| 123 | 122, 33 | sseq12i 4014 |
. . . . . . . . . . . . . . . . . 18
⊢ (((0[,]1)
× 𝑣) ⊆ 𝑆 ↔ {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}) |
| 124 | | ssopab2bw 5552 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
| 125 | | r2al 3195 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑟 ∈
(0[,]1)∀𝑡 ∈
𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
| 126 | | ralcom 3289 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑟 ∈
(0[,]1)∀𝑡 ∈
𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
| 127 | 124, 125,
126 | 3bitr2i 299 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
| 128 | 123, 127 | bitri 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((0[,]1)
× 𝑣) ⊆ 𝑆 ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
| 129 | 121, 128 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (((0[,]1)
× 𝑣) ⊆
((int‘(II ×t II))‘𝑆) → ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
| 130 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
| 131 | 130 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑟 ∈
(0[,]1)(𝑡 ∈ (0[,]1)
∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
| 132 | | cvmlift2lem1 35307 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
| 133 | | bicom 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀)) |
| 134 | 133 | rexbii 3094 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀)) |
| 135 | 134 | ralbii 3093 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀)) |
| 136 | | cvmlift2lem1 35307 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
| 137 | 135, 136 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
| 138 | 132, 137 | impbid 212 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
| 139 | 131, 138 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑟 ∈
(0[,]1)(𝑡 ∈ (0[,]1)
∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
| 140 | | cvmlift2.a |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐴 = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) ×
{𝑎}) ⊆ 𝑀} |
| 141 | 140 | reqabi 3460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ 𝐴 ↔ (𝑎 ∈ (0[,]1) ∧ ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
| 142 | 141 | baib 535 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ (0[,]1) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
| 143 | 142 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
| 144 | | elssuni 4937 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∈ II → 𝑣 ⊆ ∪ II) |
| 145 | 144, 13 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ II → 𝑣 ⊆
(0[,]1)) |
| 146 | 145 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1)) |
| 147 | 146 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ (0[,]1)) |
| 148 | | sneq 4636 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑡 → {𝑎} = {𝑡}) |
| 149 | 148 | xpeq2d 5715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡})) |
| 150 | 149 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
| 151 | 150, 140 | elrab2 3695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ 𝐴 ↔ (𝑡 ∈ (0[,]1) ∧ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
| 152 | 151 | baib 535 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ (0[,]1) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
| 153 | 147, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
| 154 | 143, 153 | bibi12d 345 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → ((𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴) ↔ (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))) |
| 155 | 139, 154 | imbitrrid 246 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
| 156 | 155 | ralimdva 3167 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
| 157 | 129, 156 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (((0[,]1) × 𝑣) ⊆ ((int‘(II
×t II))‘𝑆) → ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
| 158 | 157 | anim2d 612 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → ((𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆)) →
(𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))) |
| 159 | 158 | reximdva 3168 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆)) →
∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))) |
| 160 | 117, 159 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
| 161 | 160 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
| 162 | | ssrab2 4080 |
. . . . . . . . . . . . 13
⊢ {𝑎 ∈ (0[,]1) ∣ ((0[,]1)
× {𝑎}) ⊆ 𝑀} ⊆
(0[,]1) |
| 163 | 140, 162 | eqsstri 4030 |
. . . . . . . . . . . 12
⊢ 𝐴 ⊆
(0[,]1) |
| 164 | 13 | isclo 23095 |
. . . . . . . . . . . 12
⊢ ((II
∈ Top ∧ 𝐴 ⊆
(0[,]1)) → (𝐴 ∈
(II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))) |
| 165 | 19, 163, 164 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (II ∩
(Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
| 166 | 161, 165 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (II ∩
(Clsd‘II))) |
| 167 | 16, 166 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ II) |
| 168 | | 0elunit 13509 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]1) |
| 169 | 168 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
(0[,]1)) |
| 170 | | relxp 5703 |
. . . . . . . . . . . . 13
⊢ Rel
((0[,]1) × {0}) |
| 171 | 170 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → Rel ((0[,]1) ×
{0})) |
| 172 | | opelxp 5721 |
. . . . . . . . . . . . 13
⊢
(〈𝑟, 𝑎〉 ∈ ((0[,]1) ×
{0}) ↔ (𝑟 ∈
(0[,]1) ∧ 𝑎 ∈
{0})) |
| 173 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈
(0[,]1)) |
| 174 | | opelxpi 5722 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑟 ∈ (0[,]1) ∧ 0 ∈
(0[,]1)) → 〈𝑟,
0〉 ∈ ((0[,]1) × (0[,]1))) |
| 175 | 173, 169,
174 | syl2anr 597 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 〈𝑟, 0〉 ∈ ((0[,]1)
× (0[,]1))) |
| 176 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 177 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
| 178 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝑃 ∈ 𝐵) |
| 179 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (𝐹‘𝑃) = (0𝐺0)) |
| 180 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝑟 ∈ (0[,]1)) |
| 181 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 0 ∈
(0[,]1)) |
| 182 | 1, 176, 177, 178, 179, 6, 7, 44, 180, 181 | cvmlift2lem10 35317 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) |
| 183 | | df-3an 1089 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) ↔ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) |
| 184 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 0 ∈ 𝑣) |
| 185 | 8 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
| 186 | 185 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 Fn ((0[,]1) ×
(0[,]1))) |
| 187 | | fnov 7564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐾 Fn ((0[,]1) × (0[,]1))
↔ 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤))) |
| 188 | 186, 187 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤))) |
| 189 | 188 | reseq1d 5996 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0}))) |
| 190 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II) |
| 191 | | elssuni 4937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 ∈ II → 𝑢 ⊆ ∪ II) |
| 192 | 191, 13 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 ∈ II → 𝑢 ⊆
(0[,]1)) |
| 193 | 190, 192 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1)) |
| 194 | 169 | snssd 4809 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → {0} ⊆
(0[,]1)) |
| 195 | 194 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → {0} ⊆
(0[,]1)) |
| 196 | | resmpo 7553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 ⊆ (0[,]1) ∧ {0}
⊆ (0[,]1)) → ((𝑏
∈ (0[,]1), 𝑤 ∈
(0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤))) |
| 197 | 193, 195,
196 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤))) |
| 198 | 193 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → 𝑏 ∈ (0[,]1)) |
| 199 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝜑) |
| 200 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem8 35315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏)) |
| 201 | 199, 200 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏)) |
| 202 | 198, 201 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑏𝐾0) = (𝐻‘𝑏)) |
| 203 | | elsni 4643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ {0} → 𝑤 = 0) |
| 204 | 203 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0)) |
| 205 | 204 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {0} → ((𝑏𝐾𝑤) = (𝐻‘𝑏) ↔ (𝑏𝐾0) = (𝐻‘𝑏))) |
| 206 | 202, 205 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝐻‘𝑏))) |
| 207 | 206 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢 ∧ 𝑤 ∈ {0}) → (𝑏𝐾𝑤) = (𝐻‘𝑏)) |
| 208 | 207 | mpoeq3dva 7510 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏))) |
| 209 | 189, 197,
208 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏))) |
| 210 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (II
↾t 𝑢) =
(II ↾t 𝑢) |
| 211 | | iitopon 24905 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ II ∈
(TopOn‘(0[,]1)) |
| 212 | 211 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈
(TopOn‘(0[,]1))) |
| 213 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (II
↾t {0}) = (II ↾t {0}) |
| 214 | 212, 212 | cnmpt1st 23676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×t II) Cn
II)) |
| 215 | 1, 2, 3, 4, 5, 6 | cvmlift2lem2 35309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃)) |
| 216 | 215 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐶)) |
| 217 | 199, 216 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐻 ∈ (II Cn 𝐶)) |
| 218 | 212, 212,
214, 217 | cnmpt21f 23680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻‘𝑏)) ∈ ((II ×t II) Cn
𝐶)) |
| 219 | 210, 212,
193, 213, 212, 195, 218 | cnmpt2res 23685 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ↾t 𝑢) ×t (II
↾t {0})) Cn 𝐶)) |
| 220 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑢 ∈ V |
| 221 | | snex 5436 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {0}
∈ V |
| 222 | | txrest 23639 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ V ∧ {0} ∈ V)) → ((II
×t II) ↾t (𝑢 × {0})) = ((II ↾t
𝑢) ×t (II
↾t {0}))) |
| 223 | 19, 19, 220, 221, 222 | mp4an 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((II
×t II) ↾t (𝑢 × {0})) = ((II ↾t
𝑢) ×t (II
↾t {0})) |
| 224 | 223 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((II
×t II) ↾t (𝑢 × {0})) Cn 𝐶) = (((II ↾t 𝑢) ×t (II
↾t {0})) Cn 𝐶) |
| 225 | 219, 224 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ×t II)
↾t (𝑢
× {0})) Cn 𝐶)) |
| 226 | 209, 225 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II
×t II) ↾t (𝑢 × {0})) Cn 𝐶)) |
| 227 | | sneq 4636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 0 → {𝑤} = {0}) |
| 228 | 227 | xpeq2d 5715 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0})) |
| 229 | 228 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0}))) |
| 230 | 228 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 0 → ((II
×t II) ↾t (𝑢 × {𝑤})) = ((II ×t II)
↾t (𝑢
× {0}))) |
| 231 | 230 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 0 → (((II
×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×t II)
↾t (𝑢
× {0})) Cn 𝐶)) |
| 232 | 229, 231 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II
×t II) ↾t (𝑢 × {0})) Cn 𝐶))) |
| 233 | 232 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {0})) ∈ (((II
×t II) ↾t (𝑢 × {0})) Cn 𝐶)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶)) |
| 234 | 184, 226,
233 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶)) |
| 235 | | opelxpi 5722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) → 〈𝑟, 0〉 ∈ (𝑢 × 𝑣)) |
| 236 | 235 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 〈𝑟, 0〉 ∈ (𝑢 × 𝑣)) |
| 237 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ∈ II) |
| 238 | 237, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ⊆ (0[,]1)) |
| 239 | | xpss12 5700 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑢 ⊆ (0[,]1) ∧ 𝑣 ⊆ (0[,]1)) → (𝑢 × 𝑣) ⊆ ((0[,]1) ×
(0[,]1))) |
| 240 | 193, 238,
239 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ⊆ ((0[,]1) ×
(0[,]1))) |
| 241 | 36 | restuni 23170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((II
×t II) ∈ Top ∧ (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1))) →
(𝑢 × 𝑣) = ∪
((II ×t II) ↾t (𝑢 × 𝑣))) |
| 242 | 21, 240, 241 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) = ∪ ((II
×t II) ↾t (𝑢 × 𝑣))) |
| 243 | 236, 242 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 〈𝑟, 0〉 ∈ ∪
((II ×t II) ↾t (𝑢 × 𝑣))) |
| 244 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∪ ((II ×t II) ↾t (𝑢 × 𝑣)) = ∪ ((II
×t II) ↾t (𝑢 × 𝑣)) |
| 245 | 244 | cncnpi 23286 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶) ∧ 〈𝑟, 0〉 ∈ ∪
((II ×t II) ↾t (𝑢 × 𝑣))) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II)
↾t (𝑢
× 𝑣)) CnP 𝐶)‘〈𝑟, 0〉)) |
| 246 | 245 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑟, 0〉
∈ ∪ ((II ×t II)
↾t (𝑢
× 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II)
↾t (𝑢
× 𝑣)) CnP 𝐶)‘〈𝑟, 0〉))) |
| 247 | 243, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II)
↾t (𝑢
× 𝑣)) CnP 𝐶)‘〈𝑟, 0〉))) |
| 248 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (II ×t II) ∈
Top) |
| 249 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ Top) |
| 250 | 249, 249,
190, 237, 53 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ∈ (II ×t
II)) |
| 251 | | isopn3i 23090 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((II
×t II) ∈ Top ∧ (𝑢 × 𝑣) ∈ (II ×t II)) →
((int‘(II ×t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣)) |
| 252 | 21, 250, 251 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((int‘(II ×t
II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣)) |
| 253 | 236, 252 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 〈𝑟, 0〉 ∈ ((int‘(II
×t II))‘(𝑢 × 𝑣))) |
| 254 | 36, 1 | cnprest 23297 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((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 839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉) ↔ (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II)
↾t (𝑢
× 𝑣)) CnP 𝐶)‘〈𝑟, 0〉))) |
| 256 | 247, 255 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
| 257 | 234, 256 | embantd 59 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
| 258 | 257 | expimpd 453 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
| 259 | 183, 258 | biimtrid 242 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
| 260 | 259 | rexlimdvva 3213 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
| 261 | 182, 260 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉)) |
| 262 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑟, 0〉 → (((II ×t
II) CnP 𝐶)‘𝑧) = (((II ×t
II) CnP 𝐶)‘〈𝑟, 0〉)) |
| 263 | 262 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑟, 0〉 → (𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
| 264 | 263, 68 | elrab2 3695 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑟, 0〉
∈ 𝑀 ↔
(〈𝑟, 0〉 ∈
((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
| 265 | 175, 261,
264 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 〈𝑟, 0〉 ∈ 𝑀) |
| 266 | | elsni 4643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ {0} → 𝑎 = 0) |
| 267 | 266 | opeq2d 4880 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ {0} → 〈𝑟, 𝑎〉 = 〈𝑟, 0〉) |
| 268 | 267 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {0} → (〈𝑟, 𝑎〉 ∈ 𝑀 ↔ 〈𝑟, 0〉 ∈ 𝑀)) |
| 269 | 265, 268 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (𝑎 ∈ {0} → 〈𝑟, 𝑎〉 ∈ 𝑀)) |
| 270 | 269 | expimpd 453 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}) → 〈𝑟, 𝑎〉 ∈ 𝑀)) |
| 271 | 172, 270 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑟, 𝑎〉 ∈ ((0[,]1) × {0}) →
〈𝑟, 𝑎〉 ∈ 𝑀)) |
| 272 | 171, 271 | relssdv 5798 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0[,]1) × {0})
⊆ 𝑀) |
| 273 | | sneq 4636 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 0 → {𝑎} = {0}) |
| 274 | 273 | xpeq2d 5715 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 0 → ((0[,]1) ×
{𝑎}) = ((0[,]1) ×
{0})) |
| 275 | 274 | sseq1d 4015 |
. . . . . . . . . . . 12
⊢ (𝑎 = 0 → (((0[,]1) ×
{𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0})
⊆ 𝑀)) |
| 276 | 275, 140 | elrab2 3695 |
. . . . . . . . . . 11
⊢ (0 ∈
𝐴 ↔ (0 ∈ (0[,]1)
∧ ((0[,]1) × {0}) ⊆ 𝑀)) |
| 277 | 169, 272,
276 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ 𝐴) |
| 278 | 277 | ne0d 4342 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ ∅) |
| 279 | | inss2 4238 |
. . . . . . . . . 10
⊢ (II ∩
(Clsd‘II)) ⊆ (Clsd‘II) |
| 280 | 279, 166 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (Clsd‘II)) |
| 281 | 13, 15, 167, 278, 280 | connclo 23423 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = (0[,]1)) |
| 282 | 281, 140 | eqtr3di 2792 |
. . . . . . 7
⊢ (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1)
× {𝑎}) ⊆ 𝑀}) |
| 283 | | rabid2 3470 |
. . . . . . 7
⊢ ((0[,]1)
= {𝑎 ∈ (0[,]1) ∣
((0[,]1) × {𝑎})
⊆ 𝑀} ↔
∀𝑎 ∈
(0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀) |
| 284 | 282, 283 | sylib 218 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀) |
| 285 | | iunss 5045 |
. . . . . 6
⊢ (∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀) |
| 286 | 284, 285 | sylibr 234 |
. . . . 5
⊢ (𝜑 → ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀) |
| 287 | 12, 286 | eqsstrid 4022 |
. . . 4
⊢ (𝜑 → ((0[,]1) × (0[,]1))
⊆ 𝑀) |
| 288 | 287, 68 | sseqtrdi 4024 |
. . 3
⊢ (𝜑 → ((0[,]1) × (0[,]1))
⊆ {𝑧 ∈ ((0[,]1)
× (0[,]1)) ∣ 𝐾
∈ (((II ×t II) CnP 𝐶)‘𝑧)}) |
| 289 | | ssrab 4073 |
. . . 4
⊢ (((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 496 |
. . 3
⊢ (((0[,]1)
× (0[,]1)) ⊆ {𝑧
∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)} → ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)) |
| 291 | 288, 290 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)) |
| 292 | | txtopon 23599 |
. . . 4
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II
×t II) ∈ (TopOn‘((0[,]1) ×
(0[,]1)))) |
| 293 | 211, 211,
292 | mp2an 692 |
. . 3
⊢ (II
×t II) ∈ (TopOn‘((0[,]1) ×
(0[,]1))) |
| 294 | | cvmtop1 35265 |
. . . . 5
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
| 295 | 2, 294 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Top) |
| 296 | 1 | toptopon 22923 |
. . . 4
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
| 297 | 295, 296 | sylib 218 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
| 298 | | cncnp 23288 |
. . 3
⊢ (((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 587 |
. 2
⊢ (𝜑 → (𝐾 ∈ ((II ×t II) Cn
𝐶) ↔ (𝐾:((0[,]1) ×
(0[,]1))⟶𝐵 ∧
∀𝑧 ∈ ((0[,]1)
× (0[,]1))𝐾 ∈
(((II ×t II) CnP 𝐶)‘𝑧)))) |
| 300 | 8, 291, 299 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐾 ∈ ((II ×t II) Cn
𝐶)) |