Theorem reldmlan

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

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

Proof

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