Theorem reldmprcof

Description: The domain of -o.F is a relation. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Assertion	reldmprcof	Could not format assertion : No typesetting found for |- Rel dom -o.F with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-prcof	Could not format -o.F = ( p e. _V , f e. _V |-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. ) : No typesetting found for |- -o.F = ( p e. _V , f e. _V |-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. ) with typecode |-
2	1	reldmmpo	Could not format Rel dom -o.F : No typesetting found for |- Rel dom -o.F with typecode |-