This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrexmpldifpr

Description: Lemma for usgrexmpledg : all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017)

Ref Expression
Assertion usgrexmpldifpr ( ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 0 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 1 , 2 } ≠ { 2 , 0 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 2 , 0 } ≠ { 0 , 3 } ) )

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 1z ⊢ 1 ∈ ℤ
3 1 2 pm3.2i ⊢ ( 0 ∈ ℤ ∧ 1 ∈ ℤ )
4 2z ⊢ 2 ∈ ℤ
5 2 4 pm3.2i ⊢ ( 1 ∈ ℤ ∧ 2 ∈ ℤ )
6 3 5 pm3.2i ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 1 ∈ ℤ ∧ 2 ∈ ℤ ) )
7 ax-1ne0 ⊢ 1 ≠ 0
8 7 necomi ⊢ 0 ≠ 1
9 2ne0 ⊢ 2 ≠ 0
10 9 necomi ⊢ 0 ≠ 2
11 8 10 pm3.2i ⊢ ( 0 ≠ 1 ∧ 0 ≠ 2 )
12 11 orci ⊢ ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 1 ≠ 1 ∧ 1 ≠ 2 ) )
13 prneimg ⊢ ( ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 1 ∈ ℤ ∧ 2 ∈ ℤ ) ) → ( ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 1 ≠ 1 ∧ 1 ≠ 2 ) ) → { 0 , 1 } ≠ { 1 , 2 } ) )
14 6 12 13 mp2 ⊢ { 0 , 1 } ≠ { 1 , 2 }
15 4 1 pm3.2i ⊢ ( 2 ∈ ℤ ∧ 0 ∈ ℤ )
16 3 15 pm3.2i ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 2 ∈ ℤ ∧ 0 ∈ ℤ ) )
17 1ne2 ⊢ 1 ≠ 2
18 17 7 pm3.2i ⊢ ( 1 ≠ 2 ∧ 1 ≠ 0 )
19 18 olci ⊢ ( ( 0 ≠ 2 ∧ 0 ≠ 0 ) ∨ ( 1 ≠ 2 ∧ 1 ≠ 0 ) )
20 prneimg ⊢ ( ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 2 ∈ ℤ ∧ 0 ∈ ℤ ) ) → ( ( ( 0 ≠ 2 ∧ 0 ≠ 0 ) ∨ ( 1 ≠ 2 ∧ 1 ≠ 0 ) ) → { 0 , 1 } ≠ { 2 , 0 } ) )
21 16 19 20 mp2 ⊢ { 0 , 1 } ≠ { 2 , 0 }
22 3nn ⊢ 3 ∈ ℕ
23 1 22 pm3.2i ⊢ ( 0 ∈ ℤ ∧ 3 ∈ ℕ )
24 3 23 pm3.2i ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ 3 ∈ ℕ ) )
25 1re ⊢ 1 ∈ ℝ
26 1lt3 ⊢ 1 < 3
27 25 26 ltneii ⊢ 1 ≠ 3
28 7 27 pm3.2i ⊢ ( 1 ≠ 0 ∧ 1 ≠ 3 )
29 28 olci ⊢ ( ( 0 ≠ 0 ∧ 0 ≠ 3 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 3 ) )
30 prneimg ⊢ ( ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ 3 ∈ ℕ ) ) → ( ( ( 0 ≠ 0 ∧ 0 ≠ 3 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 3 ) ) → { 0 , 1 } ≠ { 0 , 3 } ) )
31 24 29 30 mp2 ⊢ { 0 , 1 } ≠ { 0 , 3 }
32 14 21 31 3pm3.2i ⊢ ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 0 } ∧ { 0 , 1 } ≠ { 0 , 3 } )
33 5 15 pm3.2i ⊢ ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 2 ∈ ℤ ∧ 0 ∈ ℤ ) )
34 18 orci ⊢ ( ( 1 ≠ 2 ∧ 1 ≠ 0 ) ∨ ( 2 ≠ 2 ∧ 2 ≠ 0 ) )
35 prneimg ⊢ ( ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 2 ∈ ℤ ∧ 0 ∈ ℤ ) ) → ( ( ( 1 ≠ 2 ∧ 1 ≠ 0 ) ∨ ( 2 ≠ 2 ∧ 2 ≠ 0 ) ) → { 1 , 2 } ≠ { 2 , 0 } ) )
36 33 34 35 mp2 ⊢ { 1 , 2 } ≠ { 2 , 0 }
37 5 23 pm3.2i ⊢ ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ 3 ∈ ℕ ) )
38 28 orci ⊢ ( ( 1 ≠ 0 ∧ 1 ≠ 3 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 3 ) )
39 prneimg ⊢ ( ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ 3 ∈ ℕ ) ) → ( ( ( 1 ≠ 0 ∧ 1 ≠ 3 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 3 ) ) → { 1 , 2 } ≠ { 0 , 3 } ) )
40 37 38 39 mp2 ⊢ { 1 , 2 } ≠ { 0 , 3 }
41 15 23 pm3.2i ⊢ ( ( 2 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ 3 ∈ ℕ ) )
42 2re ⊢ 2 ∈ ℝ
43 2lt3 ⊢ 2 < 3
44 42 43 ltneii ⊢ 2 ≠ 3
45 9 44 pm3.2i ⊢ ( 2 ≠ 0 ∧ 2 ≠ 3 )
46 45 orci ⊢ ( ( 2 ≠ 0 ∧ 2 ≠ 3 ) ∨ ( 0 ≠ 0 ∧ 0 ≠ 3 ) )
47 prneimg ⊢ ( ( ( 2 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ 3 ∈ ℕ ) ) → ( ( ( 2 ≠ 0 ∧ 2 ≠ 3 ) ∨ ( 0 ≠ 0 ∧ 0 ≠ 3 ) ) → { 2 , 0 } ≠ { 0 , 3 } ) )
48 41 46 47 mp2 ⊢ { 2 , 0 } ≠ { 0 , 3 }
49 36 40 48 3pm3.2i ⊢ ( { 1 , 2 } ≠ { 2 , 0 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 2 , 0 } ≠ { 0 , 3 } )
50 32 49 pm3.2i ⊢ ( ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 0 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 1 , 2 } ≠ { 2 , 0 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 2 , 0 } ≠ { 0 , 3 } ) )