| Step |
Hyp |
Ref |
Expression |
| 1 |
|
5eluz3 |
⊢ 5 ∈ ( ℤ≥ ‘ 3 ) |
| 2 |
|
3z |
⊢ 3 ∈ ℤ |
| 3 |
|
1lt3 |
⊢ 1 < 3 |
| 4 |
|
eluz2b1 |
⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 3 ∈ ℤ ∧ 1 < 3 ) ) |
| 5 |
2 3 4
|
mpbir2an |
⊢ 3 ∈ ( ℤ≥ ‘ 2 ) |
| 6 |
|
fzo1lb |
⊢ ( 1 ∈ ( 1 ..^ 3 ) ↔ 3 ∈ ( ℤ≥ ‘ 2 ) ) |
| 7 |
5 6
|
mpbir |
⊢ 1 ∈ ( 1 ..^ 3 ) |
| 8 |
|
ceil5half3 |
⊢ ( ⌈ ‘ ( 5 / 2 ) ) = 3 |
| 9 |
8
|
eqcomi |
⊢ 3 = ( ⌈ ‘ ( 5 / 2 ) ) |
| 10 |
9
|
oveq2i |
⊢ ( 1 ..^ 3 ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) |
| 11 |
7 10
|
eleqtri |
⊢ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) |
| 12 |
|
gpgusgra |
⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 1 ) ∈ USGraph ) |
| 13 |
1 11 12
|
mp2an |
⊢ ( 5 gPetersenGr 1 ) ∈ USGraph |
| 14 |
|
2nn |
⊢ 2 ∈ ℕ |
| 15 |
|
3nn |
⊢ 3 ∈ ℕ |
| 16 |
|
2lt3 |
⊢ 2 < 3 |
| 17 |
|
elfzo1 |
⊢ ( 2 ∈ ( 1 ..^ 3 ) ↔ ( 2 ∈ ℕ ∧ 3 ∈ ℕ ∧ 2 < 3 ) ) |
| 18 |
14 15 16 17
|
mpbir3an |
⊢ 2 ∈ ( 1 ..^ 3 ) |
| 19 |
18 10
|
eleqtri |
⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) |
| 20 |
|
gpgusgra |
⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 2 ) ∈ USGraph ) |
| 21 |
1 19 20
|
mp2an |
⊢ ( 5 gPetersenGr 2 ) ∈ USGraph |
| 22 |
|
2eluzge1 |
⊢ 2 ∈ ( ℤ≥ ‘ 1 ) |
| 23 |
|
eluzfz1 |
⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 2 ) ) |
| 24 |
22 23
|
ax-mp |
⊢ 1 ∈ ( 1 ... 2 ) |
| 25 |
|
gpg5order |
⊢ ( 1 ∈ ( 1 ... 2 ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ; 1 0 ) |
| 26 |
24 25
|
ax-mp |
⊢ ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ; 1 0 |
| 27 |
|
eluzfz2 |
⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 2 ∈ ( 1 ... 2 ) ) |
| 28 |
22 27
|
ax-mp |
⊢ 2 ∈ ( 1 ... 2 ) |
| 29 |
|
gpg5order |
⊢ ( 2 ∈ ( 1 ... 2 ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) |
| 30 |
28 29
|
ax-mp |
⊢ ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = ; 1 0 |
| 31 |
|
eqtr3 |
⊢ ( ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ; 1 0 ∧ ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) ) |
| 32 |
|
fvex |
⊢ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ V |
| 33 |
|
10nn0 |
⊢ ; 1 0 ∈ ℕ0 |
| 34 |
|
hashvnfin |
⊢ ( ( ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ V ∧ ; 1 0 ∈ ℕ0 ) → ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ; 1 0 → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ Fin ) ) |
| 35 |
32 33 34
|
mp2an |
⊢ ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ; 1 0 → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ Fin ) |
| 36 |
|
fvex |
⊢ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ V |
| 37 |
|
hashvnfin |
⊢ ( ( ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ V ∧ ; 1 0 ∈ ℕ0 ) → ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = ; 1 0 → ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ Fin ) ) |
| 38 |
36 33 37
|
mp2an |
⊢ ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = ; 1 0 → ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ Fin ) |
| 39 |
|
hashen |
⊢ ( ( ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ Fin ∧ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ Fin ) → ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) ↔ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) ) |
| 40 |
35 38 39
|
syl2an |
⊢ ( ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ; 1 0 ∧ ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) → ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) ↔ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) ) |
| 41 |
31 40
|
mpbid |
⊢ ( ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = ; 1 0 ∧ ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) |
| 42 |
26 30 41
|
mp2an |
⊢ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) |
| 43 |
13 21 42
|
3pm3.2i |
⊢ ( ( 5 gPetersenGr 1 ) ∈ USGraph ∧ ( 5 gPetersenGr 2 ) ∈ USGraph ∧ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) |
| 44 |
|
eqid |
⊢ ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) |
| 45 |
44
|
gpg5gricstgr3 |
⊢ ( ( 1 ∈ ( 1 ... 2 ) ∧ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) → ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ) |
| 46 |
24 45
|
mpan |
⊢ ( 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) → ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ) |
| 47 |
46
|
rgen |
⊢ ∀ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) |
| 48 |
|
eqid |
⊢ ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) |
| 49 |
48
|
gpg5gricstgr3 |
⊢ ( ( 2 ∈ ( 1 ... 2 ) ∧ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) → ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ) |
| 50 |
28 49
|
mpan |
⊢ ( 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) → ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ) |
| 51 |
50
|
rgen |
⊢ ∀ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) |
| 52 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
| 53 |
|
eqid |
⊢ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) = ( Vtx ‘ ( 5 gPetersenGr 1 ) ) |
| 54 |
|
eqid |
⊢ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) = ( Vtx ‘ ( 5 gPetersenGr 2 ) ) |
| 55 |
52 53 54
|
clnbgr3stgrgrlic |
⊢ ( ( ( ( 5 gPetersenGr 1 ) ∈ USGraph ∧ ( 5 gPetersenGr 2 ) ∈ USGraph ∧ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ) → ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 ) ) |
| 56 |
43 47 51 55
|
mp3an |
⊢ ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 ) |