MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prnebg Structured version   Visualization version   GIF version

Theorem prnebg 4784
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.)
Assertion
Ref Expression
prnebg (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))

Proof of Theorem prnebg
StepHypRef Expression
1 prneimg 4783 . . 3 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌)) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
213adant3 1126 . 2 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
3 ioran 979 . . . . 5 (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ (¬ (𝐴𝐶𝐴𝐷) ∧ ¬ (𝐵𝐶𝐵𝐷)))
4 ianor 977 . . . . . . 7 (¬ (𝐴𝐶𝐴𝐷) ↔ (¬ 𝐴𝐶 ∨ ¬ 𝐴𝐷))
5 nne 3024 . . . . . . . 8 𝐴𝐶𝐴 = 𝐶)
6 nne 3024 . . . . . . . 8 𝐴𝐷𝐴 = 𝐷)
75, 6orbi12i 910 . . . . . . 7 ((¬ 𝐴𝐶 ∨ ¬ 𝐴𝐷) ↔ (𝐴 = 𝐶𝐴 = 𝐷))
84, 7bitri 276 . . . . . 6 (¬ (𝐴𝐶𝐴𝐷) ↔ (𝐴 = 𝐶𝐴 = 𝐷))
9 ianor 977 . . . . . . 7 (¬ (𝐵𝐶𝐵𝐷) ↔ (¬ 𝐵𝐶 ∨ ¬ 𝐵𝐷))
10 nne 3024 . . . . . . . 8 𝐵𝐶𝐵 = 𝐶)
11 nne 3024 . . . . . . . 8 𝐵𝐷𝐵 = 𝐷)
1210, 11orbi12i 910 . . . . . . 7 ((¬ 𝐵𝐶 ∨ ¬ 𝐵𝐷) ↔ (𝐵 = 𝐶𝐵 = 𝐷))
139, 12bitri 276 . . . . . 6 (¬ (𝐵𝐶𝐵𝐷) ↔ (𝐵 = 𝐶𝐵 = 𝐷))
148, 13anbi12i 626 . . . . 5 ((¬ (𝐴𝐶𝐴𝐷) ∧ ¬ (𝐵𝐶𝐵𝐷)) ↔ ((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)))
153, 14bitri 276 . . . 4 (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ ((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)))
16 anddi 1006 . . . . 5 (((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)) ↔ (((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))))
17 eqtr3 2847 . . . . . . . . . 10 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
18 eqneqall 3031 . . . . . . . . . 10 (𝐴 = 𝐵 → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
1917, 18syl 17 . . . . . . . . 9 ((𝐴 = 𝐶𝐵 = 𝐶) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
20 preq12 4669 . . . . . . . . . 10 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
2120a1d 25 . . . . . . . . 9 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
2219, 21jaoi 853 . . . . . . . 8 (((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
23 preq12 4669 . . . . . . . . . . 11 ((𝐴 = 𝐷𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐷, 𝐶})
24 prcom 4666 . . . . . . . . . . 11 {𝐷, 𝐶} = {𝐶, 𝐷}
2523, 24syl6eq 2876 . . . . . . . . . 10 ((𝐴 = 𝐷𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶, 𝐷})
2625a1d 25 . . . . . . . . 9 ((𝐴 = 𝐷𝐵 = 𝐶) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
27 eqtr3 2847 . . . . . . . . . 10 ((𝐴 = 𝐷𝐵 = 𝐷) → 𝐴 = 𝐵)
2827, 18syl 17 . . . . . . . . 9 ((𝐴 = 𝐷𝐵 = 𝐷) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
2926, 28jaoi 853 . . . . . . . 8 (((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷)) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
3022, 29jaoi 853 . . . . . . 7 ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
3130com12 32 . . . . . 6 (𝐴𝐵 → ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
32313ad2ant3 1129 . . . . 5 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3316, 32syl5bi 243 . . . 4 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3415, 33syl5bi 243 . . 3 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3534necon1ad 3037 . 2 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → ({𝐴, 𝐵} ≠ {𝐶, 𝐷} → ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷))))
362, 35impbid 213 1 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  wcel 2107  wne 3020  {cpr 4565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-v 3501  df-un 3944  df-sn 4564  df-pr 4566
This theorem is referenced by:  zlmodzxznm  44386
  Copyright terms: Public domain W3C validator