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

Metamath Proof Explorer

Theorem prnebg

Description: A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018)

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

Proof

Step Hyp Ref Expression
1 prneimg ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } ) )
2 1 3adant3 ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } ) )
3 ioran ⊢ ( ¬ ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) ↔ ( ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) )
4 ianor ⊢ ( ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ↔ ( ¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷 ) )
5 nne ⊢ ( ¬ 𝐴 ≠ 𝐶 ↔ 𝐴 = 𝐶 )
6 nne ⊢ ( ¬ 𝐴 ≠ 𝐷 ↔ 𝐴 = 𝐷 )
7 5 6 orbi12i ⊢ ( ( ¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷 ) ↔ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) )
8 4 7 bitri ⊢ ( ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ↔ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) )
9 ianor ⊢ ( ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ↔ ( ¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷 ) )
10 nne ⊢ ( ¬ 𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶 )
11 nne ⊢ ( ¬ 𝐵 ≠ 𝐷 ↔ 𝐵 = 𝐷 )
12 10 11 orbi12i ⊢ ( ( ¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷 ) ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) )
13 9 12 bitri ⊢ ( ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) )
14 8 13 anbi12i ⊢ ( ( ¬ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ¬ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) ↔ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) )
15 3 14 bitri ⊢ ( ¬ ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) ↔ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) )
16 anddi ⊢ ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ↔ ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ∨ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) ) ) )
17 eqtr3 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐵 )
18 eqneqall ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
19 17 18 syl ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
20 preq12 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
21 20 a1d ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
22 19 21 jaoi ⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
23 preq12 ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } )
24 prcom ⊢ { 𝐷 , 𝐶 } = { 𝐶 , 𝐷 }
25 23 24 eqtrdi ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
26 25 a1d ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
27 eqtr3 ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) → 𝐴 = 𝐵 )
28 27 18 syl ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
29 26 28 jaoi ⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
30 22 29 jaoi ⊢ ( ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ∨ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) ) ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
31 30 com12 ⊢ ( 𝐴 ≠ 𝐵 → ( ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ∨ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) ) ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
32 31 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ∨ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) ) ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
33 16 32 biimtrid ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
34 15 33 biimtrid ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( ¬ ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
35 34 necon1ad ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } → ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) ) )
36 2 35 impbid ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∨ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) ↔ { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } ) )