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 ⊢ W = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
dprdff.1 ⊢ φ → G dom ⁡ DProd S
dprdff.2 ⊢ φ → dom ⁡ S = I
dprdwd.3 ⊢ φ ∧ x ∈ I → A ∈ S ⁡ x
dprdwd.4 ⊢ φ → finSupp 0 ˙⁡ x ∈ I ⟼ A
Assertion dprdwd ⊢ φ → x ∈ I ⟼ A ∈ W

Proof

Step Hyp Ref Expression
1 dprdff.w ⊢ W = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
2 dprdff.1 ⊢ φ → G dom ⁡ DProd S
3 dprdff.2 ⊢ φ → dom ⁡ S = I
4 dprdwd.3 ⊢ φ ∧ x ∈ I → A ∈ S ⁡ x
5 dprdwd.4 ⊢ φ → finSupp 0 ˙⁡ x ∈ I ⟼ A
6 breq1 ⊢ h = x ∈ I ⟼ A → finSupp 0 ˙⁡ h ↔ finSupp 0 ˙⁡ x ∈ I ⟼ A
7 4 ralrimiva ⊢ φ → ∀ x ∈ I A ∈ S ⁡ x
8 2 3 dprddomcld ⊢ φ → I ∈ V
9 mptelixpg ⊢ I ∈ V → x ∈ I ⟼ A ∈ ⨉ x ∈ I S ⁡ x ↔ ∀ x ∈ I A ∈ S ⁡ x
10 8 9 syl ⊢ φ → x ∈ I ⟼ A ∈ ⨉ x ∈ I S ⁡ x ↔ ∀ x ∈ I A ∈ S ⁡ x
11 7 10 mpbird ⊢ φ → x ∈ I ⟼ A ∈ ⨉ x ∈ I S ⁡ x
12 fveq2 ⊢ x = i → S ⁡ x = S ⁡ i
13 12 cbvixpv ⊢ ⨉ x ∈ I S ⁡ x = ⨉ i ∈ I S ⁡ i
14 11 13 eleqtrdi ⊢ φ → x ∈ I ⟼ A ∈ ⨉ i ∈ I S ⁡ i
15 6 14 5 elrabd ⊢ φ → x ∈ I ⟼ A ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
16 15 1 eleqtrrdi ⊢ φ → x ∈ I ⟼ A ∈ W