| Step | Hyp | Ref
| Expression |
| 1 | | 1nn0 12542 |
. . 3
⊢ 1 ∈
ℕ0 |
| 2 | | stgrfv 47920 |
. . 3
⊢ (1 ∈
ℕ0 → (StarGr‘1) = {〈(Base‘ndx),
(0...1)〉, 〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...1) ∣
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}})〉}) |
| 3 | 1, 2 | ax-mp 5 |
. 2
⊢
(StarGr‘1) = {〈(Base‘ndx), (0...1)〉,
〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...1) ∣
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}})〉} |
| 4 | | fz01pr 13790 |
. . . 4
⊢ (0...1) =
{0, 1} |
| 5 | 4 | opeq2i 4877 |
. . 3
⊢
〈(Base‘ndx), (0...1)〉 = 〈(Base‘ndx), {0,
1}〉 |
| 6 | | elsni 4643 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {1} → 𝑥 = 1) |
| 7 | | preq2 4734 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → {0, 𝑥} = {0, 1}) |
| 8 | 7 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (𝑒 = {0, 𝑥} ↔ 𝑒 = {0, 1})) |
| 9 | 8 | biimpd 229 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑒 = {0, 𝑥} → 𝑒 = {0, 1})) |
| 10 | 6, 9 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {1} → (𝑒 = {0, 𝑥} → 𝑒 = {0, 1})) |
| 11 | | 1z 12647 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
| 12 | | fzsn 13606 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → (1...1) = {1}) |
| 13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (1...1) =
{1} |
| 14 | 10, 13 | eleq2s 2859 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...1) → (𝑒 = {0, 𝑥} → 𝑒 = {0, 1})) |
| 15 | 14 | rexlimiv 3148 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥} → 𝑒 = {0, 1}) |
| 16 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((𝑒 ∈ 𝒫 (0...1) ∧
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}) → 𝑒 = {0, 1}) |
| 17 | | c0ex 11255 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
| 18 | 17 | prid1 4762 |
. . . . . . . . . . . 12
⊢ 0 ∈
{0, 1} |
| 19 | 18, 4 | eleqtrri 2840 |
. . . . . . . . . . 11
⊢ 0 ∈
(0...1) |
| 20 | | 1ex 11257 |
. . . . . . . . . . . . 13
⊢ 1 ∈
V |
| 21 | 20 | prid2 4763 |
. . . . . . . . . . . 12
⊢ 1 ∈
{0, 1} |
| 22 | 21, 4 | eleqtrri 2840 |
. . . . . . . . . . 11
⊢ 1 ∈
(0...1) |
| 23 | | prelpwi 5452 |
. . . . . . . . . . 11
⊢ ((0
∈ (0...1) ∧ 1 ∈ (0...1)) → {0, 1} ∈ 𝒫
(0...1)) |
| 24 | 19, 22, 23 | mp2an 692 |
. . . . . . . . . 10
⊢ {0, 1}
∈ 𝒫 (0...1) |
| 25 | | eqid 2737 |
. . . . . . . . . . 11
⊢ {0, 1} =
{0, 1} |
| 26 | 13 | rexeqi 3325 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
(1...1){0, 1} = {0, 𝑥}
↔ ∃𝑥 ∈ {1}
{0, 1} = {0, 𝑥}) |
| 27 | 7 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → ({0, 1} = {0, 𝑥} ↔ {0, 1} = {0,
1})) |
| 28 | 20, 27 | rexsn 4682 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈ {1}
{0, 1} = {0, 𝑥} ↔ {0,
1} = {0, 1}) |
| 29 | 26, 28 | bitri 275 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
(1...1){0, 1} = {0, 𝑥}
↔ {0, 1} = {0, 1}) |
| 30 | 25, 29 | mpbir 231 |
. . . . . . . . . 10
⊢
∃𝑥 ∈
(1...1){0, 1} = {0, 𝑥} |
| 31 | 24, 30 | pm3.2i 470 |
. . . . . . . . 9
⊢ ({0, 1}
∈ 𝒫 (0...1) ∧ ∃𝑥 ∈ (1...1){0, 1} = {0, 𝑥}) |
| 32 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑒 = {0, 1} → (𝑒 ∈ 𝒫 (0...1) ↔
{0, 1} ∈ 𝒫 (0...1))) |
| 33 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑒 = {0, 1} → (𝑒 = {0, 𝑥} ↔ {0, 1} = {0, 𝑥})) |
| 34 | 33 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑒 = {0, 1} → (∃𝑥 ∈ (1...1)𝑒 = {0, 𝑥} ↔ ∃𝑥 ∈ (1...1){0, 1} = {0, 𝑥})) |
| 35 | 32, 34 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑒 = {0, 1} → ((𝑒 ∈ 𝒫 (0...1) ∧
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}) ↔ ({0, 1} ∈
𝒫 (0...1) ∧ ∃𝑥 ∈ (1...1){0, 1} = {0, 𝑥}))) |
| 36 | 31, 35 | mpbiri 258 |
. . . . . . . 8
⊢ (𝑒 = {0, 1} → (𝑒 ∈ 𝒫 (0...1) ∧
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥})) |
| 37 | 16, 36 | impbii 209 |
. . . . . . 7
⊢ ((𝑒 ∈ 𝒫 (0...1) ∧
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}) ↔ 𝑒 = {0, 1}) |
| 38 | 37 | abbii 2809 |
. . . . . 6
⊢ {𝑒 ∣ (𝑒 ∈ 𝒫 (0...1) ∧ ∃𝑥 ∈ (1...1)𝑒 = {0, 𝑥})} = {𝑒 ∣ 𝑒 = {0, 1}} |
| 39 | | df-rab 3437 |
. . . . . 6
⊢ {𝑒 ∈ 𝒫 (0...1)
∣ ∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}} = {𝑒 ∣ (𝑒 ∈ 𝒫 (0...1) ∧ ∃𝑥 ∈ (1...1)𝑒 = {0, 𝑥})} |
| 40 | | df-sn 4627 |
. . . . . 6
⊢ {{0, 1}}
= {𝑒 ∣ 𝑒 = {0, 1}} |
| 41 | 38, 39, 40 | 3eqtr4i 2775 |
. . . . 5
⊢ {𝑒 ∈ 𝒫 (0...1)
∣ ∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}} = {{0, 1}} |
| 42 | 41 | reseq2i 5994 |
. . . 4
⊢ ( I
↾ {𝑒 ∈ 𝒫
(0...1) ∣ ∃𝑥
∈ (1...1)𝑒 = {0, 𝑥}}) = ( I ↾ {{0,
1}}) |
| 43 | 42 | opeq2i 4877 |
. . 3
⊢
〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...1) ∣
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}})〉 =
〈(.ef‘ndx), ( I ↾ {{0, 1}})〉 |
| 44 | 5, 43 | preq12i 4738 |
. 2
⊢
{〈(Base‘ndx), (0...1)〉, 〈(.ef‘ndx), ( I
↾ {𝑒 ∈ 𝒫
(0...1) ∣ ∃𝑥
∈ (1...1)𝑒 = {0, 𝑥}})〉} =
{〈(Base‘ndx), {0, 1}〉, 〈(.ef‘ndx), ( I ↾ {{0,
1}})〉} |
| 45 | 3, 44 | eqtri 2765 |
1
⊢
(StarGr‘1) = {〈(Base‘ndx), {0, 1}〉,
〈(.ef‘ndx), ( I ↾ {{0, 1}})〉} |