Theorem reldmup

Description: The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025)

	Ref	Expression
Assertion	reldmup	⊢ Rel dom UP

Proof

Step	Hyp	Ref	Expression
1		df-up	⊢ UP = ( 𝑑 ∈ V , 𝑒 ∈ V ↦ ⦋ ( Base ‘ 𝑑 ) / 𝑏 ⦌ ⦋ ( Base ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( Hom ‘ 𝑑 ) / ℎ ⦌ ⦋ ( Hom ‘ 𝑒 ) / 𝑗 ⦌ ⦋ ( comp ‘ 𝑒 ) / 𝑜 ⦌ ( 𝑓 ∈ ( 𝑑 Func 𝑒 ) , 𝑤 ∈ 𝑐 ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑚 ∈ ( 𝑤 𝑗 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑔 ∈ ( 𝑤 𝑗 ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ℎ 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ 𝑜 ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
2	1	reldmmpo	⊢ Rel dom UP