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 30543 |
. 2
⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
9 | | iunid 4511 |
. . . . . . 7
⊢ ∪ 𝑎 ∈ (0[,]1){𝑎} = (0[,]1) |
10 | 9 | xpeq2i 5060 |
. . . . . 6
⊢ ((0[,]1)
× ∪ 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) ×
(0[,]1)) |
11 | | xpiundi 5096 |
. . . . . 6
⊢ ((0[,]1)
× ∪ 𝑎 ∈ (0[,]1){𝑎}) = ∪
𝑎 ∈ (0[,]1)((0[,]1)
× {𝑎}) |
12 | 10, 11 | eqtr3i 2634 |
. . . . 5
⊢ ((0[,]1)
× (0[,]1)) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) |
13 | | cvmlift2.a |
. . . . . . . 8
⊢ 𝐴 = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) ×
{𝑎}) ⊆ 𝑀} |
14 | | iiuni 22492 |
. . . . . . . . 9
⊢ (0[,]1) =
∪ II |
15 | | iicon 22498 |
. . . . . . . . . 10
⊢ II ∈
Con |
16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → II ∈
Con) |
17 | | inss1 3795 |
. . . . . . . . . 10
⊢ (II ∩
(Clsd‘II)) ⊆ II |
18 | | iicmp 22497 |
. . . . . . . . . . . . . . 15
⊢ II ∈
Comp |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈
Comp) |
20 | | iitop 22491 |
. . . . . . . . . . . . . . 15
⊢ II ∈
Top |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈
Top) |
22 | 20, 20 | txtopi 21203 |
. . . . . . . . . . . . . . . 16
⊢ (II
×t II) ∈ Top |
23 | 14 | neiss2 20715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((II
∈ Top ∧ 𝑢 ∈
((nei‘II)‘{𝑟}))
→ {𝑟} ⊆
(0[,]1)) |
24 | 20, 23 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈
((nei‘II)‘{𝑟})
→ {𝑟} ⊆
(0[,]1)) |
25 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑟 ∈ V |
26 | 25 | snss 4259 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑟 ∈ (0[,]1) ↔ {𝑟} ⊆
(0[,]1)) |
27 | 24, 26 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈
((nei‘II)‘{𝑟})
→ 𝑟 ∈
(0[,]1)) |
28 | 27 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈
((nei‘II)‘{𝑟})
→ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1))) |
29 | 28 | rexlimiv 3009 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1)) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑟 ∈ (0[,]1)) |
31 | | simpl 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑡 ∈ (0[,]1)) |
32 | 30, 31 | jca 553 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) |
33 | 32 | ssopab2i 4928 |
. . . . . . . . . . . . . . . . 17
⊢
{〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))} |
34 | | cvmlift2.s |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} |
35 | | df-xp 5044 |
. . . . . . . . . . . . . . . . 17
⊢ ((0[,]1)
× (0[,]1)) = {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))} |
36 | 33, 34, 35 | 3sstr4i 3607 |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 ⊆ ((0[,]1) ×
(0[,]1)) |
37 | 20, 20, 14, 14 | txunii 21206 |
. . . . . . . . . . . . . . . . 17
⊢ ((0[,]1)
× (0[,]1)) = ∪ (II ×t
II) |
38 | 37 | ntropn 20663 |
. . . . . . . . . . . . . . . 16
⊢ (((II
×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) →
((int‘(II ×t II))‘𝑆) ∈ (II ×t
II)) |
39 | 22, 36, 38 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢
((int‘(II ×t II))‘𝑆) ∈ (II ×t
II) |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((int‘(II
×t II))‘𝑆) ∈ (II ×t
II)) |
41 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
42 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
43 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑃 ∈ 𝐵) |
44 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (𝐹‘𝑃) = (0𝐺0)) |
45 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
46 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑏 ∈ (0[,]1)) |
47 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑎 ∈ (0[,]1)) |
48 | 1, 41, 42, 43, 44, 6, 7, 45, 46, 47 | cvmlift2lem10 30548 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) |
49 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → (II
×t II) ∈ Top) |
50 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑆 ⊆ ((0[,]1) ×
(0[,]1))) |
51 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → II ∈
Top) |
52 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑢 ∈ II) |
53 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑣 ∈ II) |
54 | | txopn 21215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (𝑢 × 𝑣) ∈ (II ×t
II)) |
55 | 51, 51, 52, 53, 54 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ∈ (II ×t
II)) |
56 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ 𝑣) |
57 | | elunii 4377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ ∪
II) |
58 | 57, 14 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ (0[,]1)) |
59 | 56, 53, 58 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ (0[,]1)) |
60 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → II ∈ Top) |
61 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ II) |
62 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑟 ∈ 𝑢) |
63 | | opnneip 20733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((II
∈ Top ∧ 𝑢 ∈
II ∧ 𝑟 ∈ 𝑢) → 𝑢 ∈ ((nei‘II)‘{𝑟})) |
64 | 60, 61, 62, 63 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ ((nei‘II)‘{𝑟})) |
65 | 41 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
66 | 42 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
67 | 43 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑃 ∈ 𝐵) |
68 | 44 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝐹‘𝑃) = (0𝐺0)) |
69 | | cvmlift2.m |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)} |
70 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑣 ∈ II) |
71 | | simplr2 1097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑎 ∈ 𝑣) |
72 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ 𝑣) |
73 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑐 = 𝑤 → {𝑐} = {𝑤}) |
74 | 73 | xpeq2d 5063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤})) |
75 | 74 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤}))) |
76 | 74 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 = 𝑤 → ((II ×t II)
↾t (𝑢
× {𝑐})) = ((II
×t II) ↾t (𝑢 × {𝑤}))) |
77 | 76 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 = 𝑤 → (((II ×t II)
↾t (𝑢
× {𝑐})) Cn 𝐶) = (((II ×t
II) ↾t (𝑢
× {𝑤})) Cn 𝐶)) |
78 | 75, 77 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×t II)
↾t (𝑢
× {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) |
79 | 78 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑐 ∈
𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×t II)
↾t (𝑢
× {𝑐})) Cn 𝐶) ↔ ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶)) |
80 | | simplr3 1098 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 𝐶))) |
81 | 79, 80 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 𝐶))) |
82 | 1, 65, 66, 67, 68, 6, 7, 69, 61, 70, 71, 72, 81 | cvmlift2lem11 30549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀)) |
83 | 1, 65, 66, 67, 68, 6, 7, 69, 61, 70, 72, 71, 81 | cvmlift2lem11 30549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑡}) ⊆ 𝑀 → (𝑢 × {𝑎}) ⊆ 𝑀)) |
84 | 82, 83 | impbid 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
85 | | rspe 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑢 ∈
((nei‘II)‘{𝑟})
∧ ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
86 | 64, 84, 85 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
87 | 59, 86 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
88 | 87 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
89 | 88 | alrimivv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
90 | | df-xp 5044 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 × 𝑣) = {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} |
91 | 90, 34 | sseq12i 3594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}) |
92 | | ssopab2b 4927 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
({〈𝑟, 𝑡〉 ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
93 | 91, 92 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
94 | 89, 93 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ 𝑆) |
95 | 37 | ssntr 20672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((II
×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) ∧
((𝑢 × 𝑣) ∈ (II ×t
II) ∧ (𝑢 × 𝑣) ⊆ 𝑆)) → (𝑢 × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆)) |
96 | 49, 50, 55, 94, 95 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆)) |
97 | | simpr1 1060 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑏 ∈ 𝑢) |
98 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 𝑎 ∈ 𝑣) |
99 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣) → 〈𝑏, 𝑎〉 ∈ (𝑢 × 𝑣)) |
100 | 97, 98, 99 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 〈𝑏, 𝑎〉 ∈ (𝑢 × 𝑣)) |
101 | 96, 100 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) → 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆)) |
102 | 101 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆))) |
103 | 102 | rexlimdvva 3020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆))) |
104 | 48, 103 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆)) |
105 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑎 ∈ V |
106 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑎 → 〈𝑏, 𝑤〉 = 〈𝑏, 𝑎〉) |
107 | 106 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑎 → (〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆) ↔ 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆))) |
108 | 105, 107 | ralsn 4169 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑤 ∈
{𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆) ↔ 〈𝑏, 𝑎〉 ∈ ((int‘(II
×t II))‘𝑆)) |
109 | 104, 108 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
110 | 109 | anassrs 678 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑏 ∈ (0[,]1)) → ∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
111 | 110 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
112 | | dfss3 3558 |
. . . . . . . . . . . . . . . 16
⊢ (((0[,]1)
× {𝑎}) ⊆
((int‘(II ×t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×t
II))‘𝑆)) |
113 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 〈𝑏, 𝑤〉 → (𝑢 ∈ ((int‘(II ×t
II))‘𝑆) ↔
〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆))) |
114 | 113 | ralxp 5185 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑢 ∈
((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II
×t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
115 | 112, 114 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢ (((0[,]1)
× {𝑎}) ⊆
((int‘(II ×t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}〈𝑏, 𝑤〉 ∈ ((int‘(II
×t II))‘𝑆)) |
116 | 111, 115 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((0[,]1) ×
{𝑎}) ⊆
((int‘(II ×t II))‘𝑆)) |
117 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → 𝑎 ∈ (0[,]1)) |
118 | 14, 14, 19, 21, 40, 116, 117 | txtube 21253 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆))) |
119 | 37 | ntrss2 20671 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((II
×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) →
((int‘(II ×t II))‘𝑆) ⊆ 𝑆) |
120 | 22, 36, 119 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢
((int‘(II ×t II))‘𝑆) ⊆ 𝑆 |
121 | | sstr 3576 |
. . . . . . . . . . . . . . . . . 18
⊢
((((0[,]1) × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆) ∧
((int‘(II ×t II))‘𝑆) ⊆ 𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆) |
122 | 120, 121 | mpan2 703 |
. . . . . . . . . . . . . . . . 17
⊢ (((0[,]1)
× 𝑣) ⊆
((int‘(II ×t II))‘𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆) |
123 | | df-xp 5044 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0[,]1)
× 𝑣) = {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} |
124 | 123, 34 | sseq12i 3594 |
. . . . . . . . . . . . . . . . . 18
⊢ (((0[,]1)
× 𝑣) ⊆ 𝑆 ↔ {〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}) |
125 | | ssopab2b 4927 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
126 | | r2al 2923 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑟 ∈
(0[,]1)∀𝑡 ∈
𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))) |
127 | | ralcom 3079 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑟 ∈
(0[,]1)∀𝑡 ∈
𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
128 | 125, 126,
127 | 3bitr2i 287 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈𝑟, 𝑡〉 ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
129 | 124, 128 | bitri 263 |
. . . . . . . . . . . . . . . . 17
⊢ (((0[,]1)
× 𝑣) ⊆ 𝑆 ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
130 | 122, 129 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (((0[,]1)
× 𝑣) ⊆
((int‘(II ×t II))‘𝑆) → ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))) |
131 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ (0[,]1) ∧
∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
132 | 131 | ralimi 2936 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑟 ∈
(0[,]1)(𝑡 ∈ (0[,]1)
∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) |
133 | | cvmlift2lem1 30538 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
134 | | bicom 211 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀)) |
135 | 134 | rexbii 3023 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀)) |
136 | 135 | ralbii 2963 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀)) |
137 | | cvmlift2lem1 30538 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
138 | 136, 137 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
139 | 133, 138 | impbid 201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑟 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
140 | 132, 139 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑟 ∈
(0[,]1)(𝑡 ∈ (0[,]1)
∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
141 | 13 | rabeq2i 3170 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ 𝐴 ↔ (𝑎 ∈ (0[,]1) ∧ ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
142 | 141 | baib 942 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ (0[,]1) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
143 | 142 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀)) |
144 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∈ II → 𝑣 ⊆ ∪ II) |
145 | 144, 14 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ II → 𝑣 ⊆
(0[,]1)) |
146 | 145 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1)) |
147 | 146 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ (0[,]1)) |
148 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑡 → {𝑎} = {𝑡}) |
149 | 148 | xpeq2d 5063 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡})) |
150 | 149 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
151 | 150, 13 | elrab2 3333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ 𝐴 ↔ (𝑡 ∈ (0[,]1) ∧ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
152 | 151 | baib 942 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ (0[,]1) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
153 | 147, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)) |
154 | 143, 153 | bibi12d 334 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → ((𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴) ↔ (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))) |
155 | 140, 154 | syl5ibr 235 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
156 | 155 | ralimdva 2945 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
157 | 130, 156 | syl5 33 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (((0[,]1) × 𝑣) ⊆ ((int‘(II
×t II))‘𝑆) → ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
158 | 157 | anim2d 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → ((𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆)) →
(𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))) |
159 | 158 | reximdva 3000 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t
II))‘𝑆)) →
∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))) |
160 | 118, 159 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
161 | 160 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
162 | | ssrab2 3650 |
. . . . . . . . . . . . 13
⊢ {𝑎 ∈ (0[,]1) ∣ ((0[,]1)
× {𝑎}) ⊆ 𝑀} ⊆
(0[,]1) |
163 | 13, 162 | eqsstri 3598 |
. . . . . . . . . . . 12
⊢ 𝐴 ⊆
(0[,]1) |
164 | 14 | isclo 20701 |
. . . . . . . . . . . 12
⊢ ((II
∈ Top ∧ 𝐴 ⊆
(0[,]1)) → (𝐴 ∈
(II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))) |
165 | 20, 163, 164 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (II ∩
(Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))) |
166 | 161, 165 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (II ∩
(Clsd‘II))) |
167 | 17, 166 | sseldi 3566 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ II) |
168 | | 0elunit 12161 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]1) |
169 | 168 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
(0[,]1)) |
170 | | relxp 5150 |
. . . . . . . . . . . . 13
⊢ Rel
((0[,]1) × {0}) |
171 | 170 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → Rel ((0[,]1) ×
{0})) |
172 | | opelxp 5070 |
. . . . . . . . . . . . 13
⊢
(〈𝑟, 𝑎〉 ∈ ((0[,]1) ×
{0}) ↔ (𝑟 ∈
(0[,]1) ∧ 𝑎 ∈
{0})) |
173 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈
(0[,]1)) |
174 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑟 ∈ (0[,]1) ∧ 0 ∈
(0[,]1)) → 〈𝑟,
0〉 ∈ ((0[,]1) × (0[,]1))) |
175 | 173, 169,
174 | syl2anr 494 |
. . . . . . . . . . . . . . . 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 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝑟 ∈ (0[,]1)) |
181 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 0 ∈
(0[,]1)) |
182 | 1, 176, 177, 178, 179, 6, 7, 45, 180, 181 | cvmlift2lem10 30548 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) |
183 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . 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 792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 0 ∈ 𝑣) |
185 | 8 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
186 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐾:((0[,]1) ×
(0[,]1))⟶𝐵 →
𝐾 Fn ((0[,]1) ×
(0[,]1))) |
187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 Fn ((0[,]1) ×
(0[,]1))) |
188 | | fnov 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐾 Fn ((0[,]1) × (0[,]1))
↔ 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤))) |
189 | 187, 188 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤))) |
190 | 189 | reseq1d 5316 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0}))) |
191 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II) |
192 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 ∈ II → 𝑢 ⊆ ∪ II) |
193 | 192, 14 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 ∈ II → 𝑢 ⊆
(0[,]1)) |
194 | 191, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1)) |
195 | 169 | snssd 4281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → {0} ⊆
(0[,]1)) |
196 | 195 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → {0} ⊆
(0[,]1)) |
197 | | resmpt2 6656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 ⊆ (0[,]1) ∧ {0}
⊆ (0[,]1)) → ((𝑏
∈ (0[,]1), 𝑤 ∈
(0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤))) |
198 | 194, 196,
197 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤))) |
199 | 194 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → 𝑏 ∈ (0[,]1)) |
200 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝜑) |
201 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem8 30546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏)) |
202 | 200, 201 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏)) |
203 | 199, 202 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑏𝐾0) = (𝐻‘𝑏)) |
204 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ {0} → 𝑤 = 0) |
205 | 204 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0)) |
206 | 205 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {0} → ((𝑏𝐾𝑤) = (𝐻‘𝑏) ↔ (𝑏𝐾0) = (𝐻‘𝑏))) |
207 | 203, 206 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝐻‘𝑏))) |
208 | 207 | 3impia 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢 ∧ 𝑤 ∈ {0}) → (𝑏𝐾𝑤) = (𝐻‘𝑏)) |
209 | 208 | mpt2eq3dva 6617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏))) |
210 | 190, 198,
209 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏))) |
211 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (II
↾t 𝑢) =
(II ↾t 𝑢) |
212 | | iitopon 22490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ II ∈
(TopOn‘(0[,]1)) |
213 | 212 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈
(TopOn‘(0[,]1))) |
214 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (II
↾t {0}) = (II ↾t {0}) |
215 | 213, 213 | cnmpt1st 21281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×t II) Cn
II)) |
216 | 1, 2, 3, 4, 5, 6 | cvmlift2lem2 30540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃)) |
217 | 216 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐶)) |
218 | 200, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐻 ∈ (II Cn 𝐶)) |
219 | 213, 213,
215, 218 | cnmpt21f 21285 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻‘𝑏)) ∈ ((II ×t II) Cn
𝐶)) |
220 | 211, 213,
194, 214, 213, 196, 219 | cnmpt2res 21290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ↾t 𝑢) ×t (II
↾t {0})) Cn 𝐶)) |
221 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑢 ∈ V |
222 | | snex 4835 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {0}
∈ V |
223 | | txrest 21244 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ V ∧ {0} ∈ V)) → ((II
×t II) ↾t (𝑢 × {0})) = ((II ↾t
𝑢) ×t (II
↾t {0}))) |
224 | 20, 20, 221, 222, 223 | mp4an 705 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((II
×t II) ↾t (𝑢 × {0})) = ((II ↾t
𝑢) ×t (II
↾t {0})) |
225 | 224 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((II
×t II) ↾t (𝑢 × {0})) Cn 𝐶) = (((II ↾t 𝑢) ×t (II
↾t {0})) Cn 𝐶) |
226 | 220, 225 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ×t II)
↾t (𝑢
× {0})) Cn 𝐶)) |
227 | 210, 226 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II
×t II) ↾t (𝑢 × {0})) Cn 𝐶)) |
228 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 0 → {𝑤} = {0}) |
229 | 228 | xpeq2d 5063 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0})) |
230 | 229 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0}))) |
231 | 229 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 0 → ((II
×t II) ↾t (𝑢 × {𝑤})) = ((II ×t II)
↾t (𝑢
× {0}))) |
232 | 231 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 0 → (((II
×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×t II)
↾t (𝑢
× {0})) Cn 𝐶)) |
233 | 230, 232 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II
×t II) ↾t (𝑢 × {0})) Cn 𝐶))) |
234 | 233 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {0})) ∈ (((II
×t II) ↾t (𝑢 × {0})) Cn 𝐶)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶)) |
235 | 184, 227,
234 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶)) |
236 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) → 〈𝑟, 0〉 ∈ (𝑢 × 𝑣)) |
237 | 236 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 〈𝑟, 0〉 ∈ (𝑢 × 𝑣)) |
238 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ∈ II) |
239 | 238, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ⊆ (0[,]1)) |
240 | | xpss12 5148 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑢 ⊆ (0[,]1) ∧ 𝑣 ⊆ (0[,]1)) → (𝑢 × 𝑣) ⊆ ((0[,]1) ×
(0[,]1))) |
241 | 194, 239,
240 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ⊆ ((0[,]1) ×
(0[,]1))) |
242 | 37 | restuni 20776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((II
×t II) ∈ Top ∧ (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1))) →
(𝑢 × 𝑣) = ∪
((II ×t II) ↾t (𝑢 × 𝑣))) |
243 | 22, 241, 242 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) = ∪ ((II
×t II) ↾t (𝑢 × 𝑣))) |
244 | 237, 243 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 〈𝑟, 0〉 ∈ ∪
((II ×t II) ↾t (𝑢 × 𝑣))) |
245 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∪ ((II ×t II) ↾t (𝑢 × 𝑣)) = ∪ ((II
×t II) ↾t (𝑢 × 𝑣)) |
246 | 245 | cncnpi 20892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶) ∧ 〈𝑟, 0〉 ∈ ∪
((II ×t II) ↾t (𝑢 × 𝑣))) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II)
↾t (𝑢
× 𝑣)) CnP 𝐶)‘〈𝑟, 0〉)) |
247 | 246 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑟, 0〉
∈ ∪ ((II ×t II)
↾t (𝑢
× 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II)
↾t (𝑢
× 𝑣)) CnP 𝐶)‘〈𝑟, 0〉))) |
248 | 244, 247 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II)
↾t (𝑢
× 𝑣)) CnP 𝐶)‘〈𝑟, 0〉))) |
249 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (II ×t II) ∈
Top) |
250 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ Top) |
251 | 250, 250,
191, 238, 54 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ∈ (II ×t
II)) |
252 | | isopn3i 20696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((II
×t II) ∈ Top ∧ (𝑢 × 𝑣) ∈ (II ×t II)) →
((int‘(II ×t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣)) |
253 | 22, 251, 252 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((int‘(II ×t
II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣)) |
254 | 237, 253 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 〈𝑟, 0〉 ∈ ((int‘(II
×t II))‘(𝑢 × 𝑣))) |
255 | 37, 1 | cnprest 20903 |
. . . . . . . . . . . . . . . . . . . . . . 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〉))) |
256 | 249, 241,
254, 185, 255 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉) ↔ (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II)
↾t (𝑢
× 𝑣)) CnP 𝐶)‘〈𝑟, 0〉))) |
257 | 248, 256 | sylibrd 248 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
258 | 235, 257 | embantd 57 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
259 | 258 | expimpd 627 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
260 | 183, 259 | syl5bi 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
261 | 260 | rexlimdvva 3020 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
262 | 182, 261 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉)) |
263 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑟, 0〉 → (((II ×t
II) CnP 𝐶)‘𝑧) = (((II ×t
II) CnP 𝐶)‘〈𝑟, 0〉)) |
264 | 263 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑟, 0〉 → (𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
265 | 264, 69 | elrab2 3333 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑟, 0〉
∈ 𝑀 ↔
(〈𝑟, 0〉 ∈
((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×t II) CnP
𝐶)‘〈𝑟, 0〉))) |
266 | 175, 262,
265 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 〈𝑟, 0〉 ∈ 𝑀) |
267 | | elsni 4142 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ {0} → 𝑎 = 0) |
268 | 267 | opeq2d 4347 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ {0} → 〈𝑟, 𝑎〉 = 〈𝑟, 0〉) |
269 | 268 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {0} → (〈𝑟, 𝑎〉 ∈ 𝑀 ↔ 〈𝑟, 0〉 ∈ 𝑀)) |
270 | 266, 269 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (𝑎 ∈ {0} → 〈𝑟, 𝑎〉 ∈ 𝑀)) |
271 | 270 | expimpd 627 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}) → 〈𝑟, 𝑎〉 ∈ 𝑀)) |
272 | 172, 271 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝑟, 𝑎〉 ∈ ((0[,]1) × {0}) →
〈𝑟, 𝑎〉 ∈ 𝑀)) |
273 | 171, 272 | relssdv 5135 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0[,]1) × {0})
⊆ 𝑀) |
274 | | sneq 4135 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 0 → {𝑎} = {0}) |
275 | 274 | xpeq2d 5063 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 0 → ((0[,]1) ×
{𝑎}) = ((0[,]1) ×
{0})) |
276 | 275 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑎 = 0 → (((0[,]1) ×
{𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0})
⊆ 𝑀)) |
277 | 276, 13 | elrab2 3333 |
. . . . . . . . . . 11
⊢ (0 ∈
𝐴 ↔ (0 ∈ (0[,]1)
∧ ((0[,]1) × {0}) ⊆ 𝑀)) |
278 | 169, 273,
277 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ 𝐴) |
279 | | ne0i 3880 |
. . . . . . . . . 10
⊢ (0 ∈
𝐴 → 𝐴 ≠ ∅) |
280 | 278, 279 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ ∅) |
281 | | inss2 3796 |
. . . . . . . . . 10
⊢ (II ∩
(Clsd‘II)) ⊆ (Clsd‘II) |
282 | 281, 166 | sseldi 3566 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (Clsd‘II)) |
283 | 14, 16, 167, 280, 282 | conclo 21028 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = (0[,]1)) |
284 | 13, 283 | syl5reqr 2659 |
. . . . . . 7
⊢ (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1)
× {𝑎}) ⊆ 𝑀}) |
285 | | rabid2 3096 |
. . . . . . 7
⊢ ((0[,]1)
= {𝑎 ∈ (0[,]1) ∣
((0[,]1) × {𝑎})
⊆ 𝑀} ↔
∀𝑎 ∈
(0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀) |
286 | 284, 285 | sylib 207 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀) |
287 | | iunss 4497 |
. . . . . 6
⊢ (∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀) |
288 | 286, 287 | sylibr 223 |
. . . . 5
⊢ (𝜑 → ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀) |
289 | 12, 288 | syl5eqss 3612 |
. . . 4
⊢ (𝜑 → ((0[,]1) × (0[,]1))
⊆ 𝑀) |
290 | 289, 69 | syl6sseq 3614 |
. . 3
⊢ (𝜑 → ((0[,]1) × (0[,]1))
⊆ {𝑧 ∈ ((0[,]1)
× (0[,]1)) ∣ 𝐾
∈ (((II ×t II) CnP 𝐶)‘𝑧)}) |
291 | | ssrab 3643 |
. . . 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 𝐶)‘𝑧))) |
292 | 291 | simprbi 479 |
. . 3
⊢ (((0[,]1)
× (0[,]1)) ⊆ {𝑧
∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧)} → ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)) |
293 | 290, 292 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)) |
294 | | txtopon 21204 |
. . . 4
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II
×t II) ∈ (TopOn‘((0[,]1) ×
(0[,]1)))) |
295 | 212, 212,
294 | mp2an 704 |
. . 3
⊢ (II
×t II) ∈ (TopOn‘((0[,]1) ×
(0[,]1))) |
296 | | cvmtop1 30496 |
. . . . 5
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
297 | 2, 296 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Top) |
298 | 1 | toptopon 20548 |
. . . 4
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
299 | 297, 298 | sylib 207 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
300 | | cncnp 20894 |
. . 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 𝐶)‘𝑧)))) |
301 | 295, 299,
300 | sylancr 694 |
. 2
⊢ (𝜑 → (𝐾 ∈ ((II ×t II) Cn
𝐶) ↔ (𝐾:((0[,]1) ×
(0[,]1))⟶𝐵 ∧
∀𝑧 ∈ ((0[,]1)
× (0[,]1))𝐾 ∈
(((II ×t II) CnP 𝐶)‘𝑧)))) |
302 | 8, 293, 301 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐾 ∈ ((II ×t II) Cn
𝐶)) |