Metamath Proof Explorer

Theorem gpg5edgnedg

Description: Two consecutive (according to the numbering) inside vertices of the Petersen graph G(5,2) are not connected by an edge, but are connected by an edge in a 5-prism G(5,1). (Contributed by AV, 29-Dec-2025)

Ref Expression
Assertion gpg5edgnedg ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) )

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 eleq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ∈ ( 0 ..^ 5 ) ↔ 0 ∈ ( 0 ..^ 5 ) ) )
3 opeq2 ⊢ ( 𝑥 = 0 → ⟨ 0 , 𝑥 ⟩ = ⟨ 0 , 0 ⟩ )
4 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 + 1 ) = ( 0 + 1 ) )
5 4 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 + 1 ) mod 5 ) = ( ( 0 + 1 ) mod 5 ) )
6 5 opeq2d ⊢ ( 𝑥 = 0 → ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 0 + 1 ) mod 5 ) ⟩ )
7 3 6 preq12d ⊢ ( 𝑥 = 0 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 + 1 ) mod 5 ) ⟩ } )
8 7 eqeq2d ⊢ ( 𝑥 = 0 → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ↔ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 + 1 ) mod 5 ) ⟩ } ) )
9 opeq2 ⊢ ( 𝑥 = 0 → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 0 ⟩ )
10 3 9 preq12d ⊢ ( 𝑥 = 0 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } )
11 10 eqeq2d ⊢ ( 𝑥 = 0 → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ) )
12 5 opeq2d ⊢ ( 𝑥 = 0 → ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩ )
13 9 12 preq12d ⊢ ( 𝑥 = 0 → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩ } )
14 13 eqeq2d ⊢ ( 𝑥 = 0 → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ↔ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩ } ) )
15 8 11 14 3orbi123d ⊢ ( 𝑥 = 0 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ) ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩ } ) ) )
16 2 15 anbi12d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ∈ ( 0 ..^ 5 ) ∧ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ) ) ↔ ( 0 ∈ ( 0 ..^ 5 ) ∧ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩ } ) ) ) )
17 5nn ⊢ 5 ∈ ℕ
18 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 5 ) ↔ 5 ∈ ℕ )
19 17 18 mpbir ⊢ 0 ∈ ( 0 ..^ 5 )
20 0p1e1 ⊢ ( 0 + 1 ) = 1
21 20 oveq1i ⊢ ( ( 0 + 1 ) mod 5 ) = ( 1 mod 5 )
22 5re ⊢ 5 ∈ ℝ
23 1lt5 ⊢ 1 < 5
24 1mod ⊢ ( ( 5 ∈ ℝ ∧ 1 < 5 ) → ( 1 mod 5 ) = 1 )
25 22 23 24 mp2an ⊢ ( 1 mod 5 ) = 1
26 21 25 eqtr2i ⊢ 1 = ( ( 0 + 1 ) mod 5 )
27 26 opeq2i ⊢ ⟨ 1 , 1 ⟩ = ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩
28 27 preq2i ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩ }
29 28 3mix3i ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩ } )
30 19 29 pm3.2i ⊢ ( 0 ∈ ( 0 ..^ 5 ) ∧ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 0 ⟩ , ⟨ 1 , ( ( 0 + 1 ) mod 5 ) ⟩ } ) )
31 1 16 30 ceqsexv2d ⊢ ∃ 𝑥 ( 𝑥 ∈ ( 0 ..^ 5 ) ∧ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ) )
32 df-rex ⊢ ( ∃ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ) ↔ ∃ 𝑥 ( 𝑥 ∈ ( 0 ..^ 5 ) ∧ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ) ) )
33 31 32 mpbir ⊢ ∃ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } )
34 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
35 2z ⊢ 2 ∈ ℤ
36 22 rehalfcli ⊢ ( 5 / 2 ) ∈ ℝ
37 ceilcl ⊢ ( ( 5 / 2 ) ∈ ℝ → ( ⌈ ‘ ( 5 / 2 ) ) ∈ ℤ )
38 36 37 ax-mp ⊢ ( ⌈ ‘ ( 5 / 2 ) ) ∈ ℤ
39 2ltceilhalf ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ ( ⌈ ‘ ( 5 / 2 ) ) )
40 34 39 ax-mp ⊢ 2 ≤ ( ⌈ ‘ ( 5 / 2 ) )
41 eluz2 ⊢ ( ( ⌈ ‘ ( 5 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ⌈ ‘ ( 5 / 2 ) ) ∈ ℤ ∧ 2 ≤ ( ⌈ ‘ ( 5 / 2 ) ) ) )
42 35 38 40 41 mpbir3an ⊢ ( ⌈ ‘ ( 5 / 2 ) ) ∈ ( ℤ≥ ‘ 2 )
43 fzo1lb ⊢ ( 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ↔ ( ⌈ ‘ ( 5 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) )
44 42 43 mpbir ⊢ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
45 eqid ⊢ ( 0 ..^ 5 ) = ( 0 ..^ 5 )
46 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
47 eqid ⊢ ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 )
48 eqid ⊢ ( Edg ‘ ( 5 gPetersenGr 1 ) ) = ( Edg ‘ ( 5 gPetersenGr 1 ) )
49 45 46 47 48 gpgedgel ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ) ) )
50 34 44 49 mp2an ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ) )
51 33 50 mpbir ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) )
52 pglem ⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
53 opex ⊢ ⟨ 1 , 0 ⟩ ∈ V
54 opex ⊢ ⟨ 1 , 1 ⟩ ∈ V
55 53 54 pm3.2i ⊢ ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V )
56 opex ⊢ ⟨ 0 , 𝑥 ⟩ ∈ V
57 opex ⊢ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ∈ V
58 56 57 pm3.2i ⊢ ( ⟨ 0 , 𝑥 ⟩ ∈ V ∧ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ∈ V )
59 55 58 pm3.2i ⊢ ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 0 , 𝑥 ⟩ ∈ V ∧ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ∈ V ) )
60 ax-1ne0 ⊢ 1 ≠ 0
61 60 orci ⊢ ( 1 ≠ 0 ∨ 0 ≠ 𝑥 )
62 1ex ⊢ 1 ∈ V
63 62 1 opthne ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ↔ ( 1 ≠ 0 ∨ 0 ≠ 𝑥 ) )
64 61 63 mpbir ⊢ ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩
65 60 orci ⊢ ( 1 ≠ 0 ∨ 0 ≠ ( ( 𝑥 + 1 ) mod 5 ) )
66 62 1 opthne ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ↔ ( 1 ≠ 0 ∨ 0 ≠ ( ( 𝑥 + 1 ) mod 5 ) ) )
67 65 66 mpbir ⊢ ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩
68 64 67 pm3.2i ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ )
69 68 a1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ) )
70 69 orcd ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ) ∨ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ) ) )
71 prneimg ⊢ ( ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 0 , 𝑥 ⟩ ∈ V ∧ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ∈ V ) ) → ( ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∧ ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ) ∨ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ) )
72 59 70 71 mpsyl ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } )
73 64 orci ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ )
74 73 a1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ) )
75 60 orci ⊢ ( 1 ≠ 0 ∨ 1 ≠ 𝑥 )
76 62 62 opthne ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ↔ ( 1 ≠ 0 ∨ 1 ≠ 𝑥 ) )
77 75 76 mpbir ⊢ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 𝑥 ⟩
78 77 olci ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ )
79 78 a1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ) )
80 opex ⊢ ⟨ 1 , 𝑥 ⟩ ∈ V
81 56 80 pm3.2i ⊢ ( ⟨ 0 , 𝑥 ⟩ ∈ V ∧ ⟨ 1 , 𝑥 ⟩ ∈ V )
82 55 81 pm3.2i ⊢ ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 0 , 𝑥 ⟩ ∈ V ∧ ⟨ 1 , 𝑥 ⟩ ∈ V ) )
83 prneimg2 ⊢ ( ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 0 , 𝑥 ⟩ ∈ V ∧ ⟨ 1 , 𝑥 ⟩ ∈ V ) ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ) ∧ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ) ) ) )
84 82 83 mp1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ) ∧ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 0 , 𝑥 ⟩ ) ) ) )
85 74 79 84 mpbir2and ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } )
86 1ne2 ⊢ 1 ≠ 2
87 86 a1i ⊢ ( ( 0 = 𝑥 ∧ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) ) → 1 ≠ 2 )
88 2cn ⊢ 2 ∈ ℂ
89 88 addlidi ⊢ ( 0 + 2 ) = 2
90 89 oveq1i ⊢ ( ( 0 + 2 ) mod 5 ) = ( 2 mod 5 )
91 2nn0 ⊢ 2 ∈ ℕ0
92 2lt5 ⊢ 2 < 5
93 elfzo0 ⊢ ( 2 ∈ ( 0 ..^ 5 ) ↔ ( 2 ∈ ℕ0 ∧ 5 ∈ ℕ ∧ 2 < 5 ) )
94 91 17 92 93 mpbir3an ⊢ 2 ∈ ( 0 ..^ 5 )
95 zmodidfzoimp ⊢ ( 2 ∈ ( 0 ..^ 5 ) → ( 2 mod 5 ) = 2 )
96 94 95 ax-mp ⊢ ( 2 mod 5 ) = 2
97 90 96 eqtr2i ⊢ 2 = ( ( 0 + 2 ) mod 5 )
98 oveq1 ⊢ ( 0 = 𝑥 → ( 0 + 2 ) = ( 𝑥 + 2 ) )
99 98 oveq1d ⊢ ( 0 = 𝑥 → ( ( 0 + 2 ) mod 5 ) = ( ( 𝑥 + 2 ) mod 5 ) )
100 97 99 eqtrid ⊢ ( 0 = 𝑥 → 2 = ( ( 𝑥 + 2 ) mod 5 ) )
101 100 adantr ⊢ ( ( 0 = 𝑥 ∧ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) ) → 2 = ( ( 𝑥 + 2 ) mod 5 ) )
102 87 101 neeqtrd ⊢ ( ( 0 = 𝑥 ∧ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) ) → 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) )
103 102 olcd ⊢ ( ( 0 = 𝑥 ∧ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) ) → ( 0 ≠ 𝑥 ∨ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
104 103 ex ⊢ ( 0 = 𝑥 → ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( 0 ≠ 𝑥 ∨ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) ) )
105 orc ⊢ ( 0 ≠ 𝑥 → ( 0 ≠ 𝑥 ∨ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
106 105 a1d ⊢ ( 0 ≠ 𝑥 → ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( 0 ≠ 𝑥 ∨ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) ) )
107 104 106 pm2.61ine ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( 0 ≠ 𝑥 ∨ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
108 62 1 opthne ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ↔ ( 1 ≠ 1 ∨ 0 ≠ 𝑥 ) )
109 neirr ⊢ ¬ 1 ≠ 1
110 109 biorfi ⊢ ( 0 ≠ 𝑥 ↔ ( 1 ≠ 1 ∨ 0 ≠ 𝑥 ) )
111 108 110 bitr4i ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ↔ 0 ≠ 𝑥 )
112 111 a1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ↔ 0 ≠ 𝑥 ) )
113 62 62 opthne ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ↔ ( 1 ≠ 1 ∨ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
114 109 biorfi ⊢ ( 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ↔ ( 1 ≠ 1 ∨ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
115 113 114 bitr4i ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ↔ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) )
116 115 a1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ↔ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
117 112 116 orbi12d ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ) ↔ ( 0 ≠ 𝑥 ∨ 1 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) ) )
118 107 117 mpbird ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ) )
119 0re ⊢ 0 ∈ ℝ
120 3pos ⊢ 0 < 3
121 119 120 ltneii ⊢ 0 ≠ 3
122 121 a1i ⊢ ( ( 1 = 𝑥 ∧ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) ) → 0 ≠ 3 )
123 1p2e3 ⊢ ( 1 + 2 ) = 3
124 123 oveq1i ⊢ ( ( 1 + 2 ) mod 5 ) = ( 3 mod 5 )
125 3nn0 ⊢ 3 ∈ ℕ0
126 3lt5 ⊢ 3 < 5
127 elfzo0 ⊢ ( 3 ∈ ( 0 ..^ 5 ) ↔ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ ∧ 3 < 5 ) )
128 125 17 126 127 mpbir3an ⊢ 3 ∈ ( 0 ..^ 5 )
129 zmodidfzoimp ⊢ ( 3 ∈ ( 0 ..^ 5 ) → ( 3 mod 5 ) = 3 )
130 128 129 ax-mp ⊢ ( 3 mod 5 ) = 3
131 124 130 eqtr2i ⊢ 3 = ( ( 1 + 2 ) mod 5 )
132 oveq1 ⊢ ( 1 = 𝑥 → ( 1 + 2 ) = ( 𝑥 + 2 ) )
133 132 oveq1d ⊢ ( 1 = 𝑥 → ( ( 1 + 2 ) mod 5 ) = ( ( 𝑥 + 2 ) mod 5 ) )
134 131 133 eqtrid ⊢ ( 1 = 𝑥 → 3 = ( ( 𝑥 + 2 ) mod 5 ) )
135 134 adantr ⊢ ( ( 1 = 𝑥 ∧ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) ) → 3 = ( ( 𝑥 + 2 ) mod 5 ) )
136 122 135 neeqtrd ⊢ ( ( 1 = 𝑥 ∧ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) ) → 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) )
137 136 orcd ⊢ ( ( 1 = 𝑥 ∧ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) ) → ( 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ∨ 1 ≠ 𝑥 ) )
138 137 ex ⊢ ( 1 = 𝑥 → ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ∨ 1 ≠ 𝑥 ) ) )
139 olc ⊢ ( 1 ≠ 𝑥 → ( 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ∨ 1 ≠ 𝑥 ) )
140 139 a1d ⊢ ( 1 ≠ 𝑥 → ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ∨ 1 ≠ 𝑥 ) ) )
141 138 140 pm2.61ine ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ∨ 1 ≠ 𝑥 ) )
142 62 1 opthne ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ↔ ( 1 ≠ 1 ∨ 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
143 109 biorfi ⊢ ( 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ↔ ( 1 ≠ 1 ∨ 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
144 142 143 bitr4i ⊢ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ↔ 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) )
145 144 a1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ↔ 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ) )
146 62 62 opthne ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ↔ ( 1 ≠ 1 ∨ 1 ≠ 𝑥 ) )
147 109 biorfi ⊢ ( 1 ≠ 𝑥 ↔ ( 1 ≠ 1 ∨ 1 ≠ 𝑥 ) )
148 146 147 bitr4i ⊢ ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ↔ 1 ≠ 𝑥 )
149 148 a1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ↔ 1 ≠ 𝑥 ) )
150 145 149 orbi12d ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ) ↔ ( 0 ≠ ( ( 𝑥 + 2 ) mod 5 ) ∨ 1 ≠ 𝑥 ) ) )
151 141 150 mpbird ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ) )
152 opex ⊢ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ∈ V
153 80 152 pm3.2i ⊢ ( ⟨ 1 , 𝑥 ⟩ ∈ V ∧ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ∈ V )
154 55 153 pm3.2i ⊢ ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 𝑥 ⟩ ∈ V ∧ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ∈ V ) )
155 prneimg2 ⊢ ( ( ( ⟨ 1 , 0 ⟩ ∈ V ∧ ⟨ 1 , 1 ⟩ ∈ V ) ∧ ( ⟨ 1 , 𝑥 ⟩ ∈ V ∧ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ∈ V ) ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ↔ ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ) ∧ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ) ) ) )
156 154 155 mp1i ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ↔ ( ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ) ∧ ( ⟨ 1 , 0 ⟩ ≠ ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ ∨ ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 𝑥 ⟩ ) ) ) )
157 118 151 156 mpbir2and ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } )
158 72 85 157 3jca ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
159 158 ralrimiva ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ∀ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
160 ralnex ⊢ ( ∀ 𝑥 ∈ ( 0 ..^ 5 ) ¬ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) ↔ ¬ ∃ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
161 3ioran ⊢ ( ¬ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) ↔ ( ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∧ ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∧ ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
162 df-ne ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ↔ ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } )
163 df-ne ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } )
164 df-ne ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ↔ ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } )
165 162 163 164 3anbi123i ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) ↔ ( ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∧ ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∧ ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
166 161 165 bitr4i ⊢ ( ¬ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
167 166 ralbii ⊢ ( ∀ 𝑥 ∈ ( 0 ..^ 5 ) ¬ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) ↔ ∀ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
168 160 167 bitr3i ⊢ ( ¬ ∃ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) ↔ ∀ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ≠ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
169 159 168 sylibr ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ¬ ∃ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) )
170 eqid ⊢ ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
171 eqid ⊢ ( Edg ‘ ( 5 gPetersenGr 2 ) ) = ( Edg ‘ ( 5 gPetersenGr 2 ) )
172 45 46 170 171 gpgedgel ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 2 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 5 ) ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 5 ) ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 2 ) mod 5 ) ⟩ } ) ) )
173 169 172 mtbird ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 2 ) ) )
174 34 52 173 mp2an ⊢ ¬ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 2 ) )
175 174 nelir ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) )
176 51 175 pm3.2i ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∈ ( Edg ‘ ( 5 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 0 ⟩ , ⟨ 1 , 1 ⟩ } ∉ ( Edg ‘ ( 5 gPetersenGr 2 ) ) )