| Step | Hyp | Ref
| Expression |
| 1 | | 5eluz3 12927 |
. . . 4
⊢ 5 ∈
(ℤ≥‘3) |
| 2 | | 3z 12650 |
. . . . . . 7
⊢ 3 ∈
ℤ |
| 3 | | 1lt3 12439 |
. . . . . . 7
⊢ 1 <
3 |
| 4 | | eluz2b1 12961 |
. . . . . . 7
⊢ (3 ∈
(ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 1 <
3)) |
| 5 | 2, 3, 4 | mpbir2an 711 |
. . . . . 6
⊢ 3 ∈
(ℤ≥‘2) |
| 6 | | fzo1lb 13753 |
. . . . . 6
⊢ (1 ∈
(1..^3) ↔ 3 ∈ (ℤ≥‘2)) |
| 7 | 5, 6 | mpbir 231 |
. . . . 5
⊢ 1 ∈
(1..^3) |
| 8 | | ceil5half3 47342 |
. . . . . . 7
⊢
(⌈‘(5 / 2)) = 3 |
| 9 | 8 | eqcomi 2746 |
. . . . . 6
⊢ 3 =
(⌈‘(5 / 2)) |
| 10 | 9 | oveq2i 7442 |
. . . . 5
⊢ (1..^3) =
(1..^(⌈‘(5 / 2))) |
| 11 | 7, 10 | eleqtri 2839 |
. . . 4
⊢ 1 ∈
(1..^(⌈‘(5 / 2))) |
| 12 | | gpgusgra 48012 |
. . . 4
⊢ ((5
∈ (ℤ≥‘3) ∧ 1 ∈ (1..^(⌈‘(5 /
2)))) → (5 gPetersenGr 1) ∈ USGraph) |
| 13 | 1, 11, 12 | mp2an 692 |
. . 3
⊢ (5
gPetersenGr 1) ∈ USGraph |
| 14 | | 2nn 12339 |
. . . . . 6
⊢ 2 ∈
ℕ |
| 15 | | 3nn 12345 |
. . . . . 6
⊢ 3 ∈
ℕ |
| 16 | | 2lt3 12438 |
. . . . . 6
⊢ 2 <
3 |
| 17 | | elfzo1 13752 |
. . . . . 6
⊢ (2 ∈
(1..^3) ↔ (2 ∈ ℕ ∧ 3 ∈ ℕ ∧ 2 <
3)) |
| 18 | 14, 15, 16, 17 | mpbir3an 1342 |
. . . . 5
⊢ 2 ∈
(1..^3) |
| 19 | 18, 10 | eleqtri 2839 |
. . . 4
⊢ 2 ∈
(1..^(⌈‘(5 / 2))) |
| 20 | | gpgusgra 48012 |
. . . 4
⊢ ((5
∈ (ℤ≥‘3) ∧ 2 ∈ (1..^(⌈‘(5 /
2)))) → (5 gPetersenGr 2) ∈ USGraph) |
| 21 | 1, 19, 20 | mp2an 692 |
. . 3
⊢ (5
gPetersenGr 2) ∈ USGraph |
| 22 | | 2eluzge1 12936 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘1) |
| 23 | | eluzfz1 13571 |
. . . . . 6
⊢ (2 ∈
(ℤ≥‘1) → 1 ∈ (1...2)) |
| 24 | 22, 23 | ax-mp 5 |
. . . . 5
⊢ 1 ∈
(1...2) |
| 25 | | gpg5order 48014 |
. . . . 5
⊢ (1 ∈
(1...2) → (♯‘(Vtx‘(5 gPetersenGr 1))) = ;10) |
| 26 | 24, 25 | ax-mp 5 |
. . . 4
⊢
(♯‘(Vtx‘(5 gPetersenGr 1))) = ;10 |
| 27 | | eluzfz2 13572 |
. . . . . 6
⊢ (2 ∈
(ℤ≥‘1) → 2 ∈ (1...2)) |
| 28 | 22, 27 | ax-mp 5 |
. . . . 5
⊢ 2 ∈
(1...2) |
| 29 | | gpg5order 48014 |
. . . . 5
⊢ (2 ∈
(1...2) → (♯‘(Vtx‘(5 gPetersenGr 2))) = ;10) |
| 30 | 28, 29 | ax-mp 5 |
. . . 4
⊢
(♯‘(Vtx‘(5 gPetersenGr 2))) = ;10 |
| 31 | | eqtr3 2763 |
. . . . 5
⊢
(((♯‘(Vtx‘(5 gPetersenGr 1))) = ;10 ∧ (♯‘(Vtx‘(5 gPetersenGr
2))) = ;10) →
(♯‘(Vtx‘(5 gPetersenGr 1))) = (♯‘(Vtx‘(5
gPetersenGr 2)))) |
| 32 | | fvex 6919 |
. . . . . . 7
⊢
(Vtx‘(5 gPetersenGr 1)) ∈ V |
| 33 | | 10nn0 12751 |
. . . . . . 7
⊢ ;10 ∈
ℕ0 |
| 34 | | hashvnfin 14399 |
. . . . . . 7
⊢
(((Vtx‘(5 gPetersenGr 1)) ∈ V ∧ ;10 ∈ ℕ0) →
((♯‘(Vtx‘(5 gPetersenGr 1))) = ;10 → (Vtx‘(5 gPetersenGr 1)) ∈
Fin)) |
| 35 | 32, 33, 34 | mp2an 692 |
. . . . . 6
⊢
((♯‘(Vtx‘(5 gPetersenGr 1))) = ;10 → (Vtx‘(5 gPetersenGr 1)) ∈
Fin) |
| 36 | | fvex 6919 |
. . . . . . 7
⊢
(Vtx‘(5 gPetersenGr 2)) ∈ V |
| 37 | | hashvnfin 14399 |
. . . . . . 7
⊢
(((Vtx‘(5 gPetersenGr 2)) ∈ V ∧ ;10 ∈ ℕ0) →
((♯‘(Vtx‘(5 gPetersenGr 2))) = ;10 → (Vtx‘(5 gPetersenGr 2)) ∈
Fin)) |
| 38 | 36, 33, 37 | mp2an 692 |
. . . . . 6
⊢
((♯‘(Vtx‘(5 gPetersenGr 2))) = ;10 → (Vtx‘(5 gPetersenGr 2)) ∈
Fin) |
| 39 | | hashen 14386 |
. . . . . 6
⊢
(((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 596 |
. . . . 5
⊢
(((♯‘(Vtx‘(5 gPetersenGr 1))) = ;10 ∧ (♯‘(Vtx‘(5 gPetersenGr
2))) = ;10) →
((♯‘(Vtx‘(5 gPetersenGr 1))) = (♯‘(Vtx‘(5
gPetersenGr 2))) ↔ (Vtx‘(5 gPetersenGr 1)) ≈ (Vtx‘(5
gPetersenGr 2)))) |
| 41 | 31, 40 | mpbid 232 |
. . . 4
⊢
(((♯‘(Vtx‘(5 gPetersenGr 1))) = ;10 ∧ (♯‘(Vtx‘(5 gPetersenGr
2))) = ;10) → (Vtx‘(5
gPetersenGr 1)) ≈ (Vtx‘(5 gPetersenGr 2))) |
| 42 | 26, 30, 41 | mp2an 692 |
. . 3
⊢
(Vtx‘(5 gPetersenGr 1)) ≈ (Vtx‘(5 gPetersenGr
2)) |
| 43 | 13, 21, 42 | 3pm3.2i 1340 |
. 2
⊢ ((5
gPetersenGr 1) ∈ USGraph ∧ (5 gPetersenGr 2) ∈ USGraph ∧
(Vtx‘(5 gPetersenGr 1)) ≈ (Vtx‘(5 gPetersenGr
2))) |
| 44 | | eqid 2737 |
. . . . 5
⊢ (5
gPetersenGr 1) = (5 gPetersenGr 1) |
| 45 | 44 | gpg5gricstgr3 48046 |
. . . 4
⊢ ((1
∈ (1...2) ∧ 𝑣
∈ (Vtx‘(5 gPetersenGr 1))) → ((5 gPetersenGr 1) ISubGr ((5
gPetersenGr 1) ClNeighbVtx 𝑣)) ≃𝑔𝑟
(StarGr‘3)) |
| 46 | 24, 45 | mpan 690 |
. . 3
⊢ (𝑣 ∈ (Vtx‘(5
gPetersenGr 1)) → ((5 gPetersenGr 1) ISubGr ((5 gPetersenGr 1) ClNeighbVtx
𝑣))
≃𝑔𝑟 (StarGr‘3)) |
| 47 | 46 | rgen 3063 |
. 2
⊢
∀𝑣 ∈
(Vtx‘(5 gPetersenGr 1))((5 gPetersenGr 1) ISubGr ((5 gPetersenGr 1)
ClNeighbVtx 𝑣))
≃𝑔𝑟 (StarGr‘3) |
| 48 | | eqid 2737 |
. . . . 5
⊢ (5
gPetersenGr 2) = (5 gPetersenGr 2) |
| 49 | 48 | gpg5gricstgr3 48046 |
. . . 4
⊢ ((2
∈ (1...2) ∧ 𝑤
∈ (Vtx‘(5 gPetersenGr 2))) → ((5 gPetersenGr 2) ISubGr ((5
gPetersenGr 2) ClNeighbVtx 𝑤)) ≃𝑔𝑟
(StarGr‘3)) |
| 50 | 28, 49 | mpan 690 |
. . 3
⊢ (𝑤 ∈ (Vtx‘(5
gPetersenGr 2)) → ((5 gPetersenGr 2) ISubGr ((5 gPetersenGr 2) ClNeighbVtx
𝑤))
≃𝑔𝑟 (StarGr‘3)) |
| 51 | 50 | rgen 3063 |
. 2
⊢
∀𝑤 ∈
(Vtx‘(5 gPetersenGr 2))((5 gPetersenGr 2) ISubGr ((5 gPetersenGr 2)
ClNeighbVtx 𝑤))
≃𝑔𝑟 (StarGr‘3) |
| 52 | | 3nn0 12544 |
. . 3
⊢ 3 ∈
ℕ0 |
| 53 | | eqid 2737 |
. . 3
⊢
(Vtx‘(5 gPetersenGr 1)) = (Vtx‘(5 gPetersenGr
1)) |
| 54 | | eqid 2737 |
. . 3
⊢
(Vtx‘(5 gPetersenGr 2)) = (Vtx‘(5 gPetersenGr
2)) |
| 55 | 52, 53, 54 | clnbgr3stgrgrlic 47979 |
. 2
⊢ ((((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 1463 |
1
⊢ (5
gPetersenGr 1) ≃𝑙𝑔𝑟 (5 gPetersenGr
2) |