Theorem reldmopsr

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

	Ref	Expression
Assertion	reldmopsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{ordPwSer}$$

Proof

Step	Hyp	Ref	Expression
1		df-opsr	$$⊢\mathrm{ordPwSer}=\left(i\in \mathrm{V},s\in \mathrm{V}⟼\left(r\in 𝒫\left(i\times i\right)⟼⦋\left(i\mathrm{mPwSer}s\right)/p⦌\left(p\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq {\mathrm{Base}}_p\wedge \left(\underset{\dot{}}{[}\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}/d\underset{\dot{}}{]}\exists z\in d\left(x\left(z\right){<}_{s}y\left(z\right)\wedge \forall w\in d\left(w\left(r{<}_{bag}i\right)z\to x\left(w\right)=y\left(w\right)\right)\right)\vee x=y\right)\right)\right\}⟩\right)\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{ordPwSer}$$