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)

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 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ∅ )
21 reldmsets ⊢ Rel dom sSet
22 21 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) = ∅ )
23 22 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) = ( 𝐸 ‘ ∅ ) )
24 19 20 23 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) ) )
25 18 24 pm2.61i ⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ 𝐷 , 𝐶 ⟩ ) )