ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  djuun GIF version

Theorem djuun 6707
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.) (Proof shortened by BJ, 6-Jul-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 df-ima 4426 . . . 4 (inl “ 𝐴) = ran (inl ↾ 𝐴)
2 inlresf1 6700 . . . . 5 (inl ↾ 𝐴):𝐴1-1→(𝐴𝐵)
3 f1rn 5182 . . . . 5 ((inl ↾ 𝐴):𝐴1-1→(𝐴𝐵) → ran (inl ↾ 𝐴) ⊆ (𝐴𝐵))
42, 3ax-mp 7 . . . 4 ran (inl ↾ 𝐴) ⊆ (𝐴𝐵)
51, 4eqsstri 3045 . . 3 (inl “ 𝐴) ⊆ (𝐴𝐵)
6 df-ima 4426 . . . 4 (inr “ 𝐵) = ran (inr ↾ 𝐵)
7 inrresf1 6701 . . . . 5 (inr ↾ 𝐵):𝐵1-1→(𝐴𝐵)
8 f1rn 5182 . . . . 5 ((inr ↾ 𝐵):𝐵1-1→(𝐴𝐵) → ran (inr ↾ 𝐵) ⊆ (𝐴𝐵))
97, 8ax-mp 7 . . . 4 ran (inr ↾ 𝐵) ⊆ (𝐴𝐵)
106, 9eqsstri 3045 . . 3 (inr “ 𝐵) ⊆ (𝐴𝐵)
115, 10unssi 3164 . 2 ((inl “ 𝐴) ∪ (inr “ 𝐵)) ⊆ (𝐴𝐵)
12 djur 6704 . . . . 5 (𝑥 ∈ (𝐴𝐵) → (∃𝑦𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦𝐵 𝑥 = (inr‘𝑦)))
13 vex 2618 . . . . . . . . . 10 𝑦 ∈ V
14 djulf1o 6697 . . . . . . . . . . 11 inl:V–1-1-onto→({∅} × V)
15 f1odm 5222 . . . . . . . . . . 11 (inl:V–1-1-onto→({∅} × V) → dom inl = V)
1614, 15ax-mp 7 . . . . . . . . . 10 dom inl = V
1713, 16eleqtrri 2160 . . . . . . . . 9 𝑦 ∈ dom inl
18 simpl 107 . . . . . . . . 9 ((𝑦𝐴𝑥 = (inl‘𝑦)) → 𝑦𝐴)
19 df-inl 6686 . . . . . . . . . . 11 inl = (𝑧 ∈ V ↦ ⟨∅, 𝑧⟩)
2019funmpt2 5020 . . . . . . . . . 10 Fun inl
21 funfvima 5489 . . . . . . . . . 10 ((Fun inl ∧ 𝑦 ∈ dom inl) → (𝑦𝐴 → (inl‘𝑦) ∈ (inl “ 𝐴)))
2220, 21mpan 415 . . . . . . . . 9 (𝑦 ∈ dom inl → (𝑦𝐴 → (inl‘𝑦) ∈ (inl “ 𝐴)))
2317, 18, 22mpsyl 64 . . . . . . . 8 ((𝑦𝐴𝑥 = (inl‘𝑦)) → (inl‘𝑦) ∈ (inl “ 𝐴))
24 eleq1 2147 . . . . . . . . 9 (𝑥 = (inl‘𝑦) → (𝑥 ∈ (inl “ 𝐴) ↔ (inl‘𝑦) ∈ (inl “ 𝐴)))
2524adantl 271 . . . . . . . 8 ((𝑦𝐴𝑥 = (inl‘𝑦)) → (𝑥 ∈ (inl “ 𝐴) ↔ (inl‘𝑦) ∈ (inl “ 𝐴)))
2623, 25mpbird 165 . . . . . . 7 ((𝑦𝐴𝑥 = (inl‘𝑦)) → 𝑥 ∈ (inl “ 𝐴))
2726rexlimiva 2480 . . . . . 6 (∃𝑦𝐴 𝑥 = (inl‘𝑦) → 𝑥 ∈ (inl “ 𝐴))
28 djurf1o 6698 . . . . . . . . . . 11 inr:V–1-1-onto→({1𝑜} × V)
29 f1odm 5222 . . . . . . . . . . 11 (inr:V–1-1-onto→({1𝑜} × V) → dom inr = V)
3028, 29ax-mp 7 . . . . . . . . . 10 dom inr = V
3113, 30eleqtrri 2160 . . . . . . . . 9 𝑦 ∈ dom inr
32 simpl 107 . . . . . . . . 9 ((𝑦𝐵𝑥 = (inr‘𝑦)) → 𝑦𝐵)
33 f1ofun 5220 . . . . . . . . . . 11 (inr:V–1-1-onto→({1𝑜} × V) → Fun inr)
3428, 33ax-mp 7 . . . . . . . . . 10 Fun inr
35 funfvima 5489 . . . . . . . . . 10 ((Fun inr ∧ 𝑦 ∈ dom inr) → (𝑦𝐵 → (inr‘𝑦) ∈ (inr “ 𝐵)))
3634, 35mpan 415 . . . . . . . . 9 (𝑦 ∈ dom inr → (𝑦𝐵 → (inr‘𝑦) ∈ (inr “ 𝐵)))
3731, 32, 36mpsyl 64 . . . . . . . 8 ((𝑦𝐵𝑥 = (inr‘𝑦)) → (inr‘𝑦) ∈ (inr “ 𝐵))
38 eleq1 2147 . . . . . . . . 9 (𝑥 = (inr‘𝑦) → (𝑥 ∈ (inr “ 𝐵) ↔ (inr‘𝑦) ∈ (inr “ 𝐵)))
3938adantl 271 . . . . . . . 8 ((𝑦𝐵𝑥 = (inr‘𝑦)) → (𝑥 ∈ (inr “ 𝐵) ↔ (inr‘𝑦) ∈ (inr “ 𝐵)))
4037, 39mpbird 165 . . . . . . 7 ((𝑦𝐵𝑥 = (inr‘𝑦)) → 𝑥 ∈ (inr “ 𝐵))
4140rexlimiva 2480 . . . . . 6 (∃𝑦𝐵 𝑥 = (inr‘𝑦) → 𝑥 ∈ (inr “ 𝐵))
4227, 41orim12i 709 . . . . 5 ((∃𝑦𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦𝐵 𝑥 = (inr‘𝑦)) → (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
4312, 42syl 14 . . . 4 (𝑥 ∈ (𝐴𝐵) → (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
44 elun 3130 . . . 4 (𝑥 ∈ ((inl “ 𝐴) ∪ (inr “ 𝐵)) ↔ (𝑥 ∈ (inl “ 𝐴) ∨ 𝑥 ∈ (inr “ 𝐵)))
4543, 44sylibr 132 . . 3 (𝑥 ∈ (𝐴𝐵) → 𝑥 ∈ ((inl “ 𝐴) ∪ (inr “ 𝐵)))
4645ssriv 3018 . 2 (𝐴𝐵) ⊆ ((inl “ 𝐴) ∪ (inr “ 𝐵))
4711, 46eqssi 3030 1 ((inl “ 𝐴) ∪ (inr “ 𝐵)) = (𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wo 662   = wceq 1287  wcel 1436  wrex 2356  Vcvv 2615  cun 2986  wss 2988  c0 3275  {csn 3431  cop 3434   × cxp 4411  dom cdm 4413  ran crn 4414  cres 4415  cima 4416  Fun wfun 4977  1-1wf1 4980  1-1-ontowf1o 4982  cfv 4983  1𝑜c1o 6130  cdju 6677  inlcinl 6684  inrcinr 6685
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-nul 3942  ax-pow 3986  ax-pr 4012  ax-un 4236
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-int 3674  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-id 4096  df-iord 4169  df-on 4171  df-suc 4174  df-iom 4381  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-1st 5870  df-2nd 5871  df-1o 6137  df-dju 6678  df-inl 6686  df-inr 6687
This theorem is referenced by:  dju1p1e2  6770
  Copyright terms: Public domain W3C validator