Theorem dprdwd

Description: A mapping being a finitely supported function in the family S . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019) (Proof shortened by OpenAI, 30-Mar-2020)

	Ref	Expression
Hypotheses	dprdff.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
	dprdff.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dprdff.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	dprdwd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ ( 𝑆 ‘ 𝑥 ) )
	dprdwd.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) finSupp 0 )
Assertion	dprdwd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) ∈ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
2		dprdff.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
3		dprdff.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
4		dprdwd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ ( 𝑆 ‘ 𝑥 ) )
5		dprdwd.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) finSupp 0 )
6		breq1	⊢ ( ℎ = ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) → ( ℎ finSupp 0 ↔ ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) finSupp 0 ) )
7	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝐴 ∈ ( 𝑆 ‘ 𝑥 ) )
8	2 3	dprddomcld	⊢ ( 𝜑 → 𝐼 ∈ V )
9		mptelixpg	⊢ ( 𝐼 ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 𝐴 ∈ ( 𝑆 ‘ 𝑥 ) ) )
10	8 9	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 𝐴 ∈ ( 𝑆 ‘ 𝑥 ) ) )
11	7 10	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 ) )
12		fveq2	⊢ ( 𝑥 = 𝑖 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑖 ) )
13	12	cbvixpv	⊢ X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 ) = X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 )
14	11 13	eleqtrdi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) )
15	6 14 5	elrabd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 } )
16	15 1	eleqtrrdi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) ∈ 𝑊 )