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

Theorem prnebg 4518
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 4517 . . 3 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌)) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
213adant3 1125 . 2 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
3 ioran 912 . . . . 5 (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ (¬ (𝐴𝐶𝐴𝐷) ∧ ¬ (𝐵𝐶𝐵𝐷)))
4 ianor 910 . . . . . . 7 (¬ (𝐴𝐶𝐴𝐷) ↔ (¬ 𝐴𝐶 ∨ ¬ 𝐴𝐷))
5 nne 2946 . . . . . . . 8 𝐴𝐶𝐴 = 𝐶)
6 nne 2946 . . . . . . . 8 𝐴𝐷𝐴 = 𝐷)
75, 6orbi12i 879 . . . . . . 7 ((¬ 𝐴𝐶 ∨ ¬ 𝐴𝐷) ↔ (𝐴 = 𝐶𝐴 = 𝐷))
84, 7bitri 264 . . . . . 6 (¬ (𝐴𝐶𝐴𝐷) ↔ (𝐴 = 𝐶𝐴 = 𝐷))
9 ianor 910 . . . . . . 7 (¬ (𝐵𝐶𝐵𝐷) ↔ (¬ 𝐵𝐶 ∨ ¬ 𝐵𝐷))
10 nne 2946 . . . . . . . 8 𝐵𝐶𝐵 = 𝐶)
11 nne 2946 . . . . . . . 8 𝐵𝐷𝐵 = 𝐷)
1210, 11orbi12i 879 . . . . . . 7 ((¬ 𝐵𝐶 ∨ ¬ 𝐵𝐷) ↔ (𝐵 = 𝐶𝐵 = 𝐷))
139, 12bitri 264 . . . . . 6 (¬ (𝐵𝐶𝐵𝐷) ↔ (𝐵 = 𝐶𝐵 = 𝐷))
148, 13anbi12i 604 . . . . 5 ((¬ (𝐴𝐶𝐴𝐷) ∧ ¬ (𝐵𝐶𝐵𝐷)) ↔ ((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)))
153, 14bitri 264 . . . 4 (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ ((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)))
16 anddi 970 . . . . 5 (((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)) ↔ (((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))))
17 eqtr3 2791 . . . . . . . . . 10 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
18 eqneqall 2953 . . . . . . . . . 10 (𝐴 = 𝐵 → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
1917, 18syl 17 . . . . . . . . 9 ((𝐴 = 𝐶𝐵 = 𝐶) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
20 preq12 4404 . . . . . . . . . 10 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
2120a1d 25 . . . . . . . . 9 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
2219, 21jaoi 837 . . . . . . . 8 (((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
23 preq12 4404 . . . . . . . . . . 11 ((𝐴 = 𝐷𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐷, 𝐶})
24 prcom 4401 . . . . . . . . . . 11 {𝐷, 𝐶} = {𝐶, 𝐷}
2523, 24syl6eq 2820 . . . . . . . . . 10 ((𝐴 = 𝐷𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶, 𝐷})
2625a1d 25 . . . . . . . . 9 ((𝐴 = 𝐷𝐵 = 𝐶) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
27 eqtr3 2791 . . . . . . . . . 10 ((𝐴 = 𝐷𝐵 = 𝐷) → 𝐴 = 𝐵)
2827, 18syl 17 . . . . . . . . 9 ((𝐴 = 𝐷𝐵 = 𝐷) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
2926, 28jaoi 837 . . . . . . . 8 (((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷)) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
3022, 29jaoi 837 . . . . . . 7 ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
3130com12 32 . . . . . 6 (𝐴𝐵 → ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
32313ad2ant3 1128 . . . . 5 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3316, 32syl5bi 232 . . . 4 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3415, 33syl5bi 232 . . 3 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3534necon1ad 2959 . 2 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → ({𝐴, 𝐵} ≠ {𝐶, 𝐷} → ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷))))
362, 35impbid 202 1 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826  w3a 1070   = wceq 1630  wcel 2144  wne 2942  {cpr 4316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-v 3351  df-un 3726  df-sn 4315  df-pr 4317
This theorem is referenced by:  zlmodzxznm  42804
  Copyright terms: Public domain W3C validator