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

Theorem updjudhcoinlf 7053
Description: The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.)
Hypotheses
Ref Expression
updjud.f  |-  ( ph  ->  F : A --> C )
updjud.g  |-  ( ph  ->  G : B --> C )
updjudhf.h  |-  H  =  ( x  e.  ( A B )  |->  if ( ( 1st `  x
)  =  (/) ,  ( F `  ( 2nd `  x ) ) ,  ( G `  ( 2nd `  x ) ) ) )
Assertion
Ref Expression
updjudhcoinlf  |-  ( ph  ->  ( H  o.  (inl  |`  A ) )  =  F )
Distinct variable groups:    x, A    x, B    x, C    ph, x    x, F
Allowed substitution hints:    G( x)    H( x)

Proof of Theorem updjudhcoinlf
Dummy variable  a is distinct from all other variables.
StepHypRef Expression
1 updjud.f . . . . 5  |-  ( ph  ->  F : A --> C )
2 updjud.g . . . . 5  |-  ( ph  ->  G : B --> C )
3 updjudhf.h . . . . 5  |-  H  =  ( x  e.  ( A B )  |->  if ( ( 1st `  x
)  =  (/) ,  ( F `  ( 2nd `  x ) ) ,  ( G `  ( 2nd `  x ) ) ) )
41, 2, 3updjudhf 7052 . . . 4  |-  ( ph  ->  H : ( A B ) --> C )
5 ffn 5345 . . . 4  |-  ( H : ( A B ) --> C  ->  H  Fn  ( A B ) )
64, 5syl 14 . . 3  |-  ( ph  ->  H  Fn  ( A B ) )
7 inlresf1 7034 . . . 4  |-  (inl  |`  A ) : A -1-1-> ( A B )
8 f1fn 5403 . . . 4  |-  ( (inl  |`  A ) : A -1-1-> ( A B )  ->  (inl  |`  A )  Fn  A
)
97, 8mp1i 10 . . 3  |-  ( ph  ->  (inl  |`  A )  Fn  A )
10 f1f 5401 . . . . 5  |-  ( (inl  |`  A ) : A -1-1-> ( A B )  ->  (inl  |`  A ) : A --> ( A B ) )
117, 10ax-mp 5 . . . 4  |-  (inl  |`  A ) : A --> ( A B )
12 frn 5354 . . . 4  |-  ( (inl  |`  A ) : A --> ( A B )  ->  ran  (inl  |`  A )  C_  ( A B ) )
1311, 12mp1i 10 . . 3  |-  ( ph  ->  ran  (inl  |`  A ) 
C_  ( A B ) )
14 fnco 5304 . . 3  |-  ( ( H  Fn  ( A B )  /\  (inl  |`  A )  Fn  A  /\  ran  (inl  |`  A ) 
C_  ( A B ) )  ->  ( H  o.  (inl  |`  A ) )  Fn  A )
156, 9, 13, 14syl3anc 1233 . 2  |-  ( ph  ->  ( H  o.  (inl  |`  A ) )  Fn  A )
16 ffn 5345 . . 3  |-  ( F : A --> C  ->  F  Fn  A )
171, 16syl 14 . 2  |-  ( ph  ->  F  Fn  A )
18 fvco2 5563 . . . 4  |-  ( ( (inl  |`  A )  Fn  A  /\  a  e.  A )  ->  (
( H  o.  (inl  |`  A ) ) `  a )  =  ( H `  ( (inl  |`  A ) `  a
) ) )
199, 18sylan 281 . . 3  |-  ( (
ph  /\  a  e.  A )  ->  (
( H  o.  (inl  |`  A ) ) `  a )  =  ( H `  ( (inl  |`  A ) `  a
) ) )
20 fvres 5518 . . . . . 6  |-  ( a  e.  A  ->  (
(inl  |`  A ) `  a )  =  (inl
`  a ) )
2120adantl 275 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  (
(inl  |`  A ) `  a )  =  (inl
`  a ) )
2221fveq2d 5498 . . . 4  |-  ( (
ph  /\  a  e.  A )  ->  ( H `  ( (inl  |`  A ) `  a
) )  =  ( H `  (inl `  a ) ) )
233a1i 9 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  H  =  ( x  e.  ( A B )  |->  if ( ( 1st `  x )  =  (/) ,  ( F `  ( 2nd `  x ) ) ,  ( G `  ( 2nd `  x ) ) ) ) )
24 fveq2 5494 . . . . . . . . 9  |-  ( x  =  (inl `  a
)  ->  ( 1st `  x )  =  ( 1st `  (inl `  a ) ) )
2524eqeq1d 2179 . . . . . . . 8  |-  ( x  =  (inl `  a
)  ->  ( ( 1st `  x )  =  (/) 
<->  ( 1st `  (inl `  a ) )  =  (/) ) )
26 fveq2 5494 . . . . . . . . 9  |-  ( x  =  (inl `  a
)  ->  ( 2nd `  x )  =  ( 2nd `  (inl `  a ) ) )
2726fveq2d 5498 . . . . . . . 8  |-  ( x  =  (inl `  a
)  ->  ( F `  ( 2nd `  x
) )  =  ( F `  ( 2nd `  (inl `  a )
) ) )
2826fveq2d 5498 . . . . . . . 8  |-  ( x  =  (inl `  a
)  ->  ( G `  ( 2nd `  x
) )  =  ( G `  ( 2nd `  (inl `  a )
) ) )
2925, 27, 28ifbieq12d 3551 . . . . . . 7  |-  ( x  =  (inl `  a
)  ->  if (
( 1st `  x
)  =  (/) ,  ( F `  ( 2nd `  x ) ) ,  ( G `  ( 2nd `  x ) ) )  =  if ( ( 1st `  (inl `  a ) )  =  (/) ,  ( F `  ( 2nd `  (inl `  a ) ) ) ,  ( G `  ( 2nd `  (inl `  a ) ) ) ) )
3029adantl 275 . . . . . 6  |-  ( ( ( ph  /\  a  e.  A )  /\  x  =  (inl `  a )
)  ->  if (
( 1st `  x
)  =  (/) ,  ( F `  ( 2nd `  x ) ) ,  ( G `  ( 2nd `  x ) ) )  =  if ( ( 1st `  (inl `  a ) )  =  (/) ,  ( F `  ( 2nd `  (inl `  a ) ) ) ,  ( G `  ( 2nd `  (inl `  a ) ) ) ) )
31 1stinl 7047 . . . . . . . . 9  |-  ( a  e.  A  ->  ( 1st `  (inl `  a
) )  =  (/) )
3231adantl 275 . . . . . . . 8  |-  ( (
ph  /\  a  e.  A )  ->  ( 1st `  (inl `  a
) )  =  (/) )
3332adantr 274 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  A )  /\  x  =  (inl `  a )
)  ->  ( 1st `  (inl `  a )
)  =  (/) )
3433iftrued 3532 . . . . . 6  |-  ( ( ( ph  /\  a  e.  A )  /\  x  =  (inl `  a )
)  ->  if (
( 1st `  (inl `  a ) )  =  (/) ,  ( F `  ( 2nd `  (inl `  a ) ) ) ,  ( G `  ( 2nd `  (inl `  a ) ) ) )  =  ( F `
 ( 2nd `  (inl `  a ) ) ) )
3530, 34eqtrd 2203 . . . . 5  |-  ( ( ( ph  /\  a  e.  A )  /\  x  =  (inl `  a )
)  ->  if (
( 1st `  x
)  =  (/) ,  ( F `  ( 2nd `  x ) ) ,  ( G `  ( 2nd `  x ) ) )  =  ( F `
 ( 2nd `  (inl `  a ) ) ) )
36 djulcl 7024 . . . . . 6  |-  ( a  e.  A  ->  (inl `  a )  e.  ( A B ) )
3736adantl 275 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  (inl `  a )  e.  ( A B ) )
381adantr 274 . . . . . 6  |-  ( (
ph  /\  a  e.  A )  ->  F : A --> C )
39 2ndinl 7048 . . . . . . . 8  |-  ( a  e.  A  ->  ( 2nd `  (inl `  a
) )  =  a )
4039adantl 275 . . . . . . 7  |-  ( (
ph  /\  a  e.  A )  ->  ( 2nd `  (inl `  a
) )  =  a )
41 simpr 109 . . . . . . 7  |-  ( (
ph  /\  a  e.  A )  ->  a  e.  A )
4240, 41eqeltrd 2247 . . . . . 6  |-  ( (
ph  /\  a  e.  A )  ->  ( 2nd `  (inl `  a
) )  e.  A
)
4338, 42ffvelrnd 5629 . . . . 5  |-  ( (
ph  /\  a  e.  A )  ->  ( F `  ( 2nd `  (inl `  a )
) )  e.  C
)
4423, 35, 37, 43fvmptd 5575 . . . 4  |-  ( (
ph  /\  a  e.  A )  ->  ( H `  (inl `  a
) )  =  ( F `  ( 2nd `  (inl `  a )
) ) )
4522, 44eqtrd 2203 . . 3  |-  ( (
ph  /\  a  e.  A )  ->  ( H `  ( (inl  |`  A ) `  a
) )  =  ( F `  ( 2nd `  (inl `  a )
) ) )
4640fveq2d 5498 . . 3  |-  ( (
ph  /\  a  e.  A )  ->  ( F `  ( 2nd `  (inl `  a )
) )  =  ( F `  a ) )
4719, 45, 463eqtrd 2207 . 2  |-  ( (
ph  /\  a  e.  A )  ->  (
( H  o.  (inl  |`  A ) ) `  a )  =  ( F `  a ) )
4815, 17, 47eqfnfvd 5594 1  |-  ( ph  ->  ( H  o.  (inl  |`  A ) )  =  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1348    e. wcel 2141    C_ wss 3121   (/)c0 3414   ifcif 3525    |-> cmpt 4048   ran crn 4610    |` cres 4611    o. ccom 4613    Fn wfn 5191   -->wf 5192   -1-1->wf1 5193   ` cfv 5196   1stc1st 6114   2ndc2nd 6115   ⊔ cdju 7010  inlcinl 7018
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-iord 4349  df-on 4351  df-suc 4354  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-1st 6116  df-2nd 6117  df-1o 6392  df-dju 7011  df-inl 7020  df-inr 7021
This theorem is referenced by:  updjud  7055
  Copyright terms: Public domain W3C validator