# Metamath Proof Explorer

## Theorem updjudhcoinlf

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)

Ref Expression
Hypotheses 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 updjudhcoinlf
`|- ( ph -> ( H o. ( inl |` A ) ) = F )`

### Proof

Step Hyp Ref Expression
1 updjud.f
` |-  ( ph -> F : A --> C )`
2 updjud.g
` |-  ( ph -> G : B --> C )`
3 updjudhf.h
` |-  H = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) )`
4 1 2 3 updjudhf
` |-  ( ph -> H : ( A |_| B ) --> C )`
5 4 ffnd
` |-  ( ph -> H Fn ( A |_| B ) )`
6 inlresf
` |-  ( inl |` A ) : A --> ( A |_| B )`
7 ffn
` |-  ( ( inl |` A ) : A --> ( A |_| B ) -> ( inl |` A ) Fn A )`
8 6 7 mp1i
` |-  ( ph -> ( inl |` A ) Fn A )`
9 frn
` |-  ( ( inl |` A ) : A --> ( A |_| B ) -> ran ( inl |` A ) C_ ( A |_| B ) )`
10 6 9 mp1i
` |-  ( ph -> ran ( inl |` A ) C_ ( A |_| B ) )`
11 fnco
` |-  ( ( H Fn ( A |_| B ) /\ ( inl |` A ) Fn A /\ ran ( inl |` A ) C_ ( A |_| B ) ) -> ( H o. ( inl |` A ) ) Fn A )`
12 5 8 10 11 syl3anc
` |-  ( ph -> ( H o. ( inl |` A ) ) Fn A )`
13 1 ffnd
` |-  ( ph -> F Fn A )`
14 fvco2
` |-  ( ( ( inl |` A ) Fn A /\ a e. A ) -> ( ( H o. ( inl |` A ) ) ` a ) = ( H ` ( ( inl |` A ) ` a ) ) )`
15 8 14 sylan
` |-  ( ( ph /\ a e. A ) -> ( ( H o. ( inl |` A ) ) ` a ) = ( H ` ( ( inl |` A ) ` a ) ) )`
16 fvres
` |-  ( a e. A -> ( ( inl |` A ) ` a ) = ( inl ` a ) )`
17 16 adantl
` |-  ( ( ph /\ a e. A ) -> ( ( inl |` A ) ` a ) = ( inl ` a ) )`
18 17 fveq2d
` |-  ( ( ph /\ a e. A ) -> ( H ` ( ( inl |` A ) ` a ) ) = ( H ` ( inl ` a ) ) )`
19 fveqeq2
` |-  ( x = ( inl ` a ) -> ( ( 1st ` x ) = (/) <-> ( 1st ` ( inl ` a ) ) = (/) ) )`
20 2fveq3
` |-  ( x = ( inl ` a ) -> ( F ` ( 2nd ` x ) ) = ( F ` ( 2nd ` ( inl ` a ) ) ) )`
21 2fveq3
` |-  ( x = ( inl ` a ) -> ( G ` ( 2nd ` x ) ) = ( G ` ( 2nd ` ( inl ` a ) ) ) )`
22 19 20 21 ifbieq12d
` |-  ( x = ( inl ` a ) -> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) = if ( ( 1st ` ( inl ` a ) ) = (/) , ( F ` ( 2nd ` ( inl ` a ) ) ) , ( G ` ( 2nd ` ( inl ` a ) ) ) ) )`
23 22 adantl
` |-  ( ( ( 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 ) ) ) ) )`
24 1stinl
` |-  ( a e. A -> ( 1st ` ( inl ` a ) ) = (/) )`
25 24 adantl
` |-  ( ( ph /\ a e. A ) -> ( 1st ` ( inl ` a ) ) = (/) )`
26 25 adantr
` |-  ( ( ( ph /\ a e. A ) /\ x = ( inl ` a ) ) -> ( 1st ` ( inl ` a ) ) = (/) )`
27 26 iftrued
` |-  ( ( ( ph /\ a e. A ) /\ x = ( inl ` a ) ) -> if ( ( 1st ` ( inl ` a ) ) = (/) , ( F ` ( 2nd ` ( inl ` a ) ) ) , ( G ` ( 2nd ` ( inl ` a ) ) ) ) = ( F ` ( 2nd ` ( inl ` a ) ) ) )`
28 23 27 eqtrd
` |-  ( ( ( ph /\ a e. A ) /\ x = ( inl ` a ) ) -> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) = ( F ` ( 2nd ` ( inl ` a ) ) ) )`
29 djulcl
` |-  ( a e. A -> ( inl ` a ) e. ( A |_| B ) )`
30 29 adantl
` |-  ( ( ph /\ a e. A ) -> ( inl ` a ) e. ( A |_| B ) )`
31 1 adantr
` |-  ( ( ph /\ a e. A ) -> F : A --> C )`
32 2ndinl
` |-  ( a e. A -> ( 2nd ` ( inl ` a ) ) = a )`
33 32 adantl
` |-  ( ( ph /\ a e. A ) -> ( 2nd ` ( inl ` a ) ) = a )`
34 simpr
` |-  ( ( ph /\ a e. A ) -> a e. A )`
35 33 34 eqeltrd
` |-  ( ( ph /\ a e. A ) -> ( 2nd ` ( inl ` a ) ) e. A )`
36 31 35 ffvelrnd
` |-  ( ( ph /\ a e. A ) -> ( F ` ( 2nd ` ( inl ` a ) ) ) e. C )`
37 3 28 30 36 fvmptd2
` |-  ( ( ph /\ a e. A ) -> ( H ` ( inl ` a ) ) = ( F ` ( 2nd ` ( inl ` a ) ) ) )`
38 18 37 eqtrd
` |-  ( ( ph /\ a e. A ) -> ( H ` ( ( inl |` A ) ` a ) ) = ( F ` ( 2nd ` ( inl ` a ) ) ) )`
39 33 fveq2d
` |-  ( ( ph /\ a e. A ) -> ( F ` ( 2nd ` ( inl ` a ) ) ) = ( F ` a ) )`
40 15 38 39 3eqtrd
` |-  ( ( ph /\ a e. A ) -> ( ( H o. ( inl |` A ) ) ` a ) = ( F ` a ) )`
41 12 13 40 eqfnfvd
` |-  ( ph -> ( H o. ( inl |` A ) ) = F )`