Theorem zlmodzxzldeplem

Description: A and B are not equal. (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypotheses	zlmodzxzldep.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
	zlmodzxzldep.a	⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
	zlmodzxzldep.b	⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
Assertion	zlmodzxzldeplem	⊢ 𝐴 ≠ 𝐵

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzldep.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2		zlmodzxzldep.a	⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
3		zlmodzxzldep.b	⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
4		opex	⊢ ⟨ 0 , 3 ⟩ ∈ V
5		opex	⊢ ⟨ 1 , 6 ⟩ ∈ V
6	4 5	pm3.2i	⊢ ( ⟨ 0 , 3 ⟩ ∈ V ∧ ⟨ 1 , 6 ⟩ ∈ V )
7		opex	⊢ ⟨ 0 , 2 ⟩ ∈ V
8		opex	⊢ ⟨ 1 , 4 ⟩ ∈ V
9	7 8	pm3.2i	⊢ ( ⟨ 0 , 2 ⟩ ∈ V ∧ ⟨ 1 , 4 ⟩ ∈ V )
10	6 9	pm3.2i	⊢ ( ( ⟨ 0 , 3 ⟩ ∈ V ∧ ⟨ 1 , 6 ⟩ ∈ V ) ∧ ( ⟨ 0 , 2 ⟩ ∈ V ∧ ⟨ 1 , 4 ⟩ ∈ V ) )
11		2re	⊢ 2 ∈ ℝ
12		2lt3	⊢ 2 < 3
13	11 12	gtneii	⊢ 3 ≠ 2
14	13	olci	⊢ ( 0 ≠ 0 ∨ 3 ≠ 2 )
15		c0ex	⊢ 0 ∈ V
16		3ex	⊢ 3 ∈ V
17	15 16	opthne	⊢ ( ⟨ 0 , 3 ⟩ ≠ ⟨ 0 , 2 ⟩ ↔ ( 0 ≠ 0 ∨ 3 ≠ 2 ) )
18	14 17	mpbir	⊢ ⟨ 0 , 3 ⟩ ≠ ⟨ 0 , 2 ⟩
19		0ne1	⊢ 0 ≠ 1
20	19	orci	⊢ ( 0 ≠ 1 ∨ 3 ≠ 4 )
21	15 16	opthne	⊢ ( ⟨ 0 , 3 ⟩ ≠ ⟨ 1 , 4 ⟩ ↔ ( 0 ≠ 1 ∨ 3 ≠ 4 ) )
22	20 21	mpbir	⊢ ⟨ 0 , 3 ⟩ ≠ ⟨ 1 , 4 ⟩
23	18 22	pm3.2i	⊢ ( ⟨ 0 , 3 ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 0 , 3 ⟩ ≠ ⟨ 1 , 4 ⟩ )
24	23	orci	⊢ ( ( ⟨ 0 , 3 ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 0 , 3 ⟩ ≠ ⟨ 1 , 4 ⟩ ) ∨ ( ⟨ 1 , 6 ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 1 , 6 ⟩ ≠ ⟨ 1 , 4 ⟩ ) )
25		prneimg	⊢ ( ( ( ⟨ 0 , 3 ⟩ ∈ V ∧ ⟨ 1 , 6 ⟩ ∈ V ) ∧ ( ⟨ 0 , 2 ⟩ ∈ V ∧ ⟨ 1 , 4 ⟩ ∈ V ) ) → ( ( ( ⟨ 0 , 3 ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 0 , 3 ⟩ ≠ ⟨ 1 , 4 ⟩ ) ∨ ( ⟨ 1 , 6 ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 1 , 6 ⟩ ≠ ⟨ 1 , 4 ⟩ ) ) → { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) )
26	10 24 25	mp2	⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
27	2 3	neeq12i	⊢ ( 𝐴 ≠ 𝐵 ↔ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
28	26 27	mpbir	⊢ 𝐴 ≠ 𝐵