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

Theorem djuunxp 9961
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 9960 . . 3 (𝐴𝐵) ⊆ ({∅, 1o} × (𝐴𝐵))
2 djuss 9960 . . . 4 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐵𝐴))
3 uncom 4158 . . . . 5 (𝐴𝐵) = (𝐵𝐴)
43xpeq2i 5712 . . . 4 ({∅, 1o} × (𝐴𝐵)) = ({∅, 1o} × (𝐵𝐴))
52, 4sseqtrri 4033 . . 3 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐴𝐵))
61, 5unssi 4191 . 2 ((𝐴𝐵) ∪ (𝐵𝐴)) ⊆ ({∅, 1o} × (𝐴𝐵))
7 elxpi 5707 . . . 4 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → ∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))))
8 vex 3484 . . . . . . . . . 10 𝑦 ∈ V
98elpr 4650 . . . . . . . . 9 (𝑦 ∈ {∅, 1o} ↔ (𝑦 = ∅ ∨ 𝑦 = 1o))
10 elun 4153 . . . . . . . . 9 (𝑧 ∈ (𝐴𝐵) ↔ (𝑧𝐴𝑧𝐵))
11 velsn 4642 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
1211biimpri 228 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ∅ → 𝑦 ∈ {∅})
1312anim1i 615 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = ∅ ∧ 𝑧𝐴) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1413ancoms 458 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐴𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
15 opelxp 5721 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1614, 15sylibr 234 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴))
1716orcd 874 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
18 elun 4153 . . . . . . . . . . . . . . . 16 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
1917, 18sylibr 234 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
2019orcd 874 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2120ex 412 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2212anim1i 615 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ∅ ∧ 𝑧𝐵) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2322ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
24 opelxp 5721 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2523, 24sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵))
2625orcd 874 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
2726olcd 875 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2827ex 412 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2921, 28jaoi 858 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
3029com12 32 . . . . . . . . . . 11 (𝑦 = ∅ → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
31 velsn 4642 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1o} ↔ 𝑦 = 1o)
3231biimpri 228 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 1o𝑦 ∈ {1o})
3332anim1i 615 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 1o𝑧𝐴) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3433ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
35 opelxp 5721 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3634, 35sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))
3736olcd 875 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
3837olcd 875 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
3938ex 412 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4032anim1i 615 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 1o𝑧𝐵) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4140ancoms 458 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
42 opelxp 5721 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4341, 42sylibr 234 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵))
4443olcd 875 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
4544, 18sylibr 234 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
4645orcd 874 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
4746ex 412 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4839, 47jaoi 858 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4948com12 32 . . . . . . . . . . 11 (𝑦 = 1o → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5030, 49jaoi 858 . . . . . . . . . 10 ((𝑦 = ∅ ∨ 𝑦 = 1o) → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5150imp 406 . . . . . . . . 9 (((𝑦 = ∅ ∨ 𝑦 = 1o) ∧ (𝑧𝐴𝑧𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
529, 10, 51syl2anb 598 . . . . . . . 8 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
53 elun 4153 . . . . . . . . 9 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)))
54 df-dju 9941 . . . . . . . . . . 11 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
5554eleq2i 2833 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
56 df-dju 9941 . . . . . . . . . . . 12 (𝐵𝐴) = (({∅} × 𝐵) ∪ ({1o} × 𝐴))
5756eleq2i 2833 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)))
58 elun 4153 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
5957, 58bitri 275 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
6055, 59orbi12i 915 . . . . . . . . 9 ((⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6153, 60bitri 275 . . . . . . . 8 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6252, 61sylibr 234 . . . . . . 7 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6362adantl 481 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
64 eleq1 2829 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6564adantr 480 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6663, 65mpbird 257 . . . . 5 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6766exlimivv 1932 . . . 4 (∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
687, 67syl 17 . . 3 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6968ssriv 3987 . 2 ({∅, 1o} × (𝐴𝐵)) ⊆ ((𝐴𝐵) ∪ (𝐵𝐴))
706, 69eqssi 4000 1 ((𝐴𝐵) ∪ (𝐵𝐴)) = ({∅, 1o} × (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wex 1779  wcel 2108  cun 3949  c0 4333  {csn 4626  {cpr 4628  cop 4632   × cxp 5683  1oc1o 8499  cdju 9938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-suc 6390  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014  df-2nd 8015  df-1o 8506  df-dju 9941  df-inl 9942  df-inr 9943
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator