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

Theorem djuunxp 9338
Description: The union of a disjoint union and its inversion is the Cartesian product of an unordered pair and the union of the left and right classes of the disjoint unions. (Proposed by GL, 4-Jul-2022.) (Contributed by AV, 4-Jul-2022.)
Assertion
Ref Expression
djuunxp ((𝐴𝐵) ∪ (𝐵𝐴)) = ({∅, 1o} × (𝐴𝐵))

Proof of Theorem djuunxp
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 djuss 9337 . . 3 (𝐴𝐵) ⊆ ({∅, 1o} × (𝐴𝐵))
2 djuss 9337 . . . 4 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐵𝐴))
3 uncom 4126 . . . . 5 (𝐴𝐵) = (𝐵𝐴)
43xpeq2i 5575 . . . 4 ({∅, 1o} × (𝐴𝐵)) = ({∅, 1o} × (𝐵𝐴))
52, 4sseqtrri 4001 . . 3 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐴𝐵))
61, 5unssi 4158 . 2 ((𝐴𝐵) ∪ (𝐵𝐴)) ⊆ ({∅, 1o} × (𝐴𝐵))
7 elxpi 5570 . . . 4 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → ∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))))
8 vex 3495 . . . . . . . . . 10 𝑦 ∈ V
98elpr 4580 . . . . . . . . 9 (𝑦 ∈ {∅, 1o} ↔ (𝑦 = ∅ ∨ 𝑦 = 1o))
10 elun 4122 . . . . . . . . 9 (𝑧 ∈ (𝐴𝐵) ↔ (𝑧𝐴𝑧𝐵))
11 velsn 4573 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
1211biimpri 229 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ∅ → 𝑦 ∈ {∅})
1312anim1i 614 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = ∅ ∧ 𝑧𝐴) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1413ancoms 459 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐴𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
15 opelxp 5584 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1614, 15sylibr 235 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴))
1716orcd 869 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
18 elun 4122 . . . . . . . . . . . . . . . 16 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
1917, 18sylibr 235 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
2019orcd 869 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2120ex 413 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2212anim1i 614 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ∅ ∧ 𝑧𝐵) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2322ancoms 459 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
24 opelxp 5584 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2523, 24sylibr 235 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵))
2625orcd 869 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
2726olcd 870 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2827ex 413 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2921, 28jaoi 851 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
3029com12 32 . . . . . . . . . . 11 (𝑦 = ∅ → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
31 velsn 4573 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1o} ↔ 𝑦 = 1o)
3231biimpri 229 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 1o𝑦 ∈ {1o})
3332anim1i 614 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 1o𝑧𝐴) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3433ancoms 459 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
35 opelxp 5584 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3634, 35sylibr 235 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))
3736olcd 870 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
3837olcd 870 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
3938ex 413 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4032anim1i 614 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 1o𝑧𝐵) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4140ancoms 459 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
42 opelxp 5584 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4341, 42sylibr 235 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵))
4443olcd 870 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
4544, 18sylibr 235 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
4645orcd 869 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
4746ex 413 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4839, 47jaoi 851 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4948com12 32 . . . . . . . . . . 11 (𝑦 = 1o → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5030, 49jaoi 851 . . . . . . . . . 10 ((𝑦 = ∅ ∨ 𝑦 = 1o) → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5150imp 407 . . . . . . . . 9 (((𝑦 = ∅ ∨ 𝑦 = 1o) ∧ (𝑧𝐴𝑧𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
529, 10, 51syl2anb 597 . . . . . . . 8 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
53 elun 4122 . . . . . . . . 9 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)))
54 df-dju 9318 . . . . . . . . . . 11 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
5554eleq2i 2901 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
56 df-dju 9318 . . . . . . . . . . . 12 (𝐵𝐴) = (({∅} × 𝐵) ∪ ({1o} × 𝐴))
5756eleq2i 2901 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)))
58 elun 4122 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
5957, 58bitri 276 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
6055, 59orbi12i 908 . . . . . . . . 9 ((⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6153, 60bitri 276 . . . . . . . 8 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6252, 61sylibr 235 . . . . . . 7 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6362adantl 482 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
64 eleq1 2897 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6564adantr 481 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6663, 65mpbird 258 . . . . 5 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6766exlimivv 1924 . . . 4 (∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
687, 67syl 17 . . 3 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6968ssriv 3968 . 2 ({∅, 1o} × (𝐴𝐵)) ⊆ ((𝐴𝐵) ∪ (𝐵𝐴))
706, 69eqssi 3980 1 ((𝐴𝐵) ∪ (𝐵𝐴)) = ({∅, 1o} × (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wex 1771  wcel 2105  cun 3931  c0 4288  {csn 4557  {cpr 4559  cop 4563   × cxp 5546  1oc1o 8084  cdju 9315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-ord 6187  df-on 6188  df-suc 6190  df-iota 6307  df-fun 6350  df-fv 6356  df-1st 7678  df-2nd 7679  df-1o 8091  df-dju 9318  df-inl 9319  df-inr 9320
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator