Theorem reldmopsr

Description: Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015)

	Ref	Expression
Assertion	reldmopsr	⊢ Rel dom ordPwSer

Proof

Step	Hyp	Ref	Expression
1		df-opsr	⊢ ordPwSer = ( 𝑖 ∈ V , 𝑠 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑖 × 𝑖 ) ↦ ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )
2	1	reldmmpo	⊢ Rel dom ordPwSer