# 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 ) )`
` |-  ( ( 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 ) ) ) ) )`
` |-  ( ( ( 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 ) ) = (/) )`
` |-  ( ( ph /\ b e. B ) -> -. ( 1st ` ( inr ` b ) ) = (/) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ph /\ b e. B ) -> ( inr ` b ) e. ( A |_| B ) )`
` |-  ( ( ph /\ b e. B ) -> G : B --> C )`
37 2ndinr
` |-  ( b e. B -> ( 2nd ` ( inr ` b ) ) = b )`
` |-  ( ( 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 )`