Theorem reldmran

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

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

Proof

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