Metamath Proof Explorer

Theorem updjudhf

Description: The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-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 updjudhf 
|- ( ph -> H : ( A |_| B ) --> C )

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 eldju2ndl 
 |-  ( ( x e. ( A |_| B ) /\ ( 1st ` x ) = (/) ) -> ( 2nd ` x ) e. A )
5 4 ex 
 |-  ( x e. ( A |_| B ) -> ( ( 1st ` x ) = (/) -> ( 2nd ` x ) e. A ) )
6 ffvelcdm 
 |-  ( ( F : A --> C /\ ( 2nd ` x ) e. A ) -> ( F ` ( 2nd ` x ) ) e. C )
7 6 ex 
 |-  ( F : A --> C -> ( ( 2nd ` x ) e. A -> ( F ` ( 2nd ` x ) ) e. C ) )
8 1 7 syl 
 |-  ( ph -> ( ( 2nd ` x ) e. A -> ( F ` ( 2nd ` x ) ) e. C ) )
9 5 8 sylan9r 
 |-  ( ( ph /\ x e. ( A |_| B ) ) -> ( ( 1st ` x ) = (/) -> ( F ` ( 2nd ` x ) ) e. C ) )
10 9 imp 
 |-  ( ( ( ph /\ x e. ( A |_| B ) ) /\ ( 1st ` x ) = (/) ) -> ( F ` ( 2nd ` x ) ) e. C )
11 df-ne 
 |-  ( ( 1st ` x ) =/= (/) <-> -. ( 1st ` x ) = (/) )
12 eldju2ndr 
 |-  ( ( x e. ( A |_| B ) /\ ( 1st ` x ) =/= (/) ) -> ( 2nd ` x ) e. B )
13 12 ex 
 |-  ( x e. ( A |_| B ) -> ( ( 1st ` x ) =/= (/) -> ( 2nd ` x ) e. B ) )
14 ffvelcdm 
 |-  ( ( G : B --> C /\ ( 2nd ` x ) e. B ) -> ( G ` ( 2nd ` x ) ) e. C )
15 14 ex 
 |-  ( G : B --> C -> ( ( 2nd ` x ) e. B -> ( G ` ( 2nd ` x ) ) e. C ) )
16 2 15 syl 
 |-  ( ph -> ( ( 2nd ` x ) e. B -> ( G ` ( 2nd ` x ) ) e. C ) )
17 13 16 sylan9r 
 |-  ( ( ph /\ x e. ( A |_| B ) ) -> ( ( 1st ` x ) =/= (/) -> ( G ` ( 2nd ` x ) ) e. C ) )
18 11 17 biimtrrid 
 |-  ( ( ph /\ x e. ( A |_| B ) ) -> ( -. ( 1st ` x ) = (/) -> ( G ` ( 2nd ` x ) ) e. C ) )
19 18 imp 
 |-  ( ( ( ph /\ x e. ( A |_| B ) ) /\ -. ( 1st ` x ) = (/) ) -> ( G ` ( 2nd ` x ) ) e. C )
20 10 19 ifclda 
 |-  ( ( ph /\ x e. ( A |_| B ) ) -> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) e. C )
21 20 3 fmptd 
 |-  ( ph -> H : ( A |_| B ) --> C )