Theorem reldmprds

Description: The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015) (Revised by Thierry Arnoux, 15-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

	Ref	Expression
Assertion	reldmprds	⊢ Rel dom Xs

Proof

Step	Hyp	Ref	Expression
1		df-prds	⊢ Xs = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) )
2	1	reldmmpo	⊢ Rel dom Xs