Theorem reldmprcof

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

	Ref	Expression
Assertion	reldmprcof	⊢ Rel dom −∘F

Proof

Step	Hyp	Ref	Expression
1		df-prcof	⊢ −∘F = ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ )
2	1	reldmmpo	⊢ Rel dom −∘F