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 = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ( ( 𝑑 FuncCat 𝑒 ) UP ( 𝑐 FuncCat 𝑒 ) ) 𝑥 ) ) )
2	1	reldmmpo	⊢ Rel dom Lan