Theorem psrbaspropd

Description: Property deduction for power series base set. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypothesis	psrbaspropd.e	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_S$$
Assertion	psrbaspropd	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$

Proof

Step	Hyp	Ref	Expression
1		psrbaspropd.e	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_S$$
2		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4		eqid	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
5		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
6		simpr	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to I\in \mathrm{V}$$
7	2 3 4 5 6	psrbas	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={{\mathrm{Base}}_R}^{\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
8		eqid	$$⊢I\mathrm{mPwSer}S=I\mathrm{mPwSer}S$$
9		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
10		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
11	8 9 4 10 6	psrbas	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={{\mathrm{Base}}_S}^{\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
12	1	adantr	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_R={\mathrm{Base}}_S$$
13	12	oveq1d	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {{\mathrm{Base}}_R}^{\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}={{\mathrm{Base}}_S}^{\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
14	11 13	eqtr4d	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={{\mathrm{Base}}_R}^{\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
15	7 14	eqtr4d	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
16		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
17	16	ovprc1	$$⊢\neg I\in \mathrm{V}\to I\mathrm{mPwSer}R=\varnothing$$
18	16	ovprc1	$$⊢\neg I\in \mathrm{V}\to I\mathrm{mPwSer}S=\varnothing$$
19	17 18	eqtr4d	$$⊢\neg I\in \mathrm{V}\to I\mathrm{mPwSer}R=I\mathrm{mPwSer}S$$
20	19	fveq2d	$$⊢\neg I\in \mathrm{V}\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
21	20	adantl	$$⊢\left(\phi \wedge \neg I\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
22	15 21	pm2.61dan	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$