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

Metamath Proof Explorer

Theorem setsnid

Description: Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 7-Nov-2024)

Ref Expression
Hypotheses setsid.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
setsnid.n ⊢ ( 𝐸 ‘ ndx ) ≠ 𝐷
Assertion setsnid ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) )

Proof

Step Hyp Ref Expression
1 setsid.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
2 setsnid.n ⊢ ( 𝐸 ‘ ndx ) ≠ 𝐷
3 id ⊢ ( 𝑊 ∈ V → 𝑊 ∈ V )
4 1 3 strfvnd ⊢ ( 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
5 ovex ⊢ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ∈ V
6 5 1 strfvn ⊢ ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) )
7 setsres ⊢ ( 𝑊 ∈ V → ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) = ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) )
8 7 fveq1d ⊢ ( 𝑊 ∈ V → ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) )
9 fvex ⊢ ( 𝐸 ‘ ndx ) ∈ V
10 eldifsn ⊢ ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) ↔ ( ( 𝐸 ‘ ndx ) ∈ V ∧ ( 𝐸 ‘ ndx ) ≠ 𝐷 ) )
11 9 2 10 mpbir2an ⊢ ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } )
12 fvres ⊢ ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) → ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) ) )
13 11 12 ax-mp ⊢ ( ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) )
14 fvres ⊢ ( ( 𝐸 ‘ ndx ) ∈ ( V ∖ { 𝐷 } ) → ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
15 11 14 ax-mp ⊢ ( ( 𝑊 ↾ ( V ∖ { 𝐷 } ) ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) )
16 8 13 15 3eqtr3g ⊢ ( 𝑊 ∈ V → ( ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
17 6 16 eqtrid ⊢ ( 𝑊 ∈ V → ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) = ( 𝑊 ‘ ( 𝐸 ‘ ndx ) ) )
18 4 17 eqtr4d ⊢ ( 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) )
19 1 str0 ⊢ ∅ = ( 𝐸 ‘ ∅ )
20 19 eqcomi ⊢ ( 𝐸 ‘ ∅ ) = ∅
21 eqid ⊢ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) = ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ )
22 reldmsets ⊢ Rel dom sSet
23 20 21 22 oveqprc ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) )
24 18 23 pm2.61i ⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) )