Metamath Proof Explorer

Theorem reldmlan

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

		Ref	Expression
	Assertion	reldmlan	\|- Rel dom Lan

Proof

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

Step

Hyp

Ref

Expression

df-lan

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

reldmmpo

 |-  Rel dom Lan