Step |
Hyp |
Ref |
Expression |
1 |
|
stgrvtx0.g |
⊢ 𝐺 = ( StarGr ‘ 𝑁 ) |
2 |
|
stgrvtx0.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
3 |
1 2
|
stgrvtx0 |
⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ 𝑉 ) |
4 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
5 |
2 4
|
dfnbgr2 |
⊢ ( 0 ∈ 𝑉 → ( 𝐺 NeighbVtx 0 ) = { 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 0 ∈ 𝑒 ∧ 𝑥 ∈ 𝑒 ) } ) |
6 |
3 5
|
syl |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝐺 NeighbVtx 0 ) = { 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 0 ∈ 𝑒 ∧ 𝑥 ∈ 𝑒 ) } ) |
7 |
|
eleq2 |
⊢ ( 𝑒 = { 0 , 𝑥 } → ( 0 ∈ 𝑒 ↔ 0 ∈ { 0 , 𝑥 } ) ) |
8 |
|
eleq2 |
⊢ ( 𝑒 = { 0 , 𝑥 } → ( 𝑥 ∈ 𝑒 ↔ 𝑥 ∈ { 0 , 𝑥 } ) ) |
9 |
7 8
|
anbi12d |
⊢ ( 𝑒 = { 0 , 𝑥 } → ( ( 0 ∈ 𝑒 ∧ 𝑥 ∈ 𝑒 ) ↔ ( 0 ∈ { 0 , 𝑥 } ∧ 𝑥 ∈ { 0 , 𝑥 } ) ) ) |
10 |
|
0elfz |
⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) ) |
11 |
10
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 0 ∈ ( 0 ... 𝑁 ) ) |
12 |
|
fz1ssfz0 |
⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) |
13 |
1
|
fveq2i |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) |
14 |
2 13
|
eqtri |
⊢ 𝑉 = ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) |
15 |
|
stgrvtx |
⊢ ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 ) ) |
16 |
14 15
|
eqtrid |
⊢ ( 𝑁 ∈ ℕ0 → 𝑉 = ( 0 ... 𝑁 ) ) |
17 |
16
|
difeq1d |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑉 ∖ { 0 } ) = ( ( 0 ... 𝑁 ) ∖ { 0 } ) ) |
18 |
|
fz0dif1 |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 ... 𝑁 ) ∖ { 0 } ) = ( 1 ... 𝑁 ) ) |
19 |
18
|
eqimssd |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 ... 𝑁 ) ∖ { 0 } ) ⊆ ( 1 ... 𝑁 ) ) |
20 |
17 19
|
eqsstrd |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑉 ∖ { 0 } ) ⊆ ( 1 ... 𝑁 ) ) |
21 |
20
|
sselda |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑥 ∈ ( 1 ... 𝑁 ) ) |
22 |
12 21
|
sselid |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑥 ∈ ( 0 ... 𝑁 ) ) |
23 |
11 22
|
prssd |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → { 0 , 𝑥 } ⊆ ( 0 ... 𝑁 ) ) |
24 |
|
preq2 |
⊢ ( 𝑛 = 𝑥 → { 0 , 𝑛 } = { 0 , 𝑥 } ) |
25 |
24
|
eqeq2d |
⊢ ( 𝑛 = 𝑥 → ( { 0 , 𝑥 } = { 0 , 𝑛 } ↔ { 0 , 𝑥 } = { 0 , 𝑥 } ) ) |
26 |
|
eqidd |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → { 0 , 𝑥 } = { 0 , 𝑥 } ) |
27 |
25 21 26
|
rspcedvdw |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ∃ 𝑛 ∈ ( 1 ... 𝑁 ) { 0 , 𝑥 } = { 0 , 𝑛 } ) |
28 |
1
|
fveq2i |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ ( StarGr ‘ 𝑁 ) ) |
29 |
28
|
eleq2i |
⊢ ( { 0 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ↔ { 0 , 𝑥 } ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) |
30 |
|
stgredgel |
⊢ ( 𝑁 ∈ ℕ0 → ( { 0 , 𝑥 } ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( { 0 , 𝑥 } ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑛 ∈ ( 1 ... 𝑁 ) { 0 , 𝑥 } = { 0 , 𝑛 } ) ) ) |
31 |
30
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( { 0 , 𝑥 } ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( { 0 , 𝑥 } ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑛 ∈ ( 1 ... 𝑁 ) { 0 , 𝑥 } = { 0 , 𝑛 } ) ) ) |
32 |
29 31
|
bitrid |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( { 0 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ↔ ( { 0 , 𝑥 } ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑛 ∈ ( 1 ... 𝑁 ) { 0 , 𝑥 } = { 0 , 𝑛 } ) ) ) |
33 |
23 27 32
|
mpbir2and |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → { 0 , 𝑥 } ∈ ( Edg ‘ 𝐺 ) ) |
34 |
|
prid2g |
⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) → 𝑥 ∈ { 0 , 𝑥 } ) |
35 |
34
|
adantl |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑥 ∈ { 0 , 𝑥 } ) |
36 |
|
c0ex |
⊢ 0 ∈ V |
37 |
36
|
prid1 |
⊢ 0 ∈ { 0 , 𝑥 } |
38 |
35 37
|
jctil |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 0 ∈ { 0 , 𝑥 } ∧ 𝑥 ∈ { 0 , 𝑥 } ) ) |
39 |
9 33 38
|
rspcedvdw |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 0 ∈ 𝑒 ∧ 𝑥 ∈ 𝑒 ) ) |
40 |
39
|
rabeqcda |
⊢ ( 𝑁 ∈ ℕ0 → { 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 0 ∈ 𝑒 ∧ 𝑥 ∈ 𝑒 ) } = ( 𝑉 ∖ { 0 } ) ) |
41 |
6 40
|
eqtrd |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝐺 NeighbVtx 0 ) = ( 𝑉 ∖ { 0 } ) ) |