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 e. ZZ
2 1z 
 |-  1 e. ZZ
3 1 2 pm3.2i 
 |-  ( 0 e. ZZ /\ 1 e. ZZ )
4 2z 
 |-  2 e. ZZ
5 2 4 pm3.2i 
 |-  ( 1 e. ZZ /\ 2 e. ZZ )
6 3 5 pm3.2i 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) /\ ( 1 e. ZZ /\ 2 e. ZZ ) )
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 e. ZZ /\ 1 e. ZZ ) /\ ( 1 e. ZZ /\ 2 e. ZZ ) ) -> ( ( ( 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 e. ZZ /\ 0 e. ZZ )
16 3 15 pm3.2i 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) /\ ( 2 e. ZZ /\ 0 e. ZZ ) )
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 e. ZZ /\ 1 e. ZZ ) /\ ( 2 e. ZZ /\ 0 e. ZZ ) ) -> ( ( ( 0 =/= 2 /\ 0 =/= 0 ) \/ ( 1 =/= 2 /\ 1 =/= 0 ) ) -> { 0 , 1 } =/= { 2 , 0 } ) )
21 16 19 20 mp2 
 |-  { 0 , 1 } =/= { 2 , 0 }
22 3nn 
 |-  3 e. NN
23 1 22 pm3.2i 
 |-  ( 0 e. ZZ /\ 3 e. NN )
24 3 23 pm3.2i 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) /\ ( 0 e. ZZ /\ 3 e. NN ) )
25 1re 
 |-  1 e. RR
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 e. ZZ /\ 1 e. ZZ ) /\ ( 0 e. ZZ /\ 3 e. NN ) ) -> ( ( ( 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 e. ZZ /\ 2 e. ZZ ) /\ ( 2 e. ZZ /\ 0 e. ZZ ) )
34 18 orci 
 |-  ( ( 1 =/= 2 /\ 1 =/= 0 ) \/ ( 2 =/= 2 /\ 2 =/= 0 ) )
35 prneimg 
 |-  ( ( ( 1 e. ZZ /\ 2 e. ZZ ) /\ ( 2 e. ZZ /\ 0 e. ZZ ) ) -> ( ( ( 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 e. ZZ /\ 2 e. ZZ ) /\ ( 0 e. ZZ /\ 3 e. NN ) )
38 28 orci 
 |-  ( ( 1 =/= 0 /\ 1 =/= 3 ) \/ ( 2 =/= 0 /\ 2 =/= 3 ) )
39 prneimg 
 |-  ( ( ( 1 e. ZZ /\ 2 e. ZZ ) /\ ( 0 e. ZZ /\ 3 e. NN ) ) -> ( ( ( 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 e. ZZ /\ 0 e. ZZ ) /\ ( 0 e. ZZ /\ 3 e. NN ) )
42 2re 
 |-  2 e. RR
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 e. ZZ /\ 0 e. ZZ ) /\ ( 0 e. ZZ /\ 3 e. NN ) ) -> ( ( ( 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 } ) )