Theorem setsidvaldOLD

Description: Obsolete version of setsidvald as of 17-Oct-2024. (Contributed by AV, 14-Mar-2020) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		setsidvaldOLD.e	⊢ 𝐸 = Slot 𝑁
2		setsidvaldOLD.n	⊢ 𝑁 ∈ ℕ
3		setsidvaldOLD.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		setsidvaldOLD.f	⊢ ( 𝜑 → Fun 𝑆 )
5		setsidvaldOLD.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 ) , ( 𝐸 ‘ 𝑆 ) ⟩ ) )