Step | Hyp | Ref
| Expression |
1 | | opex 5457 |
. . . . 5
⊢
⟨𝐼, 𝐸⟩ ∈ V |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝐸 ∈ 𝑊 → ⟨𝐼, 𝐸⟩ ∈ V) |
3 | | setsvalg 17081 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ ⟨𝐼, 𝐸⟩ ∈ V) → (𝐺 sSet ⟨𝐼, 𝐸⟩) = ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
4 | 2, 3 | sylan2 593 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝐺 sSet ⟨𝐼, 𝐸⟩) = ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
5 | 4 | dmeqd 5897 |
. 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) = dom ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
6 | | dmun 5902 |
. . 3
⊢ dom
((𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) = (dom (𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ dom {⟨𝐼, 𝐸⟩}) |
7 | | dmres 5995 |
. . . . 5
⊢ dom
(𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) = ((V ∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom 𝐺) |
8 | | dmsnopg 6201 |
. . . . . . . . 9
⊢ (𝐸 ∈ 𝑊 → dom {⟨𝐼, 𝐸⟩} = {𝐼}) |
9 | 8 | adantl 482 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom {⟨𝐼, 𝐸⟩} = {𝐼}) |
10 | 9 | difeq2d 4118 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (V ∖ dom {⟨𝐼, 𝐸⟩}) = (V ∖ {𝐼})) |
11 | 10 | ineq1d 4207 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((V ∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom 𝐺) = ((V ∖ {𝐼}) ∩ dom 𝐺)) |
12 | | incom 4197 |
. . . . . . 7
⊢ ((V
∖ {𝐼}) ∩ dom
𝐺) = (dom 𝐺 ∩ (V ∖ {𝐼})) |
13 | | invdif 4264 |
. . . . . . 7
⊢ (dom
𝐺 ∩ (V ∖ {𝐼})) = (dom 𝐺 ∖ {𝐼}) |
14 | 12, 13 | eqtri 2759 |
. . . . . 6
⊢ ((V
∖ {𝐼}) ∩ dom
𝐺) = (dom 𝐺 ∖ {𝐼}) |
15 | 11, 14 | eqtrdi 2787 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((V ∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom 𝐺) = (dom 𝐺 ∖ {𝐼})) |
16 | 7, 15 | eqtrid 2783 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom (𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) = (dom 𝐺 ∖ {𝐼})) |
17 | 16, 9 | uneq12d 4160 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom (𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ dom {⟨𝐼, 𝐸⟩}) = ((dom 𝐺 ∖ {𝐼}) ∪ {𝐼})) |
18 | 6, 17 | eqtrid 2783 |
. 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) = ((dom 𝐺 ∖ {𝐼}) ∪ {𝐼})) |
19 | | undif1 4471 |
. . 3
⊢ ((dom
𝐺 ∖ {𝐼}) ∪ {𝐼}) = (dom 𝐺 ∪ {𝐼}) |
20 | 19 | a1i 11 |
. 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((dom 𝐺 ∖ {𝐼}) ∪ {𝐼}) = (dom 𝐺 ∪ {𝐼})) |
21 | 5, 18, 20 | 3eqtrd 2775 |
1
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) = (dom 𝐺 ∪ {𝐼})) |