This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uppropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same universal pairs. (Contributed by Zhi Wang, 20-Nov-2025)

Ref Expression
Hypotheses uppropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
uppropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
uppropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
uppropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
uppropd.a 
|- ( ph -> A e. V )
uppropd.b 
|- ( ph -> B e. V )
uppropd.c 
|- ( ph -> C e. V )
uppropd.d 
|- ( ph -> D e. V )
Assertion uppropd 
|- ( ph -> ( A UP C ) = ( B UP D ) )

Proof

Step Hyp Ref Expression
1 uppropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 uppropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 uppropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 uppropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 uppropd.a 
 |-  ( ph -> A e. V )
6 uppropd.b 
 |-  ( ph -> B e. V )
7 uppropd.c 
 |-  ( ph -> C e. V )
8 uppropd.d 
 |-  ( ph -> D e. V )
9 1 2 3 4 5 6 7 8 funcpropd 
 |-  ( ph -> ( A Func C ) = ( B Func D ) )
10 3 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
11 10 adantr 
 |-  ( ( ph /\ f e. ( A Func C ) ) -> ( Base ` C ) = ( Base ` D ) )
12 1 homfeqbas 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
13 12 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( Base ` A ) = ( Base ` B ) )
14 13 adantr 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) -> ( Base ` A ) = ( Base ` B ) )
15 eqid 
 |-  ( Base ` C ) = ( Base ` C )
16 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
17 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
18 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) -> ( Homf ` C ) = ( Homf ` D ) )
19 simprr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> w e. ( Base ` C ) )
20 19 ad2antrr 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) -> w e. ( Base ` C ) )
21 eqid 
 |-  ( Base ` A ) = ( Base ` A )
22 simprl 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> f e. ( A Func C ) )
23 22 func1st2nd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( 1st ` f ) ( A Func C ) ( 2nd ` f ) )
24 21 15 23 funcf1 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( 1st ` f ) : ( Base ` A ) --> ( Base ` C ) )
25 24 adantr 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) -> ( 1st ` f ) : ( Base ` A ) --> ( Base ` C ) )
26 25 ffvelcdmda 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) -> ( ( 1st ` f ) ` y ) e. ( Base ` C ) )
27 15 16 17 18 20 26 homfeqval 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) -> ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) = ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) )
28 eqid 
 |-  ( Hom ` A ) = ( Hom ` A )
29 eqid 
 |-  ( Hom ` B ) = ( Hom ` B )
30 1 ad4antr 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) -> ( Homf ` A ) = ( Homf ` B ) )
31 simprl 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) -> x e. ( Base ` A ) )
32 31 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) -> x e. ( Base ` A ) )
33 simplr 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) -> y e. ( Base ` A ) )
34 21 28 29 30 32 33 homfeqval 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) -> ( x ( Hom ` A ) y ) = ( x ( Hom ` B ) y ) )
35 eqid 
 |-  ( comp ` C ) = ( comp ` C )
36 eqid 
 |-  ( comp ` D ) = ( comp ` D )
37 18 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> ( Homf ` C ) = ( Homf ` D ) )
38 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> ( comf ` C ) = ( comf ` D ) )
39 20 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> w e. ( Base ` C ) )
40 24 ffvelcdmda 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ x e. ( Base ` A ) ) -> ( ( 1st ` f ) ` x ) e. ( Base ` C ) )
41 40 adantrr 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) -> ( ( 1st ` f ) ` x ) e. ( Base ` C ) )
42 41 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> ( ( 1st ` f ) ` x ) e. ( Base ` C ) )
43 26 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> ( ( 1st ` f ) ` y ) e. ( Base ` C ) )
44 simprr 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) -> m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) )
45 44 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) )
46 23 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) -> ( 1st ` f ) ( A Func C ) ( 2nd ` f ) )
47 21 28 16 46 32 33 funcf2 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) -> ( x ( 2nd ` f ) y ) : ( x ( Hom ` A ) y ) --> ( ( ( 1st ` f ) ` x ) ( Hom ` C ) ( ( 1st ` f ) ` y ) ) )
48 47 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> ( ( x ( 2nd ` f ) y ) ` k ) e. ( ( ( 1st ` f ) ` x ) ( Hom ` C ) ( ( 1st ` f ) ` y ) ) )
49 15 16 35 36 37 38 39 42 43 45 48 comfeqval 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) )
50 49 eqeq2d 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) /\ k e. ( x ( Hom ` A ) y ) ) -> ( g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) <-> g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) )
51 34 50 reueqbidva 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) /\ g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) ) -> ( E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) <-> E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) )
52 27 51 raleqbidva 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) /\ y e. ( Base ` A ) ) -> ( A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) <-> A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) )
53 14 52 raleqbidva 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) ) -> ( A. y e. ( Base ` A ) A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) <-> A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) )
54 53 pm5.32da 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` A ) A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) ) <-> ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) ) )
55 3 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ x e. ( Base ` A ) ) -> ( Homf ` C ) = ( Homf ` D ) )
56 simplrr 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ x e. ( Base ` A ) ) -> w e. ( Base ` C ) )
57 15 16 17 55 56 40 homfeqval 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ x e. ( Base ` A ) ) -> ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) = ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) )
58 57 eleq2d 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) /\ x e. ( Base ` A ) ) -> ( m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) <-> m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) )
59 58 pm5.32da 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) <-> ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) ) )
60 13 eleq2d 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( x e. ( Base ` A ) <-> x e. ( Base ` B ) ) )
61 60 anbi1d 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) <-> ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) ) )
62 59 61 bitrd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) <-> ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) ) )
63 62 anbi1d 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) <-> ( ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) ) )
64 54 63 bitrd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> ( ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` A ) A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) ) <-> ( ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) ) )
65 64 opabbidv 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ w e. ( Base ` C ) ) ) -> { <. x , m >. | ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` A ) A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) ) } = { <. x , m >. | ( ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) } )
66 9 11 65 mpoeq123dva 
 |-  ( ph -> ( f e. ( A Func C ) , w e. ( Base ` C ) |-> { <. x , m >. | ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` A ) A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) ) } ) = ( f e. ( B Func D ) , w e. ( Base ` D ) |-> { <. x , m >. | ( ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) } ) )
67 21 15 28 16 35 upfval 
 |-  ( A UP C ) = ( f e. ( A Func C ) , w e. ( Base ` C ) |-> { <. x , m >. | ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` A ) A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) ) } )
68 eqid 
 |-  ( Base ` B ) = ( Base ` B )
69 eqid 
 |-  ( Base ` D ) = ( Base ` D )
70 68 69 29 17 36 upfval 
 |-  ( B UP D ) = ( f e. ( B Func D ) , w e. ( Base ` D ) |-> { <. x , m >. | ( ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) } )
71 66 67 70 3eqtr4g 
 |-  ( ph -> ( A UP C ) = ( B UP D ) )