This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐴 ) ∈ 𝑊 )