Metamath Proof Explorer

Theorem reldmran

Description: The domain of Ran is a relation. (Contributed by Zhi Wang, 4-Nov-2025)

		Ref	Expression
	Assertion	reldmran	\|- Rel dom Ran

Proof

Step	Hyp	Ref	Expression
1		df-ran	\|- Ran = ( p e. ( _V X. _V ) , e e. _V \|-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) \|-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) )
2	1	reldmmpo	\|- Rel dom Ran

Step

Hyp

Ref

Expression

df-ran

 |-  Ran = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) )

reldmmpo

 |-  Rel dom Ran