Step | Hyp | Ref
| Expression |
1 | | biimp 214 |
. . . . . 6
⊢ (((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → ((𝑢 × {𝑥}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀)) |
2 | | iitop 24041 |
. . . . . . . . . . 11
⊢ II ∈
Top |
3 | | iiuni 24042 |
. . . . . . . . . . . 12
⊢ (0[,]1) =
∪ II |
4 | 3 | neii1 22255 |
. . . . . . . . . . 11
⊢ ((II
∈ Top ∧ 𝑢 ∈
((nei‘II)‘{𝑦}))
→ 𝑢 ⊆
(0[,]1)) |
5 | 2, 4 | mpan 687 |
. . . . . . . . . 10
⊢ (𝑢 ∈
((nei‘II)‘{𝑦})
→ 𝑢 ⊆
(0[,]1)) |
6 | 5 | adantl 482 |
. . . . . . . . 9
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → 𝑢 ⊆ (0[,]1)) |
7 | | xpss1 5609 |
. . . . . . . . 9
⊢ (𝑢 ⊆ (0[,]1) → (𝑢 × {𝑥}) ⊆ ((0[,]1) × {𝑥})) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → (𝑢 × {𝑥}) ⊆ ((0[,]1) × {𝑥})) |
9 | | simpl 483 |
. . . . . . . 8
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → ((0[,]1) ×
{𝑥}) ⊆ 𝑀) |
10 | 8, 9 | sstrd 3936 |
. . . . . . 7
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → (𝑢 × {𝑥}) ⊆ 𝑀) |
11 | | ssnei 22259 |
. . . . . . . . . . . 12
⊢ ((II
∈ Top ∧ 𝑢 ∈
((nei‘II)‘{𝑦}))
→ {𝑦} ⊆ 𝑢) |
12 | 2, 11 | mpan 687 |
. . . . . . . . . . 11
⊢ (𝑢 ∈
((nei‘II)‘{𝑦})
→ {𝑦} ⊆ 𝑢) |
13 | 12 | adantl 482 |
. . . . . . . . . 10
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → {𝑦} ⊆ 𝑢) |
14 | | vex 3435 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
15 | 14 | snss 4725 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑢 ↔ {𝑦} ⊆ 𝑢) |
16 | 13, 15 | sylibr 233 |
. . . . . . . . 9
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → 𝑦 ∈ 𝑢) |
17 | | vsnid 4604 |
. . . . . . . . 9
⊢ 𝑡 ∈ {𝑡} |
18 | | opelxpi 5627 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑢 ∧ 𝑡 ∈ {𝑡}) → 〈𝑦, 𝑡〉 ∈ (𝑢 × {𝑡})) |
19 | 16, 17, 18 | sylancl 586 |
. . . . . . . 8
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → 〈𝑦, 𝑡〉 ∈ (𝑢 × {𝑡})) |
20 | | ssel 3919 |
. . . . . . . 8
⊢ ((𝑢 × {𝑡}) ⊆ 𝑀 → (〈𝑦, 𝑡〉 ∈ (𝑢 × {𝑡}) → 〈𝑦, 𝑡〉 ∈ 𝑀)) |
21 | 19, 20 | syl5com 31 |
. . . . . . 7
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → ((𝑢 × {𝑡}) ⊆ 𝑀 → 〈𝑦, 𝑡〉 ∈ 𝑀)) |
22 | 10, 21 | embantd 59 |
. . . . . 6
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → (((𝑢 × {𝑥}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀) → 〈𝑦, 𝑡〉 ∈ 𝑀)) |
23 | 1, 22 | syl5 34 |
. . . . 5
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → (((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 〈𝑦, 𝑡〉 ∈ 𝑀)) |
24 | 23 | rexlimdva 3215 |
. . . 4
⊢ (((0[,]1)
× {𝑥}) ⊆ 𝑀 → (∃𝑢 ∈
((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 〈𝑦, 𝑡〉 ∈ 𝑀)) |
25 | 24 | ralimdv 3106 |
. . 3
⊢ (((0[,]1)
× {𝑥}) ⊆ 𝑀 → (∀𝑦 ∈ (0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → ∀𝑦 ∈ (0[,]1)〈𝑦, 𝑡〉 ∈ 𝑀)) |
26 | 25 | com12 32 |
. 2
⊢
(∀𝑦 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ∀𝑦 ∈ (0[,]1)〈𝑦, 𝑡〉 ∈ 𝑀)) |
27 | | dfss3 3914 |
. . 3
⊢ (((0[,]1)
× {𝑡}) ⊆ 𝑀 ↔ ∀𝑧 ∈ ((0[,]1) × {𝑡})𝑧 ∈ 𝑀) |
28 | | eleq1 2828 |
. . . 4
⊢ (𝑧 = 〈𝑦, 𝑢〉 → (𝑧 ∈ 𝑀 ↔ 〈𝑦, 𝑢〉 ∈ 𝑀)) |
29 | 28 | ralxp 5749 |
. . 3
⊢
(∀𝑧 ∈
((0[,]1) × {𝑡})𝑧 ∈ 𝑀 ↔ ∀𝑦 ∈ (0[,]1)∀𝑢 ∈ {𝑡}〈𝑦, 𝑢〉 ∈ 𝑀) |
30 | | vex 3435 |
. . . . 5
⊢ 𝑡 ∈ V |
31 | | opeq2 4811 |
. . . . . 6
⊢ (𝑢 = 𝑡 → 〈𝑦, 𝑢〉 = 〈𝑦, 𝑡〉) |
32 | 31 | eleq1d 2825 |
. . . . 5
⊢ (𝑢 = 𝑡 → (〈𝑦, 𝑢〉 ∈ 𝑀 ↔ 〈𝑦, 𝑡〉 ∈ 𝑀)) |
33 | 30, 32 | ralsn 4623 |
. . . 4
⊢
(∀𝑢 ∈
{𝑡}〈𝑦, 𝑢〉 ∈ 𝑀 ↔ 〈𝑦, 𝑡〉 ∈ 𝑀) |
34 | 33 | ralbii 3093 |
. . 3
⊢
(∀𝑦 ∈
(0[,]1)∀𝑢 ∈
{𝑡}〈𝑦, 𝑢〉 ∈ 𝑀 ↔ ∀𝑦 ∈ (0[,]1)〈𝑦, 𝑡〉 ∈ 𝑀) |
35 | 27, 29, 34 | 3bitri 297 |
. 2
⊢ (((0[,]1)
× {𝑡}) ⊆ 𝑀 ↔ ∀𝑦 ∈ (0[,]1)〈𝑦, 𝑡〉 ∈ 𝑀) |
36 | 26, 35 | syl6ibr 251 |
1
⊢
(∀𝑦 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀)) |