| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | biimp 215 | . . . . . 6
⊢ (((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → ((𝑢 × {𝑥}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀)) | 
| 2 |  | iitop 24906 | . . . . . . . . . . 11
⊢ II ∈
Top | 
| 3 |  | iiuni 24907 | . . . . . . . . . . . 12
⊢ (0[,]1) =
∪ II | 
| 4 | 3 | neii1 23114 | . . . . . . . . . . 11
⊢ ((II
∈ Top ∧ 𝑢 ∈
((nei‘II)‘{𝑦}))
→ 𝑢 ⊆
(0[,]1)) | 
| 5 | 2, 4 | mpan 690 | . . . . . . . . . 10
⊢ (𝑢 ∈
((nei‘II)‘{𝑦})
→ 𝑢 ⊆
(0[,]1)) | 
| 6 | 5 | adantl 481 | . . . . . . . . 9
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → 𝑢 ⊆ (0[,]1)) | 
| 7 |  | xpss1 5704 | . . . . . . . . 9
⊢ (𝑢 ⊆ (0[,]1) → (𝑢 × {𝑥}) ⊆ ((0[,]1) × {𝑥})) | 
| 8 | 6, 7 | syl 17 | . . . . . . . 8
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → (𝑢 × {𝑥}) ⊆ ((0[,]1) × {𝑥})) | 
| 9 |  | simpl 482 | . . . . . . . 8
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → ((0[,]1) ×
{𝑥}) ⊆ 𝑀) | 
| 10 | 8, 9 | sstrd 3994 | . . . . . . 7
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → (𝑢 × {𝑥}) ⊆ 𝑀) | 
| 11 |  | ssnei 23118 | . . . . . . . . . . . 12
⊢ ((II
∈ Top ∧ 𝑢 ∈
((nei‘II)‘{𝑦}))
→ {𝑦} ⊆ 𝑢) | 
| 12 | 2, 11 | mpan 690 | . . . . . . . . . . 11
⊢ (𝑢 ∈
((nei‘II)‘{𝑦})
→ {𝑦} ⊆ 𝑢) | 
| 13 | 12 | adantl 481 | . . . . . . . . . 10
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → {𝑦} ⊆ 𝑢) | 
| 14 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑦 ∈ V | 
| 15 | 14 | snss 4785 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝑢 ↔ {𝑦} ⊆ 𝑢) | 
| 16 | 13, 15 | sylibr 234 | . . . . . . . . 9
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → 𝑦 ∈ 𝑢) | 
| 17 |  | vsnid 4663 | . . . . . . . . 9
⊢ 𝑡 ∈ {𝑡} | 
| 18 |  | opelxpi 5722 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝑢 ∧ 𝑡 ∈ {𝑡}) → 〈𝑦, 𝑡〉 ∈ (𝑢 × {𝑡})) | 
| 19 | 16, 17, 18 | sylancl 586 | . . . . . . . 8
⊢
((((0[,]1) × {𝑥}) ⊆ 𝑀 ∧ 𝑢 ∈ ((nei‘II)‘{𝑦})) → 〈𝑦, 𝑡〉 ∈ (𝑢 × {𝑡})) | 
| 20 |  | ssel 3977 | . . . . . . . 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 3155 | . . . 4
⊢ (((0[,]1)
× {𝑥}) ⊆ 𝑀 → (∃𝑢 ∈
((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 〈𝑦, 𝑡〉 ∈ 𝑀)) | 
| 25 | 24 | ralimdv 3169 | . . 3
⊢ (((0[,]1)
× {𝑥}) ⊆ 𝑀 → (∀𝑦 ∈ (0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → ∀𝑦 ∈ (0[,]1)〈𝑦, 𝑡〉 ∈ 𝑀)) | 
| 26 | 25 | com12 32 | . 2
⊢
(∀𝑦 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ∀𝑦 ∈ (0[,]1)〈𝑦, 𝑡〉 ∈ 𝑀)) | 
| 27 |  | dfss3 3972 | . . 3
⊢ (((0[,]1)
× {𝑡}) ⊆ 𝑀 ↔ ∀𝑧 ∈ ((0[,]1) × {𝑡})𝑧 ∈ 𝑀) | 
| 28 |  | eleq1 2829 | . . . 4
⊢ (𝑧 = 〈𝑦, 𝑢〉 → (𝑧 ∈ 𝑀 ↔ 〈𝑦, 𝑢〉 ∈ 𝑀)) | 
| 29 | 28 | ralxp 5852 | . . 3
⊢
(∀𝑧 ∈
((0[,]1) × {𝑡})𝑧 ∈ 𝑀 ↔ ∀𝑦 ∈ (0[,]1)∀𝑢 ∈ {𝑡}〈𝑦, 𝑢〉 ∈ 𝑀) | 
| 30 |  | vex 3484 | . . . . 5
⊢ 𝑡 ∈ V | 
| 31 |  | opeq2 4874 | . . . . . 6
⊢ (𝑢 = 𝑡 → 〈𝑦, 𝑢〉 = 〈𝑦, 𝑡〉) | 
| 32 | 31 | eleq1d 2826 | . . . . 5
⊢ (𝑢 = 𝑡 → (〈𝑦, 𝑢〉 ∈ 𝑀 ↔ 〈𝑦, 𝑡〉 ∈ 𝑀)) | 
| 33 | 30, 32 | ralsn 4681 | . . . 4
⊢
(∀𝑢 ∈
{𝑡}〈𝑦, 𝑢〉 ∈ 𝑀 ↔ 〈𝑦, 𝑡〉 ∈ 𝑀) | 
| 34 | 33 | ralbii 3093 | . . 3
⊢
(∀𝑦 ∈
(0[,]1)∀𝑢 ∈
{𝑡}〈𝑦, 𝑢〉 ∈ 𝑀 ↔ ∀𝑦 ∈ (0[,]1)〈𝑦, 𝑡〉 ∈ 𝑀) | 
| 35 | 27, 29, 34 | 3bitri 297 | . 2
⊢ (((0[,]1)
× {𝑡}) ⊆ 𝑀 ↔ ∀𝑦 ∈ (0[,]1)〈𝑦, 𝑡〉 ∈ 𝑀) | 
| 36 | 26, 35 | imbitrrdi 252 | 1
⊢
(∀𝑦 ∈
(0[,]1)∃𝑢 ∈
((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀)) |