Metamath Proof Explorer

Theorem upfval

Description: Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025) (Proof shortened by Zhi Wang, 12-Nov-2025)

Ref Expression
Hypotheses upfval.b 
|- B = ( Base ` D )
upfval.c 
|- C = ( Base ` E )
upfval.h 
|- H = ( Hom ` D )
upfval.j 
|- J = ( Hom ` E )
upfval.o 
|- O = ( comp ` E )
Assertion upfval 
|- ( D UP E ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } )

Proof

Step Hyp Ref Expression
1 upfval.b 
 |-  B = ( Base ` D )
2 upfval.c 
 |-  C = ( Base ` E )
3 upfval.h 
 |-  H = ( Hom ` D )
4 upfval.j 
 |-  J = ( Hom ` E )
5 upfval.o 
 |-  O = ( comp ` E )
6 fvexd 
 |-  ( ( d = D /\ e = E ) -> ( Base ` d ) e. _V )
7 fveq2 
 |-  ( d = D -> ( Base ` d ) = ( Base ` D ) )
8 7 adantr 
 |-  ( ( d = D /\ e = E ) -> ( Base ` d ) = ( Base ` D ) )
9 8 1 eqtr4di 
 |-  ( ( d = D /\ e = E ) -> ( Base ` d ) = B )
10 fvexd 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) e. _V )
11 simplr 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> e = E )
12 11 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = ( Base ` E ) )
13 12 2 eqtr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = C )
14 fvexd 
 |-  ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) -> ( Hom ` d ) e. _V )
15 simplll 
 |-  ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) -> d = D )
16 15 fveq2d 
 |-  ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) -> ( Hom ` d ) = ( Hom ` D ) )
17 16 3 eqtr4di 
 |-  ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) -> ( Hom ` d ) = H )
18 fvexd 
 |-  ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) -> ( Hom ` e ) e. _V )
19 simp-4r 
 |-  ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) -> e = E )
20 19 fveq2d 
 |-  ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) -> ( Hom ` e ) = ( Hom ` E ) )
21 20 4 eqtr4di 
 |-  ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) -> ( Hom ` e ) = J )
22 fvexd 
 |-  ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) -> ( comp ` e ) e. _V )
23 simp-5r 
 |-  ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) -> e = E )
24 23 fveq2d 
 |-  ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) -> ( comp ` e ) = ( comp ` E ) )
25 24 5 eqtr4di 
 |-  ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) -> ( comp ` e ) = O )
26 simp-6l 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> d = D )
27 simp-6r 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> e = E )
28 26 27 oveq12d 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( d Func e ) = ( D Func E ) )
29 simp-4r 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> c = C )
30 simp-5r 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> b = B )
31 30 eleq2d 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( x e. b <-> x e. B ) )
32 simplr 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> j = J )
33 32 oveqd 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( w j ( ( 1st ` f ) ` x ) ) = ( w J ( ( 1st ` f ) ` x ) ) )
34 33 eleq2d 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( m e. ( w j ( ( 1st ` f ) ` x ) ) <-> m e. ( w J ( ( 1st ` f ) ` x ) ) ) )
35 31 34 anbi12d 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) <-> ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) ) )
36 32 oveqd 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( w j ( ( 1st ` f ) ` y ) ) = ( w J ( ( 1st ` f ) ` y ) ) )
37 simplr 
 |-  ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) -> h = H )
38 37 oveqdr 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( x h y ) = ( x H y ) )
39 simpr 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> o = O )
40 39 oveqd 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) = ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) )
41 40 oveqd 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) )
42 41 eqeq2d 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) <-> g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) )
43 38 42 reueqbidv 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) <-> E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) )
44 36 43 raleqbidv 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) <-> A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) )
45 30 44 raleqbidv 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) <-> A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) )
46 35 45 anbi12d 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) <-> ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) ) )
47 46 opabbidv 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } = { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } )
48 28 29 47 mpoeq123dv 
 |-  ( ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) /\ o = O ) -> ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) )
49 22 25 48 csbied2 
 |-  ( ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) /\ j = J ) -> [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) )
50 18 21 49 csbied2 
 |-  ( ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) /\ h = H ) -> [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) )
51 14 17 50 csbied2 
 |-  ( ( ( ( d = D /\ e = E ) /\ b = B ) /\ c = C ) -> [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) )
52 10 13 51 csbied2 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) )
53 6 9 52 csbied2 
 |-  ( ( d = D /\ e = E ) -> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) )
54 df-up 
 |-  UP = ( d e. _V , e e. _V |-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) )
55 ovex 
 |-  ( D Func E ) e. _V
56 2 fvexi 
 |-  C e. _V
57 55 56 mpoex 
 |-  ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) e. _V
58 53 54 57 ovmpoa 
 |-  ( ( D e. _V /\ E e. _V ) -> ( D UP E ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) )
59 reldmup 
 |-  Rel dom UP
60 59 ovprc 
 |-  ( -. ( D e. _V /\ E e. _V ) -> ( D UP E ) = (/) )
61 reldmfunc 
 |-  Rel dom Func
62 61 ovprc 
 |-  ( -. ( D e. _V /\ E e. _V ) -> ( D Func E ) = (/) )
63 62 orcd 
 |-  ( -. ( D e. _V /\ E e. _V ) -> ( ( D Func E ) = (/) \/ C = (/) ) )
64 0mpo0 
 |-  ( ( ( D Func E ) = (/) \/ C = (/) ) -> ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) = (/) )
65 63 64 syl 
 |-  ( -. ( D e. _V /\ E e. _V ) -> ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) = (/) )
66 60 65 eqtr4d 
 |-  ( -. ( D e. _V /\ E e. _V ) -> ( D UP E ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } ) )
67 58 66 pm2.61i 
 |-  ( D UP E ) = ( f e. ( D Func E ) , w e. C |-> { <. x , m >. | ( ( x e. B /\ m e. ( w J ( ( 1st ` f ) ` x ) ) ) /\ A. y e. B A. g e. ( w J ( ( 1st ` f ) ` y ) ) E! k e. ( x H y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. O ( ( 1st ` f ) ` y ) ) m ) ) } )