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

Theorem djuunxp 9990
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 9989 . . 3 (𝐴𝐵) ⊆ ({∅, 1o} × (𝐴𝐵))
2 djuss 9989 . . . 4 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐵𝐴))
3 uncom 4181 . . . . 5 (𝐴𝐵) = (𝐵𝐴)
43xpeq2i 5727 . . . 4 ({∅, 1o} × (𝐴𝐵)) = ({∅, 1o} × (𝐵𝐴))
52, 4sseqtrri 4046 . . 3 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐴𝐵))
61, 5unssi 4214 . 2 ((𝐴𝐵) ∪ (𝐵𝐴)) ⊆ ({∅, 1o} × (𝐴𝐵))
7 elxpi 5722 . . . 4 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → ∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))))
8 vex 3492 . . . . . . . . . 10 𝑦 ∈ V
98elpr 4672 . . . . . . . . 9 (𝑦 ∈ {∅, 1o} ↔ (𝑦 = ∅ ∨ 𝑦 = 1o))
10 elun 4176 . . . . . . . . 9 (𝑧 ∈ (𝐴𝐵) ↔ (𝑧𝐴𝑧𝐵))
11 velsn 4664 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
1211biimpri 228 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ∅ → 𝑦 ∈ {∅})
1312anim1i 614 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = ∅ ∧ 𝑧𝐴) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1413ancoms 458 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐴𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
15 opelxp 5736 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1614, 15sylibr 234 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴))
1716orcd 872 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
18 elun 4176 . . . . . . . . . . . . . . . 16 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
1917, 18sylibr 234 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
2019orcd 872 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2120ex 412 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2212anim1i 614 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ∅ ∧ 𝑧𝐵) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2322ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
24 opelxp 5736 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2523, 24sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵))
2625orcd 872 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
2726olcd 873 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2827ex 412 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2921, 28jaoi 856 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
3029com12 32 . . . . . . . . . . 11 (𝑦 = ∅ → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
31 velsn 4664 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1o} ↔ 𝑦 = 1o)
3231biimpri 228 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 1o𝑦 ∈ {1o})
3332anim1i 614 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 1o𝑧𝐴) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3433ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
35 opelxp 5736 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3634, 35sylibr 234 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))
3736olcd 873 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
3837olcd 873 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
3938ex 412 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4032anim1i 614 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 1o𝑧𝐵) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4140ancoms 458 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
42 opelxp 5736 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4341, 42sylibr 234 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵))
4443olcd 873 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
4544, 18sylibr 234 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
4645orcd 872 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
4746ex 412 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4839, 47jaoi 856 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4948com12 32 . . . . . . . . . . 11 (𝑦 = 1o → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5030, 49jaoi 856 . . . . . . . . . 10 ((𝑦 = ∅ ∨ 𝑦 = 1o) → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5150imp 406 . . . . . . . . 9 (((𝑦 = ∅ ∨ 𝑦 = 1o) ∧ (𝑧𝐴𝑧𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
529, 10, 51syl2anb 597 . . . . . . . 8 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
53 elun 4176 . . . . . . . . 9 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)))
54 df-dju 9970 . . . . . . . . . . 11 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
5554eleq2i 2836 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
56 df-dju 9970 . . . . . . . . . . . 12 (𝐵𝐴) = (({∅} × 𝐵) ∪ ({1o} × 𝐴))
5756eleq2i 2836 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)))
58 elun 4176 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
5957, 58bitri 275 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
6055, 59orbi12i 913 . . . . . . . . 9 ((⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6153, 60bitri 275 . . . . . . . 8 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6252, 61sylibr 234 . . . . . . 7 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6362adantl 481 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
64 eleq1 2832 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6564adantr 480 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6663, 65mpbird 257 . . . . 5 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6766exlimivv 1931 . . . 4 (∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
687, 67syl 17 . . 3 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6968ssriv 4012 . 2 ({∅, 1o} × (𝐴𝐵)) ⊆ ((𝐴𝐵) ∪ (𝐵𝐴))
706, 69eqssi 4025 1 ((𝐴𝐵) ∪ (𝐵𝐴)) = ({∅, 1o} × (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 846   = wceq 1537  wex 1777  wcel 2108  cun 3974  c0 4352  {csn 4648  {cpr 4650  cop 4654   × cxp 5698  1oc1o 8515  cdju 9967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-suc 6401  df-iota 6525  df-fun 6575  df-fv 6581  df-1st 8030  df-2nd 8031  df-1o 8522  df-dju 9970  df-inl 9971  df-inr 9972
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator