Step | Hyp | Ref
| Expression |
1 | | 5eluz3 12924 |
. . . 4
⊢ 5 ∈
(ℤ≥‘3) |
2 | | 3z 12647 |
. . . . . . 7
⊢ 3 ∈
ℤ |
3 | | 1lt3 12436 |
. . . . . . 7
⊢ 1 <
3 |
4 | | eluz2b1 12958 |
. . . . . . 7
⊢ (3 ∈
(ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 1 <
3)) |
5 | 2, 3, 4 | mpbir2an 711 |
. . . . . 6
⊢ 3 ∈
(ℤ≥‘2) |
6 | | fzo1lb 13749 |
. . . . . 6
⊢ (1 ∈
(1..^3) ↔ 3 ∈ (ℤ≥‘2)) |
7 | 5, 6 | mpbir 231 |
. . . . 5
⊢ 1 ∈
(1..^3) |
8 | | ceil5half3 47279 |
. . . . . . 7
⊢
(⌈‘(5 / 2)) = 3 |
9 | 8 | eqcomi 2743 |
. . . . . 6
⊢ 3 =
(⌈‘(5 / 2)) |
10 | 9 | oveq2i 7441 |
. . . . 5
⊢ (1..^3) =
(1..^(⌈‘(5 / 2))) |
11 | 7, 10 | eleqtri 2836 |
. . . 4
⊢ 1 ∈
(1..^(⌈‘(5 / 2))) |
12 | | gpgusgra 47946 |
. . . 4
⊢ ((5
∈ (ℤ≥‘3) ∧ 1 ∈ (1..^(⌈‘(5 /
2)))) → (5 gPetersenGr 1) ∈ USGraph) |
13 | 1, 11, 12 | mp2an 692 |
. . 3
⊢ (5
gPetersenGr 1) ∈ USGraph |
14 | | 2nn 12336 |
. . . . . 6
⊢ 2 ∈
ℕ |
15 | | 3nn 12342 |
. . . . . 6
⊢ 3 ∈
ℕ |
16 | | 2lt3 12435 |
. . . . . 6
⊢ 2 <
3 |
17 | | elfzo1 13748 |
. . . . . 6
⊢ (2 ∈
(1..^3) ↔ (2 ∈ ℕ ∧ 3 ∈ ℕ ∧ 2 <
3)) |
18 | 14, 15, 16, 17 | mpbir3an 1340 |
. . . . 5
⊢ 2 ∈
(1..^3) |
19 | 18, 10 | eleqtri 2836 |
. . . 4
⊢ 2 ∈
(1..^(⌈‘(5 / 2))) |
20 | | gpgusgra 47946 |
. . . 4
⊢ ((5
∈ (ℤ≥‘3) ∧ 2 ∈ (1..^(⌈‘(5 /
2)))) → (5 gPetersenGr 2) ∈ USGraph) |
21 | 1, 19, 20 | mp2an 692 |
. . 3
⊢ (5
gPetersenGr 2) ∈ USGraph |
22 | | 2eluzge1 12933 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘1) |
23 | | eluzfz1 13567 |
. . . . . 6
⊢ (2 ∈
(ℤ≥‘1) → 1 ∈ (1...2)) |
24 | 22, 23 | ax-mp 5 |
. . . . 5
⊢ 1 ∈
(1...2) |
25 | | gpg5order 47948 |
. . . . 5
⊢ (1 ∈
(1...2) → (♯‘(Vtx‘(5 gPetersenGr 1))) = ;10) |
26 | 24, 25 | ax-mp 5 |
. . . 4
⊢
(♯‘(Vtx‘(5 gPetersenGr 1))) = ;10 |
27 | | eluzfz2 13568 |
. . . . . 6
⊢ (2 ∈
(ℤ≥‘1) → 2 ∈ (1...2)) |
28 | 22, 27 | ax-mp 5 |
. . . . 5
⊢ 2 ∈
(1...2) |
29 | | gpg5order 47948 |
. . . . 5
⊢ (2 ∈
(1...2) → (♯‘(Vtx‘(5 gPetersenGr 2))) = ;10) |
30 | 28, 29 | ax-mp 5 |
. . . 4
⊢
(♯‘(Vtx‘(5 gPetersenGr 2))) = ;10 |
31 | | eqtr3 2760 |
. . . . 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 12748 |
. . . . . . 7
⊢ ;10 ∈
ℕ0 |
34 | | hashvnfin 14395 |
. . . . . . 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 14395 |
. . . . . . 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 14382 |
. . . . . 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 1338 |
. 2
⊢ ((5
gPetersenGr 1) ∈ USGraph ∧ (5 gPetersenGr 2) ∈ USGraph ∧
(Vtx‘(5 gPetersenGr 1)) ≈ (Vtx‘(5 gPetersenGr
2))) |
44 | | eqid 2734 |
. . . . 5
⊢ (5
gPetersenGr 1) = (5 gPetersenGr 1) |
45 | 44 | gpg5gricstgr3 47973 |
. . . 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 3060 |
. 2
⊢
∀𝑣 ∈
(Vtx‘(5 gPetersenGr 1))((5 gPetersenGr 1) ISubGr ((5 gPetersenGr 1)
ClNeighbVtx 𝑣))
≃𝑔𝑟 (StarGr‘3) |
48 | | eqid 2734 |
. . . . 5
⊢ (5
gPetersenGr 2) = (5 gPetersenGr 2) |
49 | 48 | gpg5gricstgr3 47973 |
. . . 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 3060 |
. 2
⊢
∀𝑤 ∈
(Vtx‘(5 gPetersenGr 2))((5 gPetersenGr 2) ISubGr ((5 gPetersenGr 2)
ClNeighbVtx 𝑤))
≃𝑔𝑟 (StarGr‘3) |
52 | | 3nn0 12541 |
. . 3
⊢ 3 ∈
ℕ0 |
53 | | eqid 2734 |
. . 3
⊢
(Vtx‘(5 gPetersenGr 1)) = (Vtx‘(5 gPetersenGr
1)) |
54 | | eqid 2734 |
. . 3
⊢
(Vtx‘(5 gPetersenGr 2)) = (Vtx‘(5 gPetersenGr
2)) |
55 | 52, 53, 54 | clnbgr3stgrgrlic 47914 |
. 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 1460 |
1
⊢ (5
gPetersenGr 1) ≃𝑙𝑔𝑟 (5 gPetersenGr
2) |