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

Metamath Proof Explorer

Theorem dprdfcl

Description: A finitely supported function in S has its X -th element in S ( X ) . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

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
dprdff.3 ⊢ φ → F ∈ W
Assertion dprdfcl ⊢ φ ∧ X ∈ I → F ⁡ X ∈ S ⁡ X

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 dprdff.3 ⊢ φ → F ∈ W
5 1 2 3 dprdw ⊢ φ → F ∈ W ↔ F Fn I ∧ ∀ x ∈ I F ⁡ x ∈ S ⁡ x ∧ finSupp 0 ˙⁡ F
6 4 5 mpbid ⊢ φ → F Fn I ∧ ∀ x ∈ I F ⁡ x ∈ S ⁡ x ∧ finSupp 0 ˙⁡ F
7 6 simp2d ⊢ φ → ∀ x ∈ I F ⁡ x ∈ S ⁡ x
8 fveq2 ⊢ x = X → F ⁡ x = F ⁡ X
9 fveq2 ⊢ x = X → S ⁡ x = S ⁡ X
10 8 9 eleq12d ⊢ x = X → F ⁡ x ∈ S ⁡ x ↔ F ⁡ X ∈ S ⁡ X
11 10 rspccva ⊢ ∀ x ∈ I F ⁡ x ∈ S ⁡ x ∧ X ∈ I → F ⁡ X ∈ S ⁡ X
12 7 11 sylan ⊢ φ ∧ X ∈ I → F ⁡ X ∈ S ⁡ X