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

Theorem prnebg 4606
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 4605 . . 3 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌)) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
213adant3 1166 . 2 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
3 ioran 1011 . . . . 5 (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ (¬ (𝐴𝐶𝐴𝐷) ∧ ¬ (𝐵𝐶𝐵𝐷)))
4 ianor 1009 . . . . . . 7 (¬ (𝐴𝐶𝐴𝐷) ↔ (¬ 𝐴𝐶 ∨ ¬ 𝐴𝐷))
5 nne 3003 . . . . . . . 8 𝐴𝐶𝐴 = 𝐶)
6 nne 3003 . . . . . . . 8 𝐴𝐷𝐴 = 𝐷)
75, 6orbi12i 943 . . . . . . 7 ((¬ 𝐴𝐶 ∨ ¬ 𝐴𝐷) ↔ (𝐴 = 𝐶𝐴 = 𝐷))
84, 7bitri 267 . . . . . 6 (¬ (𝐴𝐶𝐴𝐷) ↔ (𝐴 = 𝐶𝐴 = 𝐷))
9 ianor 1009 . . . . . . 7 (¬ (𝐵𝐶𝐵𝐷) ↔ (¬ 𝐵𝐶 ∨ ¬ 𝐵𝐷))
10 nne 3003 . . . . . . . 8 𝐵𝐶𝐵 = 𝐶)
11 nne 3003 . . . . . . . 8 𝐵𝐷𝐵 = 𝐷)
1210, 11orbi12i 943 . . . . . . 7 ((¬ 𝐵𝐶 ∨ ¬ 𝐵𝐷) ↔ (𝐵 = 𝐶𝐵 = 𝐷))
139, 12bitri 267 . . . . . 6 (¬ (𝐵𝐶𝐵𝐷) ↔ (𝐵 = 𝐶𝐵 = 𝐷))
148, 13anbi12i 620 . . . . 5 ((¬ (𝐴𝐶𝐴𝐷) ∧ ¬ (𝐵𝐶𝐵𝐷)) ↔ ((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)))
153, 14bitri 267 . . . 4 (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ ((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)))
16 anddi 1038 . . . . 5 (((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)) ↔ (((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))))
17 eqtr3 2848 . . . . . . . . . 10 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
18 eqneqall 3010 . . . . . . . . . 10 (𝐴 = 𝐵 → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
1917, 18syl 17 . . . . . . . . 9 ((𝐴 = 𝐶𝐵 = 𝐶) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
20 preq12 4490 . . . . . . . . . 10 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
2120a1d 25 . . . . . . . . 9 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
2219, 21jaoi 888 . . . . . . . 8 (((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
23 preq12 4490 . . . . . . . . . . 11 ((𝐴 = 𝐷𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐷, 𝐶})
24 prcom 4487 . . . . . . . . . . 11 {𝐷, 𝐶} = {𝐶, 𝐷}
2523, 24syl6eq 2877 . . . . . . . . . 10 ((𝐴 = 𝐷𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶, 𝐷})
2625a1d 25 . . . . . . . . 9 ((𝐴 = 𝐷𝐵 = 𝐶) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
27 eqtr3 2848 . . . . . . . . . 10 ((𝐴 = 𝐷𝐵 = 𝐷) → 𝐴 = 𝐵)
2827, 18syl 17 . . . . . . . . 9 ((𝐴 = 𝐷𝐵 = 𝐷) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
2926, 28jaoi 888 . . . . . . . 8 (((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷)) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
3022, 29jaoi 888 . . . . . . 7 ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → (𝐴𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
3130com12 32 . . . . . 6 (𝐴𝐵 → ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
32313ad2ant3 1169 . . . . 5 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → ((((𝐴 = 𝐶𝐵 = 𝐶) ∨ (𝐴 = 𝐶𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷𝐵 = 𝐶) ∨ (𝐴 = 𝐷𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3316, 32syl5bi 234 . . . 4 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴 = 𝐶𝐴 = 𝐷) ∧ (𝐵 = 𝐶𝐵 = 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3415, 33syl5bi 234 . . 3 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (¬ ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
3534necon1ad 3016 . 2 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → ({𝐴, 𝐵} ≠ {𝐶, 𝐷} → ((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷))))
362, 35impbid 204 1 (((𝐴𝑈𝐵𝑉) ∧ (𝐶𝑋𝐷𝑌) ∧ 𝐴𝐵) → (((𝐴𝐶𝐴𝐷) ∨ (𝐵𝐶𝐵𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 878  w3a 1111   = wceq 1656  wcel 2164  wne 2999  {cpr 4401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-v 3416  df-un 3803  df-sn 4400  df-pr 4402
This theorem is referenced by:  zlmodzxznm  43151
  Copyright terms: Public domain W3C validator