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

Metamath Proof Explorer

Theorem setsvalg

Description: Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion setsvalg ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
2 elex ⊢ ( 𝐴 ∈ 𝑊 → 𝐴 ∈ V )
3 resexg ⊢ ( 𝑆 ∈ V → ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∈ V )
4 3 adantr ⊢ ( ( 𝑆 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∈ V )
5 snex ⊢ { 𝐴 } ∈ V
6 unexg ⊢ ( ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∈ V ∧ { 𝐴 } ∈ V ) → ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) ∈ V )
7 4 5 6 sylancl ⊢ ( ( 𝑆 ∈ V ∧ 𝐴 ∈ V ) → ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) ∈ V )
8 simpl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → 𝑠 = 𝑆 )
9 simpr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → 𝑒 = 𝐴 )
10 9 sneqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → { 𝑒 } = { 𝐴 } )
11 10 dmeqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → dom { 𝑒 } = dom { 𝐴 } )
12 11 difeq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → ( V ∖ dom { 𝑒 } ) = ( V ∖ dom { 𝐴 } ) )
13 8 12 reseq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → ( 𝑠 ↾ ( V ∖ dom { 𝑒 } ) ) = ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) )
14 13 10 uneq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑒 = 𝐴 ) → ( ( 𝑠 ↾ ( V ∖ dom { 𝑒 } ) ) ∪ { 𝑒 } ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )
15 df-sets ⊢ sSet = ( 𝑠 ∈ V , 𝑒 ∈ V ↦ ( ( 𝑠 ↾ ( V ∖ dom { 𝑒 } ) ) ∪ { 𝑒 } ) )
16 14 15 ovmpoga ⊢ ( ( 𝑆 ∈ V ∧ 𝐴 ∈ V ∧ ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) ∈ V ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )
17 7 16 mpd3an3 ⊢ ( ( 𝑆 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )
18 1 2 17 syl2an ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑆 sSet 𝐴 ) = ( ( 𝑆 ↾ ( V ∖ dom { 𝐴 } ) ) ∪ { 𝐴 } ) )