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

Metamath Proof Explorer

Theorem updjud

Proof