Metamath Proof Explorer

Theorem updjudhcoinrg

Description: The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second 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 updjudhcoinrg 
|- ( ph -> ( H o. ( inr |` B ) ) = G )

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 inrresf 
 |-  ( inr |` B ) : B --> ( A |_| B )
7 ffn 
 |-  ( ( inr |` B ) : B --> ( A |_| B ) -> ( inr |` B ) Fn B )
8 6 7 mp1i 
 |-  ( ph -> ( inr |` B ) Fn B )
9 frn 
 |-  ( ( inr |` B ) : B --> ( A |_| B ) -> ran ( inr |` B ) C_ ( A |_| B ) )
10 6 9 mp1i 
 |-  ( ph -> ran ( inr |` B ) C_ ( A |_| B ) )
11 fnco 
 |-  ( ( H Fn ( A |_| B ) /\ ( inr |` B ) Fn B /\ ran ( inr |` B ) C_ ( A |_| B ) ) -> ( H o. ( inr |` B ) ) Fn B )
12 5 8 10 11 syl3anc 
 |-  ( ph -> ( H o. ( inr |` B ) ) Fn B )
13 2 ffnd 
 |-  ( ph -> G Fn B )
14 fvco2 
 |-  ( ( ( inr |` B ) Fn B /\ b e. B ) -> ( ( H o. ( inr |` B ) ) ` b ) = ( H ` ( ( inr |` B ) ` b ) ) )
15 8 14 sylan 
 |-  ( ( ph /\ b e. B ) -> ( ( H o. ( inr |` B ) ) ` b ) = ( H ` ( ( inr |` B ) ` b ) ) )
16 fvres 
 |-  ( b e. B -> ( ( inr |` B ) ` b ) = ( inr ` b ) )
17 16 adantl 
 |-  ( ( ph /\ b e. B ) -> ( ( inr |` B ) ` b ) = ( inr ` b ) )
18 17 fveq2d 
 |-  ( ( ph /\ b e. B ) -> ( H ` ( ( inr |` B ) ` b ) ) = ( H ` ( inr ` b ) ) )
19 fveqeq2 
 |-  ( x = ( inr ` b ) -> ( ( 1st ` x ) = (/) <-> ( 1st ` ( inr ` b ) ) = (/) ) )
20 2fveq3 
 |-  ( x = ( inr ` b ) -> ( F ` ( 2nd ` x ) ) = ( F ` ( 2nd ` ( inr ` b ) ) ) )
21 2fveq3 
 |-  ( x = ( inr ` b ) -> ( G ` ( 2nd ` x ) ) = ( G ` ( 2nd ` ( inr ` b ) ) ) )
22 19 20 21 ifbieq12d 
 |-  ( x = ( inr ` b ) -> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) = if ( ( 1st ` ( inr ` b ) ) = (/) , ( F ` ( 2nd ` ( inr ` b ) ) ) , ( G ` ( 2nd ` ( inr ` b ) ) ) ) )
23 22 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ x = ( inr ` b ) ) -> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) = if ( ( 1st ` ( inr ` b ) ) = (/) , ( F ` ( 2nd ` ( inr ` b ) ) ) , ( G ` ( 2nd ` ( inr ` b ) ) ) ) )
24 1stinr 
 |-  ( b e. B -> ( 1st ` ( inr ` b ) ) = 1o )
25 1n0 
 |-  1o =/= (/)
26 25 neii 
 |-  -. 1o = (/)
27 eqeq1 
 |-  ( ( 1st ` ( inr ` b ) ) = 1o -> ( ( 1st ` ( inr ` b ) ) = (/) <-> 1o = (/) ) )
28 26 27 mtbiri 
 |-  ( ( 1st ` ( inr ` b ) ) = 1o -> -. ( 1st ` ( inr ` b ) ) = (/) )
29 24 28 syl 
 |-  ( b e. B -> -. ( 1st ` ( inr ` b ) ) = (/) )
30 29 adantl 
 |-  ( ( ph /\ b e. B ) -> -. ( 1st ` ( inr ` b ) ) = (/) )
31 30 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ x = ( inr ` b ) ) -> -. ( 1st ` ( inr ` b ) ) = (/) )
32 31 iffalsed 
 |-  ( ( ( ph /\ b e. B ) /\ x = ( inr ` b ) ) -> if ( ( 1st ` ( inr ` b ) ) = (/) , ( F ` ( 2nd ` ( inr ` b ) ) ) , ( G ` ( 2nd ` ( inr ` b ) ) ) ) = ( G ` ( 2nd ` ( inr ` b ) ) ) )
33 23 32 eqtrd 
 |-  ( ( ( ph /\ b e. B ) /\ x = ( inr ` b ) ) -> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) = ( G ` ( 2nd ` ( inr ` b ) ) ) )
34 djurcl 
 |-  ( b e. B -> ( inr ` b ) e. ( A |_| B ) )
35 34 adantl 
 |-  ( ( ph /\ b e. B ) -> ( inr ` b ) e. ( A |_| B ) )
36 2 adantr 
 |-  ( ( ph /\ b e. B ) -> G : B --> C )
37 2ndinr 
 |-  ( b e. B -> ( 2nd ` ( inr ` b ) ) = b )
38 37 adantl 
 |-  ( ( ph /\ b e. B ) -> ( 2nd ` ( inr ` b ) ) = b )
39 simpr 
 |-  ( ( ph /\ b e. B ) -> b e. B )
40 38 39 eqeltrd 
 |-  ( ( ph /\ b e. B ) -> ( 2nd ` ( inr ` b ) ) e. B )
41 36 40 ffvelrnd 
 |-  ( ( ph /\ b e. B ) -> ( G ` ( 2nd ` ( inr ` b ) ) ) e. C )
42 3 33 35 41 fvmptd2 
 |-  ( ( ph /\ b e. B ) -> ( H ` ( inr ` b ) ) = ( G ` ( 2nd ` ( inr ` b ) ) ) )
43 18 42 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( H ` ( ( inr |` B ) ` b ) ) = ( G ` ( 2nd ` ( inr ` b ) ) ) )
44 38 fveq2d 
 |-  ( ( ph /\ b e. B ) -> ( G ` ( 2nd ` ( inr ` b ) ) ) = ( G ` b ) )
45 15 43 44 3eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( H o. ( inr |` B ) ) ` b ) = ( G ` b ) )
46 12 13 45 eqfnfvd 
 |-  ( ph -> ( H o. ( inr |` B ) ) = G )