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

Theorem djuun 8952
 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 3904 . . . 4 (𝑥 ∈ ((inl “ 𝐴) ∪ (inr “ 𝐵)) ↔ (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
2 djulf1o 8938 . . . . . . . . . . 11 inl:V–1-1-onto→({∅} × V)
3 f1ofn 6279 . . . . . . . . . . 11 (inl:V–1-1-onto→({∅} × V) → inl Fn V)
42, 3ax-mp 5 . . . . . . . . . 10 inl Fn V
5 ssv 3774 . . . . . . . . . 10 𝐴 ⊆ V
6 fvelimab 6395 . . . . . . . . . 10 ((inl Fn V ∧ 𝐴 ⊆ V) → (𝑥 ∈ (inl “ 𝐴) ↔ ∃𝑢𝐴 (inl‘𝑢) = 𝑥))
74, 5, 6mp2an 672 . . . . . . . . 9 (𝑥 ∈ (inl “ 𝐴) ↔ ∃𝑢𝐴 (inl‘𝑢) = 𝑥)
87biimpi 206 . . . . . . . 8 (𝑥 ∈ (inl “ 𝐴) → ∃𝑢𝐴 (inl‘𝑢) = 𝑥)
9 simprr 756 . . . . . . . . 9 ((𝑥 ∈ (inl “ 𝐴) ∧ (𝑢𝐴 ∧ (inl‘𝑢) = 𝑥)) → (inl‘𝑢) = 𝑥)
10 vex 3354 . . . . . . . . . . 11 𝑢 ∈ V
11 opex 5060 . . . . . . . . . . 11 ⟨∅, 𝑢⟩ ∈ V
12 opeq2 4540 . . . . . . . . . . . 12 (𝑧 = 𝑢 → ⟨∅, 𝑧⟩ = ⟨∅, 𝑢⟩)
13 df-inl 8929 . . . . . . . . . . . 12 inl = (𝑧 ∈ V ↦ ⟨∅, 𝑧⟩)
1412, 13fvmptg 6422 . . . . . . . . . . 11 ((𝑢 ∈ V ∧ ⟨∅, 𝑢⟩ ∈ V) → (inl‘𝑢) = ⟨∅, 𝑢⟩)
1510, 11, 14mp2an 672 . . . . . . . . . 10 (inl‘𝑢) = ⟨∅, 𝑢
16 0ex 4924 . . . . . . . . . . . . 13 ∅ ∈ V
1716snid 4347 . . . . . . . . . . . 12 ∅ ∈ {∅}
18 opelxpi 5288 . . . . . . . . . . . 12 ((∅ ∈ {∅} ∧ 𝑢𝐴) → ⟨∅, 𝑢⟩ ∈ ({∅} × 𝐴))
1917, 18mpan 670 . . . . . . . . . . 11 (𝑢𝐴 → ⟨∅, 𝑢⟩ ∈ ({∅} × 𝐴))
2019ad2antrl 707 . . . . . . . . . 10 ((𝑥 ∈ (inl “ 𝐴) ∧ (𝑢𝐴 ∧ (inl‘𝑢) = 𝑥)) → ⟨∅, 𝑢⟩ ∈ ({∅} × 𝐴))
2115, 20syl5eqel 2854 . . . . . . . . 9 ((𝑥 ∈ (inl “ 𝐴) ∧ (𝑢𝐴 ∧ (inl‘𝑢) = 𝑥)) → (inl‘𝑢) ∈ ({∅} × 𝐴))
229, 21eqeltrrd 2851 . . . . . . . 8 ((𝑥 ∈ (inl “ 𝐴) ∧ (𝑢𝐴 ∧ (inl‘𝑢) = 𝑥)) → 𝑥 ∈ ({∅} × 𝐴))
238, 22rexlimddv 3183 . . . . . . 7 (𝑥 ∈ (inl “ 𝐴) → 𝑥 ∈ ({∅} × 𝐴))
24 elun1 3931 . . . . . . 7 (𝑥 ∈ ({∅} × 𝐴) → 𝑥 ∈ (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵)))
2523, 24syl 17 . . . . . 6 (𝑥 ∈ (inl “ 𝐴) → 𝑥 ∈ (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵)))
26 df-dju 8928 . . . . . 6 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))
2725, 26syl6eleqr 2861 . . . . 5 (𝑥 ∈ (inl “ 𝐴) → 𝑥 ∈ (𝐴𝐵))
28 djurf1o 8939 . . . . . . . . . . 11 inr:V–1-1-onto→({1𝑜} × V)
29 f1ofn 6279 . . . . . . . . . . 11 (inr:V–1-1-onto→({1𝑜} × V) → inr Fn V)
3028, 29ax-mp 5 . . . . . . . . . 10 inr Fn V
31 ssv 3774 . . . . . . . . . 10 𝐵 ⊆ V
32 fvelimab 6395 . . . . . . . . . 10 ((inr Fn V ∧ 𝐵 ⊆ V) → (𝑥 ∈ (inr “ 𝐵) ↔ ∃𝑢𝐵 (inr‘𝑢) = 𝑥))
3330, 31, 32mp2an 672 . . . . . . . . 9 (𝑥 ∈ (inr “ 𝐵) ↔ ∃𝑢𝐵 (inr‘𝑢) = 𝑥)
3433biimpi 206 . . . . . . . 8 (𝑥 ∈ (inr “ 𝐵) → ∃𝑢𝐵 (inr‘𝑢) = 𝑥)
35 simprr 756 . . . . . . . . 9 ((𝑥 ∈ (inr “ 𝐵) ∧ (𝑢𝐵 ∧ (inr‘𝑢) = 𝑥)) → (inr‘𝑢) = 𝑥)
36 opex 5060 . . . . . . . . . . 11 ⟨1𝑜, 𝑢⟩ ∈ V
37 opeq2 4540 . . . . . . . . . . . 12 (𝑧 = 𝑢 → ⟨1𝑜, 𝑧⟩ = ⟨1𝑜, 𝑢⟩)
38 df-inr 8930 . . . . . . . . . . . 12 inr = (𝑧 ∈ V ↦ ⟨1𝑜, 𝑧⟩)
3937, 38fvmptg 6422 . . . . . . . . . . 11 ((𝑢 ∈ V ∧ ⟨1𝑜, 𝑢⟩ ∈ V) → (inr‘𝑢) = ⟨1𝑜, 𝑢⟩)
4010, 36, 39mp2an 672 . . . . . . . . . 10 (inr‘𝑢) = ⟨1𝑜, 𝑢
41 1onn 7873 . . . . . . . . . . . . . 14 1𝑜 ∈ ω
4241elexi 3365 . . . . . . . . . . . . 13 1𝑜 ∈ V
4342snid 4347 . . . . . . . . . . . 12 1𝑜 ∈ {1𝑜}
44 opelxpi 5288 . . . . . . . . . . . 12 ((1𝑜 ∈ {1𝑜} ∧ 𝑢𝐵) → ⟨1𝑜, 𝑢⟩ ∈ ({1𝑜} × 𝐵))
4543, 44mpan 670 . . . . . . . . . . 11 (𝑢𝐵 → ⟨1𝑜, 𝑢⟩ ∈ ({1𝑜} × 𝐵))
4645ad2antrl 707 . . . . . . . . . 10 ((𝑥 ∈ (inr “ 𝐵) ∧ (𝑢𝐵 ∧ (inr‘𝑢) = 𝑥)) → ⟨1𝑜, 𝑢⟩ ∈ ({1𝑜} × 𝐵))
4740, 46syl5eqel 2854 . . . . . . . . 9 ((𝑥 ∈ (inr “ 𝐵) ∧ (𝑢𝐵 ∧ (inr‘𝑢) = 𝑥)) → (inr‘𝑢) ∈ ({1𝑜} × 𝐵))
4835, 47eqeltrrd 2851 . . . . . . . 8 ((𝑥 ∈ (inr “ 𝐵) ∧ (𝑢𝐵 ∧ (inr‘𝑢) = 𝑥)) → 𝑥 ∈ ({1𝑜} × 𝐵))
4934, 48rexlimddv 3183 . . . . . . 7 (𝑥 ∈ (inr “ 𝐵) → 𝑥 ∈ ({1𝑜} × 𝐵))
50 elun2 3932 . . . . . . 7 (𝑥 ∈ ({1𝑜} × 𝐵) → 𝑥 ∈ (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵)))
5149, 50syl 17 . . . . . 6 (𝑥 ∈ (inr “ 𝐵) → 𝑥 ∈ (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵)))
5251, 26syl6eleqr 2861 . . . . 5 (𝑥 ∈ (inr “ 𝐵) → 𝑥 ∈ (𝐴𝐵))
5327, 52jaoi 846 . . . 4 ((𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)) → 𝑥 ∈ (𝐴𝐵))
541, 53sylbi 207 . . 3 (𝑥 ∈ ((inl “ 𝐴) ∪ (inr “ 𝐵)) → 𝑥 ∈ (𝐴𝐵))
5554ssriv 3756 . 2 ((inl “ 𝐴) ∪ (inr “ 𝐵)) ⊆ (𝐴𝐵)
56 djur 8945 . . . . 5 (𝑥 ∈ (𝐴𝐵) → (∃𝑦𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦𝐵 𝑥 = (inr‘𝑦)))
57 vex 3354 . . . . . . . . . 10 𝑦 ∈ V
58 f1odm 6282 . . . . . . . . . . 11 (inl:V–1-1-onto→({∅} × V) → dom inl = V)
592, 58ax-mp 5 . . . . . . . . . 10 dom inl = V
6057, 59eleqtrri 2849 . . . . . . . . 9 𝑦 ∈ dom inl
61 simpl 468 . . . . . . . . 9 ((𝑦𝐴𝑥 = (inl‘𝑦)) → 𝑦𝐴)
6213funmpt2 6070 . . . . . . . . . 10 Fun inl
63 funfvima 6635 . . . . . . . . . 10 ((Fun inl ∧ 𝑦 ∈ dom inl) → (𝑦𝐴 → (inl‘𝑦) ∈ (inl “ 𝐴)))
6462, 63mpan 670 . . . . . . . . 9 (𝑦 ∈ dom inl → (𝑦𝐴 → (inl‘𝑦) ∈ (inl “ 𝐴)))
6560, 61, 64mpsyl 68 . . . . . . . 8 ((𝑦𝐴𝑥 = (inl‘𝑦)) → (inl‘𝑦) ∈ (inl “ 𝐴))
66 eleq1 2838 . . . . . . . . 9 (𝑥 = (inl‘𝑦) → (𝑥 ∈ (inl “ 𝐴) ↔ (inl‘𝑦) ∈ (inl “ 𝐴)))
6766adantl 467 . . . . . . . 8 ((𝑦𝐴𝑥 = (inl‘𝑦)) → (𝑥 ∈ (inl “ 𝐴) ↔ (inl‘𝑦) ∈ (inl “ 𝐴)))
6865, 67mpbird 247 . . . . . . 7 ((𝑦𝐴𝑥 = (inl‘𝑦)) → 𝑥 ∈ (inl “ 𝐴))
6968rexlimiva 3176 . . . . . 6 (∃𝑦𝐴 𝑥 = (inl‘𝑦) → 𝑥 ∈ (inl “ 𝐴))
70 f1odm 6282 . . . . . . . . . . 11 (inr:V–1-1-onto→({1𝑜} × V) → dom inr = V)
7128, 70ax-mp 5 . . . . . . . . . 10 dom inr = V
7257, 71eleqtrri 2849 . . . . . . . . 9 𝑦 ∈ dom inr
73 simpl 468 . . . . . . . . 9 ((𝑦𝐵𝑥 = (inr‘𝑦)) → 𝑦𝐵)
74 f1ofun 6280 . . . . . . . . . . 11 (inr:V–1-1-onto→({1𝑜} × V) → Fun inr)
7528, 74ax-mp 5 . . . . . . . . . 10 Fun inr
76 funfvima 6635 . . . . . . . . . 10 ((Fun inr ∧ 𝑦 ∈ dom inr) → (𝑦𝐵 → (inr‘𝑦) ∈ (inr “ 𝐵)))
7775, 76mpan 670 . . . . . . . . 9 (𝑦 ∈ dom inr → (𝑦𝐵 → (inr‘𝑦) ∈ (inr “ 𝐵)))
7872, 73, 77mpsyl 68 . . . . . . . 8 ((𝑦𝐵𝑥 = (inr‘𝑦)) → (inr‘𝑦) ∈ (inr “ 𝐵))
79 eleq1 2838 . . . . . . . . 9 (𝑥 = (inr‘𝑦) → (𝑥 ∈ (inr “ 𝐵) ↔ (inr‘𝑦) ∈ (inr “ 𝐵)))
8079adantl 467 . . . . . . . 8 ((𝑦𝐵𝑥 = (inr‘𝑦)) → (𝑥 ∈ (inr “ 𝐵) ↔ (inr‘𝑦) ∈ (inr “ 𝐵)))
8178, 80mpbird 247 . . . . . . 7 ((𝑦𝐵𝑥 = (inr‘𝑦)) → 𝑥 ∈ (inr “ 𝐵))
8281rexlimiva 3176 . . . . . 6 (∃𝑦𝐵 𝑥 = (inr‘𝑦) → 𝑥 ∈ (inr “ 𝐵))
8369, 82orim12i 894 . . . . 5 ((∃𝑦𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦𝐵 𝑥 = (inr‘𝑦)) → (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
8456, 83syl 17 . . . 4 (𝑥 ∈ (𝐴𝐵) → (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
8584, 1sylibr 224 . . 3 (𝑥 ∈ (𝐴𝐵) → 𝑥 ∈ ((inl “ 𝐴) ∪ (inr “ 𝐵)))
8685ssriv 3756 . 2 (𝐴𝐵) ⊆ ((inl “ 𝐴) ∪ (inr “ 𝐵))
8755, 86eqssi 3768 1 ((inl “ 𝐴) ∪ (inr “ 𝐵)) = (𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∨ wo 836   = wceq 1631   ∈ wcel 2145  ∃wrex 3062  Vcvv 3351   ∪ cun 3721   ⊆ wss 3723  ∅c0 4063  {csn 4316  ⟨cop 4322   × cxp 5247  dom cdm 5249   “ cima 5252  Fun wfun 6025   Fn wfn 6026  –1-1-onto→wf1o 6030  ‘cfv 6031  ωcom 7212  1𝑜c1o 7706   ⊔ cdju 8925  inlcinl 8926  inrcinr 8927 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-om 7213  df-1st 7315  df-2nd 7316  df-1o 7713  df-dju 8928  df-inl 8929  df-inr 8930 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator