Step | Hyp | Ref
| Expression |
1 | | 1nn0 12539 |
. . 3
⊢ 1 ∈
ℕ0 |
2 | | stgrfv 47855 |
. . 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 13786 |
. . . 4
⊢ (0...1) =
{0, 1} |
5 | 4 | opeq2i 4881 |
. . 3
⊢
〈(Base‘ndx), (0...1)〉 = 〈(Base‘ndx), {0,
1}〉 |
6 | | elsni 4647 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {1} → 𝑥 = 1) |
7 | | preq2 4738 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → {0, 𝑥} = {0, 1}) |
8 | 7 | eqeq2d 2745 |
. . . . . . . . . . . . 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 12644 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
12 | | fzsn 13602 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → (1...1) = {1}) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (1...1) =
{1} |
14 | 10, 13 | eleq2s 2856 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...1) → (𝑒 = {0, 𝑥} → 𝑒 = {0, 1})) |
15 | 14 | rexlimiv 3145 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥} → 𝑒 = {0, 1}) |
16 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((𝑒 ∈ 𝒫 (0...1) ∧
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}) → 𝑒 = {0, 1}) |
17 | | c0ex 11252 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
18 | 17 | prid1 4766 |
. . . . . . . . . . . 12
⊢ 0 ∈
{0, 1} |
19 | 18, 4 | eleqtrri 2837 |
. . . . . . . . . . 11
⊢ 0 ∈
(0...1) |
20 | | 1ex 11254 |
. . . . . . . . . . . . 13
⊢ 1 ∈
V |
21 | 20 | prid2 4767 |
. . . . . . . . . . . 12
⊢ 1 ∈
{0, 1} |
22 | 21, 4 | eleqtrri 2837 |
. . . . . . . . . . 11
⊢ 1 ∈
(0...1) |
23 | | prelpwi 5457 |
. . . . . . . . . . 11
⊢ ((0
∈ (0...1) ∧ 1 ∈ (0...1)) → {0, 1} ∈ 𝒫
(0...1)) |
24 | 19, 22, 23 | mp2an 692 |
. . . . . . . . . 10
⊢ {0, 1}
∈ 𝒫 (0...1) |
25 | | eqid 2734 |
. . . . . . . . . . 11
⊢ {0, 1} =
{0, 1} |
26 | 13 | rexeqi 3322 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
(1...1){0, 1} = {0, 𝑥}
↔ ∃𝑥 ∈ {1}
{0, 1} = {0, 𝑥}) |
27 | 7 | eqeq2d 2745 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → ({0, 1} = {0, 𝑥} ↔ {0, 1} = {0,
1})) |
28 | 20, 27 | rexsn 4686 |
. . . . . . . . . . . 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 2826 |
. . . . . . . . . 10
⊢ (𝑒 = {0, 1} → (𝑒 ∈ 𝒫 (0...1) ↔
{0, 1} ∈ 𝒫 (0...1))) |
33 | | eqeq1 2738 |
. . . . . . . . . . 11
⊢ (𝑒 = {0, 1} → (𝑒 = {0, 𝑥} ↔ {0, 1} = {0, 𝑥})) |
34 | 33 | rexbidv 3176 |
. . . . . . . . . 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 2806 |
. . . . . 6
⊢ {𝑒 ∣ (𝑒 ∈ 𝒫 (0...1) ∧ ∃𝑥 ∈ (1...1)𝑒 = {0, 𝑥})} = {𝑒 ∣ 𝑒 = {0, 1}} |
39 | | df-rab 3433 |
. . . . . 6
⊢ {𝑒 ∈ 𝒫 (0...1)
∣ ∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}} = {𝑒 ∣ (𝑒 ∈ 𝒫 (0...1) ∧ ∃𝑥 ∈ (1...1)𝑒 = {0, 𝑥})} |
40 | | df-sn 4631 |
. . . . . 6
⊢ {{0, 1}}
= {𝑒 ∣ 𝑒 = {0, 1}} |
41 | 38, 39, 40 | 3eqtr4i 2772 |
. . . . 5
⊢ {𝑒 ∈ 𝒫 (0...1)
∣ ∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}} = {{0, 1}} |
42 | 41 | reseq2i 5996 |
. . . 4
⊢ ( I
↾ {𝑒 ∈ 𝒫
(0...1) ∣ ∃𝑥
∈ (1...1)𝑒 = {0, 𝑥}}) = ( I ↾ {{0,
1}}) |
43 | 42 | opeq2i 4881 |
. . 3
⊢
〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...1) ∣
∃𝑥 ∈
(1...1)𝑒 = {0, 𝑥}})〉 =
〈(.ef‘ndx), ( I ↾ {{0, 1}})〉 |
44 | 5, 43 | preq12i 4742 |
. 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 2762 |
1
⊢
(StarGr‘1) = {〈(Base‘ndx), {0, 1}〉,
〈(.ef‘ndx), ( I ↾ {{0, 1}})〉} |