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

Theorem djuun 9087
Description: The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.)
Assertion
Ref Expression
djuun ((inl “ 𝐴) ∪ (inr “ 𝐵)) = (𝐴𝐵)

Proof of Theorem djuun
Dummy variables 𝑥 𝑦 𝑢 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elun 3976 . . . 4 (𝑥 ∈ ((inl “ 𝐴) ∪ (inr “ 𝐵)) ↔ (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
2 djulf1o 9073 . . . . . . . . . . 11 inl:V–1-1-onto→({∅} × V)
3 f1ofn 6394 . . . . . . . . . . 11 (inl:V–1-1-onto→({∅} × V) → inl Fn V)
42, 3ax-mp 5 . . . . . . . . . 10 inl Fn V
5 ssv 3844 . . . . . . . . . 10 𝐴 ⊆ V
6 fvelimab 6515 . . . . . . . . . 10 ((inl Fn V ∧ 𝐴 ⊆ V) → (𝑥 ∈ (inl “ 𝐴) ↔ ∃𝑢𝐴 (inl‘𝑢) = 𝑥))
74, 5, 6mp2an 682 . . . . . . . . 9 (𝑥 ∈ (inl “ 𝐴) ↔ ∃𝑢𝐴 (inl‘𝑢) = 𝑥)
87biimpi 208 . . . . . . . 8 (𝑥 ∈ (inl “ 𝐴) → ∃𝑢𝐴 (inl‘𝑢) = 𝑥)
9 simprr 763 . . . . . . . . 9 ((𝑥 ∈ (inl “ 𝐴) ∧ (𝑢𝐴 ∧ (inl‘𝑢) = 𝑥)) → (inl‘𝑢) = 𝑥)
10 vex 3401 . . . . . . . . . . 11 𝑢 ∈ V
11 opex 5166 . . . . . . . . . . 11 ⟨∅, 𝑢⟩ ∈ V
12 opeq2 4639 . . . . . . . . . . . 12 (𝑧 = 𝑢 → ⟨∅, 𝑧⟩ = ⟨∅, 𝑢⟩)
13 df-inl 9064 . . . . . . . . . . . 12 inl = (𝑧 ∈ V ↦ ⟨∅, 𝑧⟩)
1412, 13fvmptg 6542 . . . . . . . . . . 11 ((𝑢 ∈ V ∧ ⟨∅, 𝑢⟩ ∈ V) → (inl‘𝑢) = ⟨∅, 𝑢⟩)
1510, 11, 14mp2an 682 . . . . . . . . . 10 (inl‘𝑢) = ⟨∅, 𝑢
16 0ex 5028 . . . . . . . . . . . . 13 ∅ ∈ V
1716snid 4430 . . . . . . . . . . . 12 ∅ ∈ {∅}
18 opelxpi 5394 . . . . . . . . . . . 12 ((∅ ∈ {∅} ∧ 𝑢𝐴) → ⟨∅, 𝑢⟩ ∈ ({∅} × 𝐴))
1917, 18mpan 680 . . . . . . . . . . 11 (𝑢𝐴 → ⟨∅, 𝑢⟩ ∈ ({∅} × 𝐴))
2019ad2antrl 718 . . . . . . . . . 10 ((𝑥 ∈ (inl “ 𝐴) ∧ (𝑢𝐴 ∧ (inl‘𝑢) = 𝑥)) → ⟨∅, 𝑢⟩ ∈ ({∅} × 𝐴))
2115, 20syl5eqel 2863 . . . . . . . . 9 ((𝑥 ∈ (inl “ 𝐴) ∧ (𝑢𝐴 ∧ (inl‘𝑢) = 𝑥)) → (inl‘𝑢) ∈ ({∅} × 𝐴))
229, 21eqeltrrd 2860 . . . . . . . 8 ((𝑥 ∈ (inl “ 𝐴) ∧ (𝑢𝐴 ∧ (inl‘𝑢) = 𝑥)) → 𝑥 ∈ ({∅} × 𝐴))
238, 22rexlimddv 3218 . . . . . . 7 (𝑥 ∈ (inl “ 𝐴) → 𝑥 ∈ ({∅} × 𝐴))
24 elun1 4003 . . . . . . 7 (𝑥 ∈ ({∅} × 𝐴) → 𝑥 ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
2523, 24syl 17 . . . . . 6 (𝑥 ∈ (inl “ 𝐴) → 𝑥 ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
26 df-dju 9063 . . . . . 6 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
2725, 26syl6eleqr 2870 . . . . 5 (𝑥 ∈ (inl “ 𝐴) → 𝑥 ∈ (𝐴𝐵))
28 djurf1o 9074 . . . . . . . . . . 11 inr:V–1-1-onto→({1o} × V)
29 f1ofn 6394 . . . . . . . . . . 11 (inr:V–1-1-onto→({1o} × V) → inr Fn V)
3028, 29ax-mp 5 . . . . . . . . . 10 inr Fn V
31 ssv 3844 . . . . . . . . . 10 𝐵 ⊆ V
32 fvelimab 6515 . . . . . . . . . 10 ((inr Fn V ∧ 𝐵 ⊆ V) → (𝑥 ∈ (inr “ 𝐵) ↔ ∃𝑢𝐵 (inr‘𝑢) = 𝑥))
3330, 31, 32mp2an 682 . . . . . . . . 9 (𝑥 ∈ (inr “ 𝐵) ↔ ∃𝑢𝐵 (inr‘𝑢) = 𝑥)
3433biimpi 208 . . . . . . . 8 (𝑥 ∈ (inr “ 𝐵) → ∃𝑢𝐵 (inr‘𝑢) = 𝑥)
35 simprr 763 . . . . . . . . 9 ((𝑥 ∈ (inr “ 𝐵) ∧ (𝑢𝐵 ∧ (inr‘𝑢) = 𝑥)) → (inr‘𝑢) = 𝑥)
36 opex 5166 . . . . . . . . . . 11 ⟨1o, 𝑢⟩ ∈ V
37 opeq2 4639 . . . . . . . . . . . 12 (𝑧 = 𝑢 → ⟨1o, 𝑧⟩ = ⟨1o, 𝑢⟩)
38 df-inr 9065 . . . . . . . . . . . 12 inr = (𝑧 ∈ V ↦ ⟨1o, 𝑧⟩)
3937, 38fvmptg 6542 . . . . . . . . . . 11 ((𝑢 ∈ V ∧ ⟨1o, 𝑢⟩ ∈ V) → (inr‘𝑢) = ⟨1o, 𝑢⟩)
4010, 36, 39mp2an 682 . . . . . . . . . 10 (inr‘𝑢) = ⟨1o, 𝑢
41 1oex 7853 . . . . . . . . . . . . 13 1o ∈ V
4241snid 4430 . . . . . . . . . . . 12 1o ∈ {1o}
43 opelxpi 5394 . . . . . . . . . . . 12 ((1o ∈ {1o} ∧ 𝑢𝐵) → ⟨1o, 𝑢⟩ ∈ ({1o} × 𝐵))
4442, 43mpan 680 . . . . . . . . . . 11 (𝑢𝐵 → ⟨1o, 𝑢⟩ ∈ ({1o} × 𝐵))
4544ad2antrl 718 . . . . . . . . . 10 ((𝑥 ∈ (inr “ 𝐵) ∧ (𝑢𝐵 ∧ (inr‘𝑢) = 𝑥)) → ⟨1o, 𝑢⟩ ∈ ({1o} × 𝐵))
4640, 45syl5eqel 2863 . . . . . . . . 9 ((𝑥 ∈ (inr “ 𝐵) ∧ (𝑢𝐵 ∧ (inr‘𝑢) = 𝑥)) → (inr‘𝑢) ∈ ({1o} × 𝐵))
4735, 46eqeltrrd 2860 . . . . . . . 8 ((𝑥 ∈ (inr “ 𝐵) ∧ (𝑢𝐵 ∧ (inr‘𝑢) = 𝑥)) → 𝑥 ∈ ({1o} × 𝐵))
4834, 47rexlimddv 3218 . . . . . . 7 (𝑥 ∈ (inr “ 𝐵) → 𝑥 ∈ ({1o} × 𝐵))
49 elun2 4004 . . . . . . 7 (𝑥 ∈ ({1o} × 𝐵) → 𝑥 ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
5048, 49syl 17 . . . . . 6 (𝑥 ∈ (inr “ 𝐵) → 𝑥 ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
5150, 26syl6eleqr 2870 . . . . 5 (𝑥 ∈ (inr “ 𝐵) → 𝑥 ∈ (𝐴𝐵))
5227, 51jaoi 846 . . . 4 ((𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)) → 𝑥 ∈ (𝐴𝐵))
531, 52sylbi 209 . . 3 (𝑥 ∈ ((inl “ 𝐴) ∪ (inr “ 𝐵)) → 𝑥 ∈ (𝐴𝐵))
5453ssriv 3825 . 2 ((inl “ 𝐴) ∪ (inr “ 𝐵)) ⊆ (𝐴𝐵)
55 djur 9080 . . . . 5 (𝑥 ∈ (𝐴𝐵) → (∃𝑦𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦𝐵 𝑥 = (inr‘𝑦)))
56 vex 3401 . . . . . . . . . 10 𝑦 ∈ V
57 f1odm 6397 . . . . . . . . . . 11 (inl:V–1-1-onto→({∅} × V) → dom inl = V)
582, 57ax-mp 5 . . . . . . . . . 10 dom inl = V
5956, 58eleqtrri 2858 . . . . . . . . 9 𝑦 ∈ dom inl
60 simpl 476 . . . . . . . . 9 ((𝑦𝐴𝑥 = (inl‘𝑦)) → 𝑦𝐴)
6113funmpt2 6176 . . . . . . . . . 10 Fun inl
62 funfvima 6766 . . . . . . . . . 10 ((Fun inl ∧ 𝑦 ∈ dom inl) → (𝑦𝐴 → (inl‘𝑦) ∈ (inl “ 𝐴)))
6361, 62mpan 680 . . . . . . . . 9 (𝑦 ∈ dom inl → (𝑦𝐴 → (inl‘𝑦) ∈ (inl “ 𝐴)))
6459, 60, 63mpsyl 68 . . . . . . . 8 ((𝑦𝐴𝑥 = (inl‘𝑦)) → (inl‘𝑦) ∈ (inl “ 𝐴))
65 eleq1 2847 . . . . . . . . 9 (𝑥 = (inl‘𝑦) → (𝑥 ∈ (inl “ 𝐴) ↔ (inl‘𝑦) ∈ (inl “ 𝐴)))
6665adantl 475 . . . . . . . 8 ((𝑦𝐴𝑥 = (inl‘𝑦)) → (𝑥 ∈ (inl “ 𝐴) ↔ (inl‘𝑦) ∈ (inl “ 𝐴)))
6764, 66mpbird 249 . . . . . . 7 ((𝑦𝐴𝑥 = (inl‘𝑦)) → 𝑥 ∈ (inl “ 𝐴))
6867rexlimiva 3210 . . . . . 6 (∃𝑦𝐴 𝑥 = (inl‘𝑦) → 𝑥 ∈ (inl “ 𝐴))
69 f1odm 6397 . . . . . . . . . . 11 (inr:V–1-1-onto→({1o} × V) → dom inr = V)
7028, 69ax-mp 5 . . . . . . . . . 10 dom inr = V
7156, 70eleqtrri 2858 . . . . . . . . 9 𝑦 ∈ dom inr
72 simpl 476 . . . . . . . . 9 ((𝑦𝐵𝑥 = (inr‘𝑦)) → 𝑦𝐵)
73 f1ofun 6395 . . . . . . . . . . 11 (inr:V–1-1-onto→({1o} × V) → Fun inr)
7428, 73ax-mp 5 . . . . . . . . . 10 Fun inr
75 funfvima 6766 . . . . . . . . . 10 ((Fun inr ∧ 𝑦 ∈ dom inr) → (𝑦𝐵 → (inr‘𝑦) ∈ (inr “ 𝐵)))
7674, 75mpan 680 . . . . . . . . 9 (𝑦 ∈ dom inr → (𝑦𝐵 → (inr‘𝑦) ∈ (inr “ 𝐵)))
7771, 72, 76mpsyl 68 . . . . . . . 8 ((𝑦𝐵𝑥 = (inr‘𝑦)) → (inr‘𝑦) ∈ (inr “ 𝐵))
78 eleq1 2847 . . . . . . . . 9 (𝑥 = (inr‘𝑦) → (𝑥 ∈ (inr “ 𝐵) ↔ (inr‘𝑦) ∈ (inr “ 𝐵)))
7978adantl 475 . . . . . . . 8 ((𝑦𝐵𝑥 = (inr‘𝑦)) → (𝑥 ∈ (inr “ 𝐵) ↔ (inr‘𝑦) ∈ (inr “ 𝐵)))
8077, 79mpbird 249 . . . . . . 7 ((𝑦𝐵𝑥 = (inr‘𝑦)) → 𝑥 ∈ (inr “ 𝐵))
8180rexlimiva 3210 . . . . . 6 (∃𝑦𝐵 𝑥 = (inr‘𝑦) → 𝑥 ∈ (inr “ 𝐵))
8268, 81orim12i 895 . . . . 5 ((∃𝑦𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦𝐵 𝑥 = (inr‘𝑦)) → (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
8355, 82syl 17 . . . 4 (𝑥 ∈ (𝐴𝐵) → (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
8483, 1sylibr 226 . . 3 (𝑥 ∈ (𝐴𝐵) → 𝑥 ∈ ((inl “ 𝐴) ∪ (inr “ 𝐵)))
8584ssriv 3825 . 2 (𝐴𝐵) ⊆ ((inl “ 𝐴) ∪ (inr “ 𝐵))
8654, 85eqssi 3837 1 ((inl “ 𝐴) ∪ (inr “ 𝐵)) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wo 836   = wceq 1601  wcel 2107  wrex 3091  Vcvv 3398  cun 3790  wss 3792  c0 4141  {csn 4398  cop 4404   × cxp 5355  dom cdm 5357  cima 5360  Fun wfun 6131   Fn wfn 6132  1-1-ontowf1o 6136  cfv 6137  1oc1o 7838  cdju 9060  inlcinl 9061  inrcinr 9062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-om 7346  df-1st 7447  df-2nd 7448  df-1o 7845  df-dju 9063  df-inl 9064  df-inr 9065
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator