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

Metamath Proof Explorer

Theorem prneimg

Description: Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017)

Ref Expression
Assertion prneimg ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } ) )

Proof

Step Hyp Ref Expression
1 preq12bg ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
2 orddi ⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ↔ ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐴 = 𝐶 ∨ 𝐵 = 𝐶 ) ) ∧ ( ( 𝐵 = 𝐷 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐷 ∨ 𝐵 = 𝐶 ) ) ) )
3 simpll ⊢ ( ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐴 = 𝐶 ∨ 𝐵 = 𝐶 ) ) ∧ ( ( 𝐵 = 𝐷 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐷 ∨ 𝐵 = 𝐶 ) ) ) → ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) )
4 pm1.4 ⊢ ( ( 𝐵 = 𝐷 ∨ 𝐵 = 𝐶 ) → ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) )
5 4 ad2antll ⊢ ( ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐴 = 𝐶 ∨ 𝐵 = 𝐶 ) ) ∧ ( ( 𝐵 = 𝐷 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐷 ∨ 𝐵 = 𝐶 ) ) ) → ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) )
6 3 5 jca ⊢ ( ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐴 = 𝐶 ∨ 𝐵 = 𝐶 ) ) ∧ ( ( 𝐵 = 𝐷 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐷 ∨ 𝐵 = 𝐶 ) ) ) → ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) )
7 2 6 sylbi ⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) → ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) )
8 1 7 biimtrdi ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ) )
9 ianor ⊢ ( ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ↔ ( ¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷 ) )
10 nne ⊢ ( ¬ 𝐴 ≠ 𝐶 ↔ 𝐴 = 𝐶 )
11 nne ⊢ ( ¬ 𝐴 ≠ 𝐷 ↔ 𝐴 = 𝐷 )
12 10 11 orbi12i ⊢ ( ( ¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷 ) ↔ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) )
13 9 12 bitr2i ⊢ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ↔ ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) )
14 ianor ⊢ ( ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ↔ ( ¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷 ) )
15 nne ⊢ ( ¬ 𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶 )
16 nne ⊢ ( ¬ 𝐵 ≠ 𝐷 ↔ 𝐵 = 𝐷 )
17 15 16 orbi12i ⊢ ( ( ¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷 ) ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) )
18 14 17 bitr2i ⊢ ( ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ↔ ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) )
19 13 18 anbi12i ⊢ ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ↔ ( ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) )
20 8 19 imbitrdi ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) ) )
21 pm4.56 ⊢ ( ( ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) ↔ ¬ ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) )
22 20 21 imbitrdi ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ¬ ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) ) )
23 22 necon2ad ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } ) )