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 } ) )