Metamath Proof Explorer

Theorem setsdm

Description: The domain of a structure with replacement is the domain of the original structure extended by the index of the replacement. (Contributed by AV, 7-Jun-2021)

Ref Expression
Assertion setsdm ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( dom 𝐺 ∪ { 𝐼 } ) )

Proof

Step Hyp Ref Expression
1 opex ⊢ ⟨ 𝐼 , 𝐸 ⟩ ∈ V
2 1 a1i ⊢ ( 𝐸 ∈ 𝑊 → ⟨ 𝐼 , 𝐸 ⟩ ∈ V )
3 setsvalg ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ⟨ 𝐼 , 𝐸 ⟩ ∈ V ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
4 2 3 sylan2 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
5 4 dmeqd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = dom ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
6 dmun ⊢ dom ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) = ( dom ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ dom { ⟨ 𝐼 , 𝐸 ⟩ } )
7 dmres ⊢ dom ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) = ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom 𝐺 )
8 dmsnopg ⊢ ( 𝐸 ∈ 𝑊 → dom { ⟨ 𝐼 , 𝐸 ⟩ } = { 𝐼 } )
9 8 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom { ⟨ 𝐼 , 𝐸 ⟩ } = { 𝐼 } )
10 9 difeq2d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ( V ∖ { 𝐼 } ) )
11 10 ineq1d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom 𝐺 ) = ( ( V ∖ { 𝐼 } ) ∩ dom 𝐺 ) )
12 incom ⊢ ( ( V ∖ { 𝐼 } ) ∩ dom 𝐺 ) = ( dom 𝐺 ∩ ( V ∖ { 𝐼 } ) )
13 invdif ⊢ ( dom 𝐺 ∩ ( V ∖ { 𝐼 } ) ) = ( dom 𝐺 ∖ { 𝐼 } )
14 12 13 eqtri ⊢ ( ( V ∖ { 𝐼 } ) ∩ dom 𝐺 ) = ( dom 𝐺 ∖ { 𝐼 } )
15 11 14 eqtrdi ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom 𝐺 ) = ( dom 𝐺 ∖ { 𝐼 } ) )
16 7 15 eqtrid ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) = ( dom 𝐺 ∖ { 𝐼 } ) )
17 16 9 uneq12d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( dom ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ( ( dom 𝐺 ∖ { 𝐼 } ) ∪ { 𝐼 } ) )
18 6 17 eqtrid ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) = ( ( dom 𝐺 ∖ { 𝐼 } ) ∪ { 𝐼 } ) )
19 undif1 ⊢ ( ( dom 𝐺 ∖ { 𝐼 } ) ∪ { 𝐼 } ) = ( dom 𝐺 ∪ { 𝐼 } )
20 19 a1i ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( dom 𝐺 ∖ { 𝐼 } ) ∪ { 𝐼 } ) = ( dom 𝐺 ∪ { 𝐼 } ) )
21 5 18 20 3eqtrd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( dom 𝐺 ∪ { 𝐼 } ) )