reldmup

Description: The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025)

		Ref	Expression
	Assertion	reldmup	\|- Rel dom UP

Proof

Step	Hyp	Ref	Expression
1		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 ) ) } ) )
2	1	reldmmpo	\|- Rel dom UP

Step

Hyp

Ref

Expression

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

reldmmpo

 |-  Rel dom UP

Metamath Proof Explorer

Theorem reldmup

Proof