Step |
Hyp |
Ref |
Expression |
1 |
|
biimp |
⊢ ( ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 → ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) ) |
2 |
|
iitop |
⊢ II ∈ Top |
3 |
|
iiuni |
⊢ ( 0 [,] 1 ) = ∪ II |
4 |
3
|
neii1 |
⊢ ( ( II ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → 𝑢 ⊆ ( 0 [,] 1 ) ) |
5 |
2 4
|
mpan |
⊢ ( 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) → 𝑢 ⊆ ( 0 [,] 1 ) ) |
6 |
5
|
adantl |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → 𝑢 ⊆ ( 0 [,] 1 ) ) |
7 |
|
xpss1 |
⊢ ( 𝑢 ⊆ ( 0 [,] 1 ) → ( 𝑢 × { 𝑥 } ) ⊆ ( ( 0 [,] 1 ) × { 𝑥 } ) ) |
8 |
6 7
|
syl |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( 𝑢 × { 𝑥 } ) ⊆ ( ( 0 [,] 1 ) × { 𝑥 } ) ) |
9 |
|
simpl |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ) |
10 |
8 9
|
sstrd |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ) |
11 |
|
ssnei |
⊢ ( ( II ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → { 𝑦 } ⊆ 𝑢 ) |
12 |
2 11
|
mpan |
⊢ ( 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) → { 𝑦 } ⊆ 𝑢 ) |
13 |
12
|
adantl |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → { 𝑦 } ⊆ 𝑢 ) |
14 |
|
vex |
⊢ 𝑦 ∈ V |
15 |
14
|
snss |
⊢ ( 𝑦 ∈ 𝑢 ↔ { 𝑦 } ⊆ 𝑢 ) |
16 |
13 15
|
sylibr |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → 𝑦 ∈ 𝑢 ) |
17 |
|
vsnid |
⊢ 𝑡 ∈ { 𝑡 } |
18 |
|
opelxpi |
⊢ ( ( 𝑦 ∈ 𝑢 ∧ 𝑡 ∈ { 𝑡 } ) → 〈 𝑦 , 𝑡 〉 ∈ ( 𝑢 × { 𝑡 } ) ) |
19 |
16 17 18
|
sylancl |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → 〈 𝑦 , 𝑡 〉 ∈ ( 𝑢 × { 𝑡 } ) ) |
20 |
|
ssel |
⊢ ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 → ( 〈 𝑦 , 𝑡 〉 ∈ ( 𝑢 × { 𝑡 } ) → 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) ) |
21 |
19 20
|
syl5com |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 → 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) ) |
22 |
10 21
|
embantd |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 → ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) ) |
23 |
1 22
|
syl5 |
⊢ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) ) |
24 |
23
|
rexlimdva |
⊢ ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ( ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) ) |
25 |
24
|
ralimdv |
⊢ ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ∀ 𝑦 ∈ ( 0 [,] 1 ) 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) ) |
26 |
25
|
com12 |
⊢ ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ∀ 𝑦 ∈ ( 0 [,] 1 ) 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) ) |
27 |
|
dfss3 |
⊢ ( ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ↔ ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × { 𝑡 } ) 𝑧 ∈ 𝑀 ) |
28 |
|
eleq1 |
⊢ ( 𝑧 = 〈 𝑦 , 𝑢 〉 → ( 𝑧 ∈ 𝑀 ↔ 〈 𝑦 , 𝑢 〉 ∈ 𝑀 ) ) |
29 |
28
|
ralxp |
⊢ ( ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × { 𝑡 } ) 𝑧 ∈ 𝑀 ↔ ∀ 𝑦 ∈ ( 0 [,] 1 ) ∀ 𝑢 ∈ { 𝑡 } 〈 𝑦 , 𝑢 〉 ∈ 𝑀 ) |
30 |
|
vex |
⊢ 𝑡 ∈ V |
31 |
|
opeq2 |
⊢ ( 𝑢 = 𝑡 → 〈 𝑦 , 𝑢 〉 = 〈 𝑦 , 𝑡 〉 ) |
32 |
31
|
eleq1d |
⊢ ( 𝑢 = 𝑡 → ( 〈 𝑦 , 𝑢 〉 ∈ 𝑀 ↔ 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) ) |
33 |
30 32
|
ralsn |
⊢ ( ∀ 𝑢 ∈ { 𝑡 } 〈 𝑦 , 𝑢 〉 ∈ 𝑀 ↔ 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) |
34 |
33
|
ralbii |
⊢ ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∀ 𝑢 ∈ { 𝑡 } 〈 𝑦 , 𝑢 〉 ∈ 𝑀 ↔ ∀ 𝑦 ∈ ( 0 [,] 1 ) 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) |
35 |
27 29 34
|
3bitri |
⊢ ( ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ↔ ∀ 𝑦 ∈ ( 0 [,] 1 ) 〈 𝑦 , 𝑡 〉 ∈ 𝑀 ) |
36 |
26 35
|
syl6ibr |
⊢ ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) ) |