Theorem reldmup

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

	Ref	Expression
Assertion	reldmup	Could not format assertion : No typesetting found for |- Rel dom UP with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-up	Could not format 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 ) ) } ) ) : No typesetting found for |- 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 ) ) } ) ) with typecode |-
2	1	reldmmpo	Could not format Rel dom UP : No typesetting found for |- Rel dom UP with typecode |-