Metamath Proof Explorer

Theorem reldmxpcALT

Description: Alternate proof of reldmxpc . (Contributed by Zhi Wang, 15-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	reldmxpcALT	⊢ Rel dom ×_c

Proof

Step	Hyp	Ref	Expression
1		df-xpc	⊢ ×_c = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ ⦋ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) ) ) ) / ℎ ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )
2	1	reldmmpo	⊢ Rel dom ×_c