Step |
Hyp |
Ref |
Expression |
1 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
2 |
|
stgrfv |
⊢ ( 0 ∈ ℕ0 → ( StarGr ‘ 0 ) = { 〈 ( Base ‘ ndx ) , ( 0 ... 0 ) 〉 , 〈 ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) 〉 } ) |
3 |
1 2
|
ax-mp |
⊢ ( StarGr ‘ 0 ) = { 〈 ( Base ‘ ndx ) , ( 0 ... 0 ) 〉 , 〈 ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) 〉 } |
4 |
|
fz0sn |
⊢ ( 0 ... 0 ) = { 0 } |
5 |
4
|
opeq2i |
⊢ 〈 ( Base ‘ ndx ) , ( 0 ... 0 ) 〉 = 〈 ( Base ‘ ndx ) , { 0 } 〉 |
6 |
|
rabeq0 |
⊢ ( { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } = ∅ ↔ ∀ 𝑒 ∈ 𝒫 ( 0 ... 0 ) ¬ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } ) |
7 |
|
noel |
⊢ ¬ 𝑥 ∈ ∅ |
8 |
7
|
pm2.21i |
⊢ ( 𝑥 ∈ ∅ → ¬ 𝑒 = { 0 , 𝑥 } ) |
9 |
|
fz10 |
⊢ ( 1 ... 0 ) = ∅ |
10 |
8 9
|
eleq2s |
⊢ ( 𝑥 ∈ ( 1 ... 0 ) → ¬ 𝑒 = { 0 , 𝑥 } ) |
11 |
10
|
a1i |
⊢ ( 𝑒 ∈ 𝒫 ( 0 ... 0 ) → ( 𝑥 ∈ ( 1 ... 0 ) → ¬ 𝑒 = { 0 , 𝑥 } ) ) |
12 |
11
|
ralrimiv |
⊢ ( 𝑒 ∈ 𝒫 ( 0 ... 0 ) → ∀ 𝑥 ∈ ( 1 ... 0 ) ¬ 𝑒 = { 0 , 𝑥 } ) |
13 |
|
ralnex |
⊢ ( ∀ 𝑥 ∈ ( 1 ... 0 ) ¬ 𝑒 = { 0 , 𝑥 } ↔ ¬ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } ) |
14 |
12 13
|
sylib |
⊢ ( 𝑒 ∈ 𝒫 ( 0 ... 0 ) → ¬ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } ) |
15 |
6 14
|
mprgbir |
⊢ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } = ∅ |
16 |
15
|
reseq2i |
⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) = ( I ↾ ∅ ) |
17 |
|
res0 |
⊢ ( I ↾ ∅ ) = ∅ |
18 |
16 17
|
eqtri |
⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) = ∅ |
19 |
18
|
opeq2i |
⊢ 〈 ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) 〉 = 〈 ( .ef ‘ ndx ) , ∅ 〉 |
20 |
5 19
|
preq12i |
⊢ { 〈 ( Base ‘ ndx ) , ( 0 ... 0 ) 〉 , 〈 ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) 〉 } = { 〈 ( Base ‘ ndx ) , { 0 } 〉 , 〈 ( .ef ‘ ndx ) , ∅ 〉 } |
21 |
3 20
|
eqtri |
⊢ ( StarGr ‘ 0 ) = { 〈 ( Base ‘ ndx ) , { 0 } 〉 , 〈 ( .ef ‘ ndx ) , ∅ 〉 } |