Metamath Proof Explorer

Theorem setsres

Description: The structure replacement function does not affect the value of S away from A . (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion setsres ( 𝑆 ∈ 𝑉 → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
2 setsvalg ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ V ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
3 1 2 mpan2 ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
4 3 reseq1d ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↾ ( V ∖ { 𝐴 } ) ) )
5 resundir ⊢ ( ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↾ ( V ∖ { 𝐴 } ) ) = ( ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) )
6 dmsnopss ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 }
7 sscon ⊢ ( dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 } → ( V ∖ { 𝐴 } ) ⊆ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) )
8 6 7 ax-mp ⊢ ( V ∖ { 𝐴 } ) ⊆ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } )
9 resabs1 ⊢ ( ( V ∖ { 𝐴 } ) ⊆ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) → ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ↾ ( V ∖ { 𝐴 } ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) )
10 8 9 ax-mp ⊢ ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ↾ ( V ∖ { 𝐴 } ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) )
11 dmres ⊢ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = ( ( V ∖ { 𝐴 } ) ∩ dom { ⟨ 𝐴 , 𝐵 ⟩ } )
12 disj2 ⊢ ( ( ( V ∖ { 𝐴 } ) ∩ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) = ∅ ↔ ( V ∖ { 𝐴 } ) ⊆ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) )
13 8 12 mpbir ⊢ ( ( V ∖ { 𝐴 } ) ∩ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) = ∅
14 11 13 eqtri ⊢ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = ∅
15 relres ⊢ Rel ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) )
16 reldm0 ⊢ ( Rel ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = ∅ ↔ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = ∅ ) )
17 15 16 ax-mp ⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = ∅ ↔ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = ∅ )
18 14 17 mpbir ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) = ∅
19 10 18 uneq12i ⊢ ( ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ ∅ )
20 un0 ⊢ ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ ∅ ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) )
21 19 20 eqtri ⊢ ( ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ↾ ( V ∖ { 𝐴 } ) ) ∪ ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( V ∖ { 𝐴 } ) ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) )
22 5 21 eqtri ⊢ ( ( ( 𝑆 ↾ ( V ∖ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↾ ( V ∖ { 𝐴 } ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) )
23 4 22 eqtrdi ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) ↾ ( V ∖ { 𝐴 } ) ) = ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) )