psrbaspropd

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

		Ref	Expression
	Hypothesis	psrbaspropd.e	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
	Assertion	psrbaspropd	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psrbaspropd.e	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
2		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4		eqid	⊢ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin }
5		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → 𝐼 ∈ V )
7	2 3 4 5 6	psrbas	⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑_m { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) )
8		eqid	⊢ ( 𝐼 mPwSer 𝑆 ) = ( 𝐼 mPwSer 𝑆 )
9		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) )
11	8 9 4 10 6	psrbas	⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( ( Base ‘ 𝑆 ) ↑_m { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) )
12	1	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
13	12	oveq1d	⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( ( Base ‘ 𝑅 ) ↑_m { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) = ( ( Base ‘ 𝑆 ) ↑_m { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) )
14	11 13	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( ( Base ‘ 𝑅 ) ↑_m { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) )
15	7 14	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐼 ∈ V ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
16		reldmpsr	⊢ Rel dom mPwSer
17	16	ovprc1	⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 mPwSer 𝑅 ) = ∅ )
18	16	ovprc1	⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 mPwSer 𝑆 ) = ∅ )
19	17 18	eqtr4d	⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑆 ) )
20	19	fveq2d	⊢ ( ¬ 𝐼 ∈ V → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐼 ∈ V ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
22	15 21	pm2.61dan	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )

Metamath Proof Explorer

Theorem psrbaspropd

Proof