This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = i ∈ V , s ∈ V ⟼ r ∈ 𝒫 i × i ⟼ ⦋ i mPwSer s / p⦌ p sSet ≤ ndx x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ ordPwSer