Metamath Proof Explorer

Theorem setsidvald

Description: Value of the structure replacement function, deduction version. (Contributed by AV, 14-Mar-2020)

Ref Expression
Hypotheses setsidvald.e ⊢ E = Slot N
setsidvald.n ⊢ N ∈ ℕ
setsidvald.s ⊢ φ → S ∈ V
setsidvald.f ⊢ φ → Fun ⁡ S
setsidvald.d ⊢ φ → E ⁡ ndx ∈ dom ⁡ S
Assertion setsidvald ⊢ φ → S = S sSet E ⁡ ndx E ⁡ S

Proof

Step Hyp Ref Expression
1 setsidvald.e ⊢ E = Slot N
2 setsidvald.n ⊢ N ∈ ℕ
3 setsidvald.s ⊢ φ → S ∈ V
4 setsidvald.f ⊢ φ → Fun ⁡ S
5 setsidvald.d ⊢ φ → E ⁡ ndx ∈ dom ⁡ S
6 fvex ⊢ E ⁡ S ∈ V
7 setsval ⊢ S ∈ V ∧ E ⁡ S ∈ V → S sSet E ⁡ ndx E ⁡ S = S ↾ V ∖ E ⁡ ndx ∪ E ⁡ ndx E ⁡ S
8 3 6 7 sylancl ⊢ φ → S sSet E ⁡ ndx E ⁡ S = S ↾ V ∖ E ⁡ ndx ∪ E ⁡ ndx E ⁡ S
9 1 2 ndxid ⊢ E = Slot E ⁡ ndx
10 9 3 strfvnd ⊢ φ → E ⁡ S = S ⁡ E ⁡ ndx
11 10 opeq2d ⊢ φ → E ⁡ ndx E ⁡ S = E ⁡ ndx S ⁡ E ⁡ ndx
12 11 sneqd ⊢ φ → E ⁡ ndx E ⁡ S = E ⁡ ndx S ⁡ E ⁡ ndx
13 12 uneq2d ⊢ φ → S ↾ V ∖ E ⁡ ndx ∪ E ⁡ ndx E ⁡ S = S ↾ V ∖ E ⁡ ndx ∪ E ⁡ ndx S ⁡ E ⁡ ndx
14 funresdfunsn ⊢ Fun ⁡ S ∧ E ⁡ ndx ∈ dom ⁡ S → S ↾ V ∖ E ⁡ ndx ∪ E ⁡ ndx S ⁡ E ⁡ ndx = S
15 4 5 14 syl2anc ⊢ φ → S ↾ V ∖ E ⁡ ndx ∪ E ⁡ ndx S ⁡ E ⁡ ndx = S
16 8 13 15 3eqtrrd ⊢ φ → S = S sSet E ⁡ ndx E ⁡ S