Metamath Proof Explorer

Theorem updjud

Description: Universal property of the disjoint union. This theorem shows that the disjoint union, together with the left and right injections df-inl and df-inr , is thecoproduct in the category of sets, see Wikipedia "Coproduct", https://en.wikipedia.org/wiki/Coproduct (25-Aug-2023). This is a special case of Example 1 of coproducts in Section 10.67 of Adamek p. 185. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022)

Ref Expression
Hypotheses updjud.f 
|- ( ph -> F : A --> C )
updjud.g 
|- ( ph -> G : B --> C )
updjud.a 
|- ( ph -> A e. V )
updjud.b 
|- ( ph -> B e. W )
Assertion updjud 
|- ( ph -> E! h ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( 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 updjud.a 
 |-  ( ph -> A e. V )
4 updjud.b 
 |-  ( ph -> B e. W )
5 3 4 jca 
 |-  ( ph -> ( A e. V /\ B e. W ) )
6 djuex 
 |-  ( ( A e. V /\ B e. W ) -> ( A |_| B ) e. _V )
7 mptexg 
 |-  ( ( A |_| B ) e. _V -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) e. _V )
8 5 6 7 3syl 
 |-  ( ph -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) e. _V )
9 feq1 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( h : ( A |_| B ) --> C <-> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C ) )
10 coeq1 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( h o. ( inl |` A ) ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) )
11 10 eqeq1d 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( ( h o. ( inl |` A ) ) = F <-> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F ) )
12 coeq1 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( h o. ( inr |` B ) ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) )
13 12 eqeq1d 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( ( h o. ( inr |` B ) ) = G <-> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) )
14 9 11 13 3anbi123d 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) <-> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) )
15 eqeq1 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( h = k <-> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) )
16 15 imbi2d 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> h = k ) <-> ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) ) )
17 16 ralbidv 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> h = k ) <-> A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) ) )
18 14 17 anbi12d 
 |-  ( h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) -> ( ( ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> h = k ) ) <-> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) ) ) )
19 18 adantl 
 |-  ( ( ph /\ h = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ) -> ( ( ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> h = k ) ) <-> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) ) ) )
20 eqid 
 |-  ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) )
21 1 2 20 updjudhf 
 |-  ( ph -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C )
22 1 2 20 updjudhcoinlf 
 |-  ( ph -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F )
23 1 2 20 updjudhcoinrg 
 |-  ( ph -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G )
24 simpr 
 |-  ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) )
25 eqeq2 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F -> ( ( k o. ( inl |` A ) ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) <-> ( k o. ( inl |` A ) ) = F ) )
26 fvres 
 |-  ( z e. A -> ( ( inl |` A ) ` z ) = ( inl ` z ) )
27 26 eqcomd 
 |-  ( z e. A -> ( inl ` z ) = ( ( inl |` A ) ` z ) )
28 27 eqeq2d 
 |-  ( z e. A -> ( y = ( inl ` z ) <-> y = ( ( inl |` A ) ` z ) ) )
29 28 adantl 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) /\ z e. A ) -> ( y = ( inl ` z ) <-> y = ( ( inl |` A ) ` z ) ) )
30 fveq1 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) ` z ) = ( ( k o. ( inl |` A ) ) ` z ) )
31 30 ad2antrr 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) /\ z e. A ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) ` z ) = ( ( k o. ( inl |` A ) ) ` z ) )
32 inlresf 
 |-  ( inl |` A ) : A --> ( A |_| B )
33 ffn 
 |-  ( ( inl |` A ) : A --> ( A |_| B ) -> ( inl |` A ) Fn A )
34 32 33 mp1i 
 |-  ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) -> ( inl |` A ) Fn A )
35 fvco2 
 |-  ( ( ( inl |` A ) Fn A /\ z e. A ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) ` z ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inl |` A ) ` z ) ) )
36 34 35 sylan 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) /\ z e. A ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) ` z ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inl |` A ) ` z ) ) )
37 fvco2 
 |-  ( ( ( inl |` A ) Fn A /\ z e. A ) -> ( ( k o. ( inl |` A ) ) ` z ) = ( k ` ( ( inl |` A ) ` z ) ) )
38 34 37 sylan 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) /\ z e. A ) -> ( ( k o. ( inl |` A ) ) ` z ) = ( k ` ( ( inl |` A ) ` z ) ) )
39 31 36 38 3eqtr3d 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) /\ z e. A ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inl |` A ) ` z ) ) = ( k ` ( ( inl |` A ) ` z ) ) )
40 fveq2 
 |-  ( y = ( ( inl |` A ) ` z ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inl |` A ) ` z ) ) )
41 fveq2 
 |-  ( y = ( ( inl |` A ) ` z ) -> ( k ` y ) = ( k ` ( ( inl |` A ) ` z ) ) )
42 40 41 eqeq12d 
 |-  ( y = ( ( inl |` A ) ` z ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) <-> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inl |` A ) ` z ) ) = ( k ` ( ( inl |` A ) ` z ) ) ) )
43 39 42 syl5ibrcom 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) /\ z e. A ) -> ( y = ( ( inl |` A ) ` z ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
44 29 43 sylbid 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) /\ z e. A ) -> ( y = ( inl ` z ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
45 44 expimpd 
 |-  ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) /\ ph ) -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
46 45 ex 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) -> ( ph -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
47 46 eqcoms 
 |-  ( ( k o. ( inl |` A ) ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) -> ( ph -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
48 25 47 biimtrrdi 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F -> ( ( k o. ( inl |` A ) ) = F -> ( ph -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) ) )
49 48 com23 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F -> ( ph -> ( ( k o. ( inl |` A ) ) = F -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) ) )
50 49 3ad2ant2 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) -> ( ph -> ( ( k o. ( inl |` A ) ) = F -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) ) )
51 50 impcom 
 |-  ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( k o. ( inl |` A ) ) = F -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
52 51 com12 
 |-  ( ( k o. ( inl |` A ) ) = F -> ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
53 52 3ad2ant2 
 |-  ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
54 53 impcom 
 |-  ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
55 54 com12 
 |-  ( ( z e. A /\ y = ( inl ` z ) ) -> ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
56 55 rexlimiva 
 |-  ( E. z e. A y = ( inl ` z ) -> ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
57 eqeq2 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G -> ( ( k o. ( inr |` B ) ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) <-> ( k o. ( inr |` B ) ) = G ) )
58 fvres 
 |-  ( z e. B -> ( ( inr |` B ) ` z ) = ( inr ` z ) )
59 58 eqcomd 
 |-  ( z e. B -> ( inr ` z ) = ( ( inr |` B ) ` z ) )
60 59 eqeq2d 
 |-  ( z e. B -> ( y = ( inr ` z ) <-> y = ( ( inr |` B ) ` z ) ) )
61 60 adantl 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) /\ z e. B ) -> ( y = ( inr ` z ) <-> y = ( ( inr |` B ) ` z ) ) )
62 fveq1 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) ` z ) = ( ( k o. ( inr |` B ) ) ` z ) )
63 62 ad2antrr 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) /\ z e. B ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) ` z ) = ( ( k o. ( inr |` B ) ) ` z ) )
64 inrresf 
 |-  ( inr |` B ) : B --> ( A |_| B )
65 ffn 
 |-  ( ( inr |` B ) : B --> ( A |_| B ) -> ( inr |` B ) Fn B )
66 64 65 mp1i 
 |-  ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) -> ( inr |` B ) Fn B )
67 fvco2 
 |-  ( ( ( inr |` B ) Fn B /\ z e. B ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) ` z ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inr |` B ) ` z ) ) )
68 66 67 sylan 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) /\ z e. B ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) ` z ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inr |` B ) ` z ) ) )
69 fvco2 
 |-  ( ( ( inr |` B ) Fn B /\ z e. B ) -> ( ( k o. ( inr |` B ) ) ` z ) = ( k ` ( ( inr |` B ) ` z ) ) )
70 66 69 sylan 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) /\ z e. B ) -> ( ( k o. ( inr |` B ) ) ` z ) = ( k ` ( ( inr |` B ) ` z ) ) )
71 63 68 70 3eqtr3d 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) /\ z e. B ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inr |` B ) ` z ) ) = ( k ` ( ( inr |` B ) ` z ) ) )
72 fveq2 
 |-  ( y = ( ( inr |` B ) ` z ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inr |` B ) ` z ) ) )
73 fveq2 
 |-  ( y = ( ( inr |` B ) ` z ) -> ( k ` y ) = ( k ` ( ( inr |` B ) ` z ) ) )
74 72 73 eqeq12d 
 |-  ( y = ( ( inr |` B ) ` z ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) <-> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` ( ( inr |` B ) ` z ) ) = ( k ` ( ( inr |` B ) ` z ) ) ) )
75 71 74 syl5ibrcom 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) /\ z e. B ) -> ( y = ( ( inr |` B ) ` z ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
76 61 75 sylbid 
 |-  ( ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) /\ z e. B ) -> ( y = ( inr ` z ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
77 76 expimpd 
 |-  ( ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) /\ ph ) -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
78 77 ex 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) -> ( ph -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
79 78 eqcoms 
 |-  ( ( k o. ( inr |` B ) ) = ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) -> ( ph -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
80 57 79 biimtrrdi 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G -> ( ( k o. ( inr |` B ) ) = G -> ( ph -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) ) )
81 80 com23 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G -> ( ph -> ( ( k o. ( inr |` B ) ) = G -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) ) )
82 81 3ad2ant3 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) -> ( ph -> ( ( k o. ( inr |` B ) ) = G -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) ) )
83 82 impcom 
 |-  ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( k o. ( inr |` B ) ) = G -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
84 83 com12 
 |-  ( ( k o. ( inr |` B ) ) = G -> ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
85 84 3ad2ant3 
 |-  ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) ) )
86 85 impcom 
 |-  ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
87 86 com12 
 |-  ( ( z e. B /\ y = ( inr ` z ) ) -> ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
88 87 rexlimiva 
 |-  ( E. z e. B y = ( inr ` z ) -> ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
89 56 88 jaoi 
 |-  ( ( E. z e. A y = ( inl ` z ) \/ E. z e. B y = ( inr ` z ) ) -> ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
90 djur 
 |-  ( y e. ( A |_| B ) -> ( E. z e. A y = ( inl ` z ) \/ E. z e. B y = ( inr ` z ) ) )
91 89 90 syl11 
 |-  ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( y e. ( A |_| B ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
92 91 ralrimiv 
 |-  ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> A. y e. ( A |_| B ) ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) )
93 ffn 
 |-  ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) Fn ( A |_| B ) )
94 93 3ad2ant1 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) Fn ( A |_| B ) )
95 94 adantl 
 |-  ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) Fn ( A |_| B ) )
96 ffn 
 |-  ( k : ( A |_| B ) --> C -> k Fn ( A |_| B ) )
97 96 3ad2ant1 
 |-  ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> k Fn ( A |_| B ) )
98 eqfnfv 
 |-  ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) Fn ( A |_| B ) /\ k Fn ( A |_| B ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k <-> A. y e. ( A |_| B ) ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
99 95 97 98 syl2an 
 |-  ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k <-> A. y e. ( A |_| B ) ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) ` y ) = ( k ` y ) ) )
100 92 99 mpbird 
 |-  ( ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) /\ ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k )
101 100 ex 
 |-  ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) )
102 101 ralrimivw 
 |-  ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) )
103 24 102 jca 
 |-  ( ( ph /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) ) )
104 103 ex 
 |-  ( ph -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) ) ) )
105 21 22 23 104 mp3and 
 |-  ( ph -> ( ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) : ( A |_| B ) --> C /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inl |` A ) ) = F /\ ( ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> ( x e. ( A |_| B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) ) = k ) ) )
106 8 19 105 rspcedvd 
 |-  ( ph -> E. h e. _V ( ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> h = k ) ) )
107 feq1 
 |-  ( h = k -> ( h : ( A |_| B ) --> C <-> k : ( A |_| B ) --> C ) )
108 coeq1 
 |-  ( h = k -> ( h o. ( inl |` A ) ) = ( k o. ( inl |` A ) ) )
109 108 eqeq1d 
 |-  ( h = k -> ( ( h o. ( inl |` A ) ) = F <-> ( k o. ( inl |` A ) ) = F ) )
110 coeq1 
 |-  ( h = k -> ( h o. ( inr |` B ) ) = ( k o. ( inr |` B ) ) )
111 110 eqeq1d 
 |-  ( h = k -> ( ( h o. ( inr |` B ) ) = G <-> ( k o. ( inr |` B ) ) = G ) )
112 107 109 111 3anbi123d 
 |-  ( h = k -> ( ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) <-> ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) ) )
113 112 reu8 
 |-  ( E! h e. _V ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) <-> E. h e. _V ( ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) /\ A. k e. _V ( ( k : ( A |_| B ) --> C /\ ( k o. ( inl |` A ) ) = F /\ ( k o. ( inr |` B ) ) = G ) -> h = k ) ) )
114 106 113 sylibr 
 |-  ( ph -> E! h e. _V ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) )
115 reuv 
 |-  ( E! h e. _V ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) <-> E! h ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) )
116 114 115 sylib 
 |-  ( ph -> E! h ( h : ( A |_| B ) --> C /\ ( h o. ( inl |` A ) ) = F /\ ( h o. ( inr |` B ) ) = G ) )