Theorem setsidvald

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

	Ref	Expression
Hypotheses	setsidvald.e	⊢ 𝐸 = Slot 𝑁
	setsidvald.n	⊢ 𝑁 ∈ ℕ
	setsidvald.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	setsidvald.f	⊢ ( 𝜑 → Fun 𝑆 )
	setsidvald.d	⊢ ( 𝜑 → ( 𝐸 ‘ ndx ) ∈ dom 𝑆 )
Assertion	setsidvald	⊢ ( 𝜑 → 𝑆 = ( 𝑆 sSet ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		setsidvald.e	⊢ 𝐸 = Slot 𝑁
2		setsidvald.n	⊢ 𝑁 ∈ ℕ
3		setsidvald.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		setsidvald.f	⊢ ( 𝜑 → Fun 𝑆 )
5		setsidvald.d	⊢ ( 𝜑 → ( 𝐸 ‘ ndx ) ∈ dom 𝑆 )
6		fvex	⊢ ( 𝐸 ‘ 𝑆 ) ∈ V
7		setsval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐸 ‘ 𝑆 ) ∈ V ) → ( 𝑆 sSet ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ } ) )
8	3 6 7	sylancl	⊢ ( 𝜑 → ( 𝑆 sSet ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ } ) )
9	1 2	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
10	9 3	strfvnd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) )
11	10	opeq2d	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ = ⟨ ( 𝐸 ‘ ndx ) , ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) ⟩ )
12	11	sneqd	⊢ ( 𝜑 → { ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ } = { ⟨ ( 𝐸 ‘ ndx ) , ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) ⟩ } )
13	12	uneq2d	⊢ ( 𝜑 → ( ( 𝑆 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ } ) = ( ( 𝑆 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) ⟩ } ) )
14		funresdfunsn	⊢ ( ( Fun 𝑆 ∧ ( 𝐸 ‘ ndx ) ∈ dom 𝑆 ) → ( ( 𝑆 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) ⟩ } ) = 𝑆 )
15	4 5 14	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) ⟩ } ) = 𝑆 )
16	8 13 15	3eqtrrd	⊢ ( 𝜑 → 𝑆 = ( 𝑆 sSet ⟨ ( 𝐸 ‘ ndx ) , ( 𝐸 ‘ 𝑆 ) ⟩ ) )