Theorem opsrval2

Description: Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	opsrval2.s	$$⊢S=I\mathrm{mPwSer}R$$
	opsrval2.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
	opsrval2.l	$$⊢\underset{\dot{}}{\le }={\le }_O$$
	opsrval2.i	$$⊢\phi \to I\in V$$
	opsrval2.r	$$⊢\phi \to R\in W$$
	opsrval2.t	$$⊢\phi \to T\subseteq I\times I$$
Assertion	opsrval2	$$⊢\phi \to O=S\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$

Proof

Step	Hyp	Ref	Expression
1		opsrval2.s	$$⊢S=I\mathrm{mPwSer}R$$
2		opsrval2.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
3		opsrval2.l	$$⊢\underset{\dot{}}{\le }={\le }_O$$
4		opsrval2.i	$$⊢\phi \to I\in V$$
5		opsrval2.r	$$⊢\phi \to R\in W$$
6		opsrval2.t	$$⊢\phi \to T\subseteq I\times I$$
7		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
8		eqid	$$⊢{<}_R={<}_R$$
9		eqid	$$⊢T{<}_{bag}I=T{<}_{bag}I$$
10		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
11		eqid	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq {\mathrm{Base}}_S\wedge \left(\exists z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(x\left(z\right){<}_{R}y\left(z\right)\wedge \forall w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(w\left(T{<}_{bag}I\right)z\to x\left(w\right)=y\left(w\right)\right)\right)\vee x=y\right)\right)\right\}=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq {\mathrm{Base}}_S\wedge \left(\exists z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(x\left(z\right){<}_{R}y\left(z\right)\wedge \forall w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(w\left(T{<}_{bag}I\right)z\to x\left(w\right)=y\left(w\right)\right)\right)\vee x=y\right)\right)\right\}$$
12	1 2 7 8 9 10 11 4 5 6	opsrval	$$⊢\phi \to O=S\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq {\mathrm{Base}}_S\wedge \left(\exists z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(x\left(z\right){<}_{R}y\left(z\right)\wedge \forall w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(w\left(T{<}_{bag}I\right)z\to x\left(w\right)=y\left(w\right)\right)\right)\vee x=y\right)\right)\right\}⟩$$
13	1 2 7 8 9 10 3 6	opsrle	$$⊢\phi \to \underset{\dot{}}{\le }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq {\mathrm{Base}}_S\wedge \left(\exists z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(x\left(z\right){<}_{R}y\left(z\right)\wedge \forall w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(w\left(T{<}_{bag}I\right)z\to x\left(w\right)=y\left(w\right)\right)\right)\vee x=y\right)\right)\right\}$$
14	13	opeq2d	$$⊢\phi \to ⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩=⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq {\mathrm{Base}}_S\wedge \left(\exists z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(x\left(z\right){<}_{R}y\left(z\right)\wedge \forall w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(w\left(T{<}_{bag}I\right)z\to x\left(w\right)=y\left(w\right)\right)\right)\vee x=y\right)\right)\right\}⟩$$
15	14	oveq2d	$$⊢\phi \to S\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩=S\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq {\mathrm{Base}}_S\wedge \left(\exists z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(x\left(z\right){<}_{R}y\left(z\right)\wedge \forall w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(w\left(T{<}_{bag}I\right)z\to x\left(w\right)=y\left(w\right)\right)\right)\vee x=y\right)\right)\right\}⟩$$
16	12 15	eqtr4d	$$⊢\phi \to O=S\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$