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

Theorem djufun 6957
Description: The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
Hypotheses
Ref Expression
djufun.f (𝜑 → Fun 𝐹)
djufun.g (𝜑 → Fun 𝐺)
Assertion
Ref Expression
djufun (𝜑 → Fun (𝐹d 𝐺))

Proof of Theorem djufun
StepHypRef Expression
1 djufun.f . . . 4 (𝜑 → Fun 𝐹)
2 inlresf1 6914 . . . . 5 (inl ↾ dom 𝐹):dom 𝐹1-1→(dom 𝐹 ⊔ dom 𝐺)
3 df-f1 5098 . . . . . 6 ((inl ↾ dom 𝐹):dom 𝐹1-1→(dom 𝐹 ⊔ dom 𝐺) ↔ ((inl ↾ dom 𝐹):dom 𝐹⟶(dom 𝐹 ⊔ dom 𝐺) ∧ Fun (inl ↾ dom 𝐹)))
43simprbi 273 . . . . 5 ((inl ↾ dom 𝐹):dom 𝐹1-1→(dom 𝐹 ⊔ dom 𝐺) → Fun (inl ↾ dom 𝐹))
52, 4mp1i 10 . . . 4 (𝜑 → Fun (inl ↾ dom 𝐹))
6 funco 5133 . . . 4 ((Fun 𝐹 ∧ Fun (inl ↾ dom 𝐹)) → Fun (𝐹(inl ↾ dom 𝐹)))
71, 5, 6syl2anc 408 . . 3 (𝜑 → Fun (𝐹(inl ↾ dom 𝐹)))
8 djufun.g . . . 4 (𝜑 → Fun 𝐺)
9 inrresf1 6915 . . . . 5 (inr ↾ dom 𝐺):dom 𝐺1-1→(dom 𝐹 ⊔ dom 𝐺)
10 df-f1 5098 . . . . . 6 ((inr ↾ dom 𝐺):dom 𝐺1-1→(dom 𝐹 ⊔ dom 𝐺) ↔ ((inr ↾ dom 𝐺):dom 𝐺⟶(dom 𝐹 ⊔ dom 𝐺) ∧ Fun (inr ↾ dom 𝐺)))
1110simprbi 273 . . . . 5 ((inr ↾ dom 𝐺):dom 𝐺1-1→(dom 𝐹 ⊔ dom 𝐺) → Fun (inr ↾ dom 𝐺))
129, 11mp1i 10 . . . 4 (𝜑 → Fun (inr ↾ dom 𝐺))
13 funco 5133 . . . 4 ((Fun 𝐺 ∧ Fun (inr ↾ dom 𝐺)) → Fun (𝐺(inr ↾ dom 𝐺)))
148, 12, 13syl2anc 408 . . 3 (𝜑 → Fun (𝐺(inr ↾ dom 𝐺)))
15 dmcoss 4778 . . . . . . 7 dom (𝐹(inl ↾ dom 𝐹)) ⊆ dom (inl ↾ dom 𝐹)
16 df-rn 4520 . . . . . . 7 ran (inl ↾ dom 𝐹) = dom (inl ↾ dom 𝐹)
1715, 16sseqtrri 3102 . . . . . 6 dom (𝐹(inl ↾ dom 𝐹)) ⊆ ran (inl ↾ dom 𝐹)
18 dmcoss 4778 . . . . . . 7 dom (𝐺(inr ↾ dom 𝐺)) ⊆ dom (inr ↾ dom 𝐺)
19 df-rn 4520 . . . . . . 7 ran (inr ↾ dom 𝐺) = dom (inr ↾ dom 𝐺)
2018, 19sseqtrri 3102 . . . . . 6 dom (𝐺(inr ↾ dom 𝐺)) ⊆ ran (inr ↾ dom 𝐺)
21 ss2in 3274 . . . . . 6 ((dom (𝐹(inl ↾ dom 𝐹)) ⊆ ran (inl ↾ dom 𝐹) ∧ dom (𝐺(inr ↾ dom 𝐺)) ⊆ ran (inr ↾ dom 𝐺)) → (dom (𝐹(inl ↾ dom 𝐹)) ∩ dom (𝐺(inr ↾ dom 𝐺))) ⊆ (ran (inl ↾ dom 𝐹) ∩ ran (inr ↾ dom 𝐺)))
2217, 20, 21mp2an 422 . . . . 5 (dom (𝐹(inl ↾ dom 𝐹)) ∩ dom (𝐺(inr ↾ dom 𝐺))) ⊆ (ran (inl ↾ dom 𝐹) ∩ ran (inr ↾ dom 𝐺))
23 djuinr 6916 . . . . . 6 (ran (inl ↾ dom 𝐹) ∩ ran (inr ↾ dom 𝐺)) = ∅
2423a1i 9 . . . . 5 (𝜑 → (ran (inl ↾ dom 𝐹) ∩ ran (inr ↾ dom 𝐺)) = ∅)
2522, 24sseqtrid 3117 . . . 4 (𝜑 → (dom (𝐹(inl ↾ dom 𝐹)) ∩ dom (𝐺(inr ↾ dom 𝐺))) ⊆ ∅)
26 ss0 3373 . . . 4 ((dom (𝐹(inl ↾ dom 𝐹)) ∩ dom (𝐺(inr ↾ dom 𝐺))) ⊆ ∅ → (dom (𝐹(inl ↾ dom 𝐹)) ∩ dom (𝐺(inr ↾ dom 𝐺))) = ∅)
2725, 26syl 14 . . 3 (𝜑 → (dom (𝐹(inl ↾ dom 𝐹)) ∩ dom (𝐺(inr ↾ dom 𝐺))) = ∅)
28 funun 5137 . . 3 (((Fun (𝐹(inl ↾ dom 𝐹)) ∧ Fun (𝐺(inr ↾ dom 𝐺))) ∧ (dom (𝐹(inl ↾ dom 𝐹)) ∩ dom (𝐺(inr ↾ dom 𝐺))) = ∅) → Fun ((𝐹(inl ↾ dom 𝐹)) ∪ (𝐺(inr ↾ dom 𝐺))))
297, 14, 27, 28syl21anc 1200 . 2 (𝜑 → Fun ((𝐹(inl ↾ dom 𝐹)) ∪ (𝐺(inr ↾ dom 𝐺))))
30 df-djud 6956 . . 3 (𝐹d 𝐺) = ((𝐹(inl ↾ dom 𝐹)) ∪ (𝐺(inr ↾ dom 𝐺)))
3130funeqi 5114 . 2 (Fun (𝐹d 𝐺) ↔ Fun ((𝐹(inl ↾ dom 𝐹)) ∪ (𝐺(inr ↾ dom 𝐺))))
3229, 31sylibr 133 1 (𝜑 → Fun (𝐹d 𝐺))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  cun 3039  cin 3040  wss 3041  c0 3333  ccnv 4508  dom cdm 4509  ran crn 4510  cres 4511  ccom 4513  Fun wfun 5087  wf 5089  1-1wf1 5090  cdju 6890  inlcinl 6898  inrcinr 6899  d cdjud 6955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-ral 2398  df-rex 2399  df-v 2662  df-sbc 2883  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-iord 4258  df-on 4260  df-suc 4263  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-1st 6006  df-2nd 6007  df-1o 6281  df-dju 6891  df-inl 6900  df-inr 6901  df-djud 6956
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator