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 ffvelcdmd 
 |-  ( ( 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 )