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

Theorem casefun 7086
Description: The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
Hypotheses
Ref Expression
casefun.f  |-  ( ph  ->  Fun  F )
casefun.g  |-  ( ph  ->  Fun  G )
Assertion
Ref Expression
casefun  |-  ( ph  ->  Fun case ( F ,  G ) )

Proof of Theorem casefun
StepHypRef Expression
1 casefun.f . . . 4  |-  ( ph  ->  Fun  F )
2 djulf1o 7059 . . . . . 6  |- inl : _V -1-1-onto-> ( { (/) }  X.  _V )
3 f1of1 5462 . . . . . 6  |-  (inl : _V
-1-1-onto-> ( { (/) }  X.  _V )  -> inl : _V -1-1-> ( {
(/) }  X.  _V )
)
42, 3ax-mp 5 . . . . 5  |- inl : _V -1-1-> ( { (/) }  X.  _V )
5 df-f1 5223 . . . . . 6  |-  (inl : _V
-1-1-> ( { (/) }  X.  _V )  <->  (inl : _V --> ( {
(/) }  X.  _V )  /\  Fun  `'inl ) )
65simprbi 275 . . . . 5  |-  (inl : _V
-1-1-> ( { (/) }  X.  _V )  ->  Fun  `'inl )
74, 6mp1i 10 . . . 4  |-  ( ph  ->  Fun  `'inl )
8 funco 5258 . . . 4  |-  ( ( Fun  F  /\  Fun  `'inl )  ->  Fun  ( F  o.  `'inl ) )
91, 7, 8syl2anc 411 . . 3  |-  ( ph  ->  Fun  ( F  o.  `'inl ) )
10 casefun.g . . . 4  |-  ( ph  ->  Fun  G )
11 djurf1o 7060 . . . . . 6  |- inr : _V -1-1-onto-> ( { 1o }  X.  _V )
12 f1of1 5462 . . . . . 6  |-  (inr : _V
-1-1-onto-> ( { 1o }  X.  _V )  -> inr : _V -1-1-> ( { 1o }  X.  _V ) )
1311, 12ax-mp 5 . . . . 5  |- inr : _V -1-1-> ( { 1o }  X.  _V )
14 df-f1 5223 . . . . . 6  |-  (inr : _V
-1-1-> ( { 1o }  X.  _V )  <->  (inr : _V
--> ( { 1o }  X.  _V )  /\  Fun  `'inr ) )
1514simprbi 275 . . . . 5  |-  (inr : _V
-1-1-> ( { 1o }  X.  _V )  ->  Fun  `'inr )
1613, 15mp1i 10 . . . 4  |-  ( ph  ->  Fun  `'inr )
17 funco 5258 . . . 4  |-  ( ( Fun  G  /\  Fun  `'inr )  ->  Fun  ( G  o.  `'inr ) )
1810, 16, 17syl2anc 411 . . 3  |-  ( ph  ->  Fun  ( G  o.  `'inr ) )
19 dmcoss 4898 . . . . . . 7  |-  dom  ( F  o.  `'inl )  C_ 
dom  `'inl
20 df-rn 4639 . . . . . . 7  |-  ran inl  =  dom  `'inl
2119, 20sseqtrri 3192 . . . . . 6  |-  dom  ( F  o.  `'inl )  C_ 
ran inl
22 dmcoss 4898 . . . . . . 7  |-  dom  ( G  o.  `'inr )  C_ 
dom  `'inr
23 df-rn 4639 . . . . . . 7  |-  ran inr  =  dom  `'inr
2422, 23sseqtrri 3192 . . . . . 6  |-  dom  ( G  o.  `'inr )  C_ 
ran inr
25 ss2in 3365 . . . . . 6  |-  ( ( dom  ( F  o.  `'inl )  C_  ran inl  /\  dom  ( G  o.  `'inr )  C_  ran inr )  ->  ( dom  ( F  o.  `'inl )  i^i  dom  ( G  o.  `'inr )
)  C_  ( ran inl  i^i 
ran inr ) )
2621, 24, 25mp2an 426 . . . . 5  |-  ( dom  ( F  o.  `'inl )  i^i  dom  ( G  o.  `'inr ) )  C_  ( ran inl  i^i  ran inr )
27 rnresv 5090 . . . . . . . . 9  |-  ran  (inl  |` 
_V )  =  ran inl
2827eqcomi 2181 . . . . . . . 8  |-  ran inl  =  ran  (inl  |`  _V )
29 rnresv 5090 . . . . . . . . 9  |-  ran  (inr  |` 
_V )  =  ran inr
3029eqcomi 2181 . . . . . . . 8  |-  ran inr  =  ran  (inr  |`  _V )
3128, 30ineq12i 3336 . . . . . . 7  |-  ( ran inl  i^i  ran inr )  =  ( ran  (inl  |`  _V )  i^i  ran  (inr  |`  _V )
)
32 djuinr 7064 . . . . . . 7  |-  ( ran  (inl  |`  _V )  i^i 
ran  (inr  |`  _V )
)  =  (/)
3331, 32eqtri 2198 . . . . . 6  |-  ( ran inl  i^i  ran inr )  =  (/)
3433a1i 9 . . . . 5  |-  ( ph  ->  ( ran inl  i^i  ran inr )  =  (/) )
3526, 34sseqtrid 3207 . . . 4  |-  ( ph  ->  ( dom  ( F  o.  `'inl )  i^i 
dom  ( G  o.  `'inr ) )  C_  (/) )
36 ss0 3465 . . . 4  |-  ( ( dom  ( F  o.  `'inl )  i^i  dom  ( G  o.  `'inr )
)  C_  (/)  ->  ( dom  ( F  o.  `'inl )  i^i  dom  ( G  o.  `'inr ) )  =  (/) )
3735, 36syl 14 . . 3  |-  ( ph  ->  ( dom  ( F  o.  `'inl )  i^i 
dom  ( G  o.  `'inr ) )  =  (/) )
38 funun 5262 . . 3  |-  ( ( ( Fun  ( F  o.  `'inl )  /\  Fun  ( G  o.  `'inr ) )  /\  ( dom  ( F  o.  `'inl )  i^i  dom  ( G  o.  `'inr ) )  =  (/) )  ->  Fun  ( ( F  o.  `'inl )  u.  ( G  o.  `'inr ) ) )
399, 18, 37, 38syl21anc 1237 . 2  |-  ( ph  ->  Fun  ( ( F  o.  `'inl )  u.  ( G  o.  `'inr ) ) )
40 df-case 7085 . . 3  |- case ( F ,  G )  =  ( ( F  o.  `'inl )  u.  ( G  o.  `'inr )
)
4140funeqi 5239 . 2  |-  ( Fun case
( F ,  G
)  <->  Fun  ( ( F  o.  `'inl )  u.  ( G  o.  `'inr ) ) )
4239, 41sylibr 134 1  |-  ( ph  ->  Fun case ( F ,  G ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353   _Vcvv 2739    u. cun 3129    i^i cin 3130    C_ wss 3131   (/)c0 3424   {csn 3594    X. cxp 4626   `'ccnv 4627   dom cdm 4628   ran crn 4629    |` cres 4630    o. ccom 4632   Fun wfun 5212   -->wf 5214   -1-1->wf1 5215   -1-1-onto->wf1o 5217   1oc1o 6412  inlcinl 7046  inrcinr 7047  casecdjucase 7084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-v 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-1st 6143  df-2nd 6144  df-1o 6419  df-inl 7048  df-inr 7049  df-case 7085
This theorem is referenced by:  casef  7089
  Copyright terms: Public domain W3C validator