Metamath Proof Explorer

Theorem reldmprcof

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

		Ref	Expression
	Assertion	reldmprcof	\|- Rel dom -o.F

Proof

Step	Hyp	Ref	Expression
1		df-prcof	\|- -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 ) ) ) ) >. )
2	1	reldmmpo	\|- Rel dom -o.F

Step

Hyp

Ref

Expression

df-prcof

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

reldmmpo

 |-  Rel dom -o.F