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

Theorem djuunxp 9959
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 9958 . . 3 (𝐴𝐵) ⊆ ({∅, 1o} × (𝐴𝐵))
2 djuss 9958 . . . 4 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐵𝐴))
3 uncom 4168 . . . . 5 (𝐴𝐵) = (𝐵𝐴)
43xpeq2i 5716 . . . 4 ({∅, 1o} × (𝐴𝐵)) = ({∅, 1o} × (𝐵𝐴))
52, 4sseqtrri 4033 . . 3 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐴𝐵))
61, 5unssi 4201 . 2 ((𝐴𝐵) ∪ (𝐵𝐴)) ⊆ ({∅, 1o} × (𝐴𝐵))
7 elxpi 5711 . . . 4 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → ∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))))
8 vex 3482 . . . . . . . . . 10 𝑦 ∈ V
98elpr 4655 . . . . . . . . 9 (𝑦 ∈ {∅, 1o} ↔ (𝑦 = ∅ ∨ 𝑦 = 1o))
10 elun 4163 . . . . . . . . 9 (𝑧 ∈ (𝐴𝐵) ↔ (𝑧𝐴𝑧𝐵))
11 velsn 4647 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
1211biimpri 228 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ∅ → 𝑦 ∈ {∅})
1312anim1i 615 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = ∅ ∧ 𝑧𝐴) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1413ancoms 458 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐴𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
15 opelxp 5725 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1614, 15sylibr 234 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴))
1716orcd 873 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
18 elun 4163 . . . . . . . . . . . . . . . 16 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
1917, 18sylibr 234 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
2019orcd 873 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2120ex 412 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2212anim1i 615 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ∅ ∧ 𝑧𝐵) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2322ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
24 opelxp 5725 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2523, 24sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵))
2625orcd 873 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
2726olcd 874 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2827ex 412 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2921, 28jaoi 857 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
3029com12 32 . . . . . . . . . . 11 (𝑦 = ∅ → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
31 velsn 4647 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1o} ↔ 𝑦 = 1o)
3231biimpri 228 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 1o𝑦 ∈ {1o})
3332anim1i 615 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 1o𝑧𝐴) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3433ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
35 opelxp 5725 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3634, 35sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))
3736olcd 874 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
3837olcd 874 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
3938ex 412 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4032anim1i 615 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 1o𝑧𝐵) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4140ancoms 458 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
42 opelxp 5725 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4341, 42sylibr 234 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵))
4443olcd 874 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
4544, 18sylibr 234 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
4645orcd 873 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
4746ex 412 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4839, 47jaoi 857 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4948com12 32 . . . . . . . . . . 11 (𝑦 = 1o → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5030, 49jaoi 857 . . . . . . . . . 10 ((𝑦 = ∅ ∨ 𝑦 = 1o) → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5150imp 406 . . . . . . . . 9 (((𝑦 = ∅ ∨ 𝑦 = 1o) ∧ (𝑧𝐴𝑧𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
529, 10, 51syl2anb 598 . . . . . . . 8 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
53 elun 4163 . . . . . . . . 9 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)))
54 df-dju 9939 . . . . . . . . . . 11 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
5554eleq2i 2831 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
56 df-dju 9939 . . . . . . . . . . . 12 (𝐵𝐴) = (({∅} × 𝐵) ∪ ({1o} × 𝐴))
5756eleq2i 2831 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)))
58 elun 4163 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
5957, 58bitri 275 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
6055, 59orbi12i 914 . . . . . . . . 9 ((⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6153, 60bitri 275 . . . . . . . 8 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6252, 61sylibr 234 . . . . . . 7 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6362adantl 481 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
64 eleq1 2827 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6564adantr 480 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6663, 65mpbird 257 . . . . 5 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6766exlimivv 1930 . . . 4 (∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
687, 67syl 17 . . 3 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6968ssriv 3999 . 2 ({∅, 1o} × (𝐴𝐵)) ⊆ ((𝐴𝐵) ∪ (𝐵𝐴))
706, 69eqssi 4012 1 ((𝐴𝐵) ∪ (𝐵𝐴)) = ({∅, 1o} × (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847   = wceq 1537  wex 1776  wcel 2106  cun 3961  c0 4339  {csn 4631  {cpr 4633  cop 4637   × cxp 5687  1oc1o 8498  cdju 9936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-suc 6392  df-iota 6516  df-fun 6565  df-fv 6571  df-1st 8013  df-2nd 8014  df-1o 8505  df-dju 9939  df-inl 9940  df-inr 9941
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator