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

Theorem djuunxp 9915
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 9914 . . 3 (𝐴𝐵) ⊆ ({∅, 1o} × (𝐴𝐵))
2 djuss 9914 . . . 4 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐵𝐴))
3 uncom 4148 . . . . 5 (𝐴𝐵) = (𝐵𝐴)
43xpeq2i 5696 . . . 4 ({∅, 1o} × (𝐴𝐵)) = ({∅, 1o} × (𝐵𝐴))
52, 4sseqtrri 4014 . . 3 (𝐵𝐴) ⊆ ({∅, 1o} × (𝐴𝐵))
61, 5unssi 4180 . 2 ((𝐴𝐵) ∪ (𝐵𝐴)) ⊆ ({∅, 1o} × (𝐴𝐵))
7 elxpi 5691 . . . 4 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → ∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))))
8 vex 3472 . . . . . . . . . 10 𝑦 ∈ V
98elpr 4646 . . . . . . . . 9 (𝑦 ∈ {∅, 1o} ↔ (𝑦 = ∅ ∨ 𝑦 = 1o))
10 elun 4143 . . . . . . . . 9 (𝑧 ∈ (𝐴𝐵) ↔ (𝑧𝐴𝑧𝐵))
11 velsn 4639 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
1211biimpri 227 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ∅ → 𝑦 ∈ {∅})
1312anim1i 614 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = ∅ ∧ 𝑧𝐴) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1413ancoms 458 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐴𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐴))
15 opelxp 5705 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐴))
1614, 15sylibr 233 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴))
1716orcd 870 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
18 elun 4143 . . . . . . . . . . . . . . . 16 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
1917, 18sylibr 233 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
2019orcd 870 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2120ex 412 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2212anim1i 614 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ∅ ∧ 𝑧𝐵) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2322ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = ∅) → (𝑦 ∈ {∅} ∧ 𝑧𝐵))
24 opelxp 5705 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ↔ (𝑦 ∈ {∅} ∧ 𝑧𝐵))
2523, 24sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = ∅) → ⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵))
2625orcd 870 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
2726olcd 871 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = ∅) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
2827ex 412 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
2921, 28jaoi 854 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = ∅ → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
3029com12 32 . . . . . . . . . . 11 (𝑦 = ∅ → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
31 velsn 4639 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1o} ↔ 𝑦 = 1o)
3231biimpri 227 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 1o𝑦 ∈ {1o})
3332anim1i 614 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 1o𝑧𝐴) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3433ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐴))
35 opelxp 5705 . . . . . . . . . . . . . . . . 17 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐴))
3634, 35sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑧𝐴𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))
3736olcd 871 . . . . . . . . . . . . . . 15 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
3837olcd 871 . . . . . . . . . . . . . 14 ((𝑧𝐴𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
3938ex 412 . . . . . . . . . . . . 13 (𝑧𝐴 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4032anim1i 614 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 1o𝑧𝐵) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4140ancoms 458 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑦 = 1o) → (𝑦 ∈ {1o} ∧ 𝑧𝐵))
42 opelxp 5705 . . . . . . . . . . . . . . . . . 18 (⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵) ↔ (𝑦 ∈ {1o} ∧ 𝑧𝐵))
4341, 42sylibr 233 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵))
4443olcd 871 . . . . . . . . . . . . . . . 16 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐴) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐵)))
4544, 18sylibr 233 . . . . . . . . . . . . . . 15 ((𝑧𝐵𝑦 = 1o) → ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
4645orcd 870 . . . . . . . . . . . . . 14 ((𝑧𝐵𝑦 = 1o) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
4746ex 412 . . . . . . . . . . . . 13 (𝑧𝐵 → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4839, 47jaoi 854 . . . . . . . . . . . 12 ((𝑧𝐴𝑧𝐵) → (𝑦 = 1o → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
4948com12 32 . . . . . . . . . . 11 (𝑦 = 1o → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5030, 49jaoi 854 . . . . . . . . . 10 ((𝑦 = ∅ ∨ 𝑦 = 1o) → ((𝑧𝐴𝑧𝐵) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))))
5150imp 406 . . . . . . . . 9 (((𝑦 = ∅ ∨ 𝑦 = 1o) ∧ (𝑧𝐴𝑧𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
529, 10, 51syl2anb 597 . . . . . . . 8 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
53 elun 4143 . . . . . . . . 9 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)))
54 df-dju 9895 . . . . . . . . . . 11 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
5554eleq2i 2819 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
56 df-dju 9895 . . . . . . . . . . . 12 (𝐵𝐴) = (({∅} × 𝐵) ∪ ({1o} × 𝐴))
5756eleq2i 2819 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)))
58 elun 4143 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐵) ∪ ({1o} × 𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
5957, 58bitri 275 . . . . . . . . . 10 (⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴) ↔ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴)))
6055, 59orbi12i 911 . . . . . . . . 9 ((⟨𝑦, 𝑧⟩ ∈ (𝐴𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6153, 60bitri 275 . . . . . . . 8 (⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ (⟨𝑦, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ∨ (⟨𝑦, 𝑧⟩ ∈ ({∅} × 𝐵) ∨ ⟨𝑦, 𝑧⟩ ∈ ({1o} × 𝐴))))
6252, 61sylibr 233 . . . . . . 7 ((𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵)) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6362adantl 481 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
64 eleq1 2815 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6564adantr 480 . . . . . 6 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → (𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)) ↔ ⟨𝑦, 𝑧⟩ ∈ ((𝐴𝐵) ∪ (𝐵𝐴))))
6663, 65mpbird 257 . . . . 5 ((𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6766exlimivv 1927 . . . 4 (∃𝑦𝑧(𝑥 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ {∅, 1o} ∧ 𝑧 ∈ (𝐴𝐵))) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
687, 67syl 17 . . 3 (𝑥 ∈ ({∅, 1o} × (𝐴𝐵)) → 𝑥 ∈ ((𝐴𝐵) ∪ (𝐵𝐴)))
6968ssriv 3981 . 2 ({∅, 1o} × (𝐴𝐵)) ⊆ ((𝐴𝐵) ∪ (𝐵𝐴))
706, 69eqssi 3993 1 ((𝐴𝐵) ∪ (𝐵𝐴)) = ({∅, 1o} × (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wo 844   = wceq 1533  wex 1773  wcel 2098  cun 3941  c0 4317  {csn 4623  {cpr 4625  cop 4629   × cxp 5667  1oc1o 8457  cdju 9892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-suc 6363  df-iota 6488  df-fun 6538  df-fv 6544  df-1st 7971  df-2nd 7972  df-1o 8464  df-dju 9895  df-inl 9896  df-inr 9897
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator