Step | Hyp | Ref
| Expression |
1 | | opexg 4228 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ⟨𝐴, 𝐵⟩ ∈ V) |
2 | | setsvalg 12491 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ ⟨𝐴, 𝐵⟩ ∈ V) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩})) |
3 | 1, 2 | sylan2 286 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋)) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩})) |
4 | 3 | 3impb 1199 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩})) |
5 | 4 | reseq1d 4906 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝑆 sSet ⟨𝐴, 𝐵⟩) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩}) ↾ (V ∖ {𝐴}))) |
6 | | resundir 4921 |
. . 3
⊢ (((𝑆 ↾ (V ∖ dom
{⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴}))) |
7 | | dmsnopg 5100 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑋 → dom {⟨𝐴, 𝐵⟩} = {𝐴}) |
8 | 7 | 3ad2ant3 1020 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → dom {⟨𝐴, 𝐵⟩} = {𝐴}) |
9 | | eqimss 3209 |
. . . . . . . 8
⊢ (dom
{⟨𝐴, 𝐵⟩} = {𝐴} → dom {⟨𝐴, 𝐵⟩} ⊆ {𝐴}) |
10 | 8, 9 | syl 14 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → dom {⟨𝐴, 𝐵⟩} ⊆ {𝐴}) |
11 | 10 | sscond 3272 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (V ∖ {𝐴}) ⊆ (V ∖ dom {⟨𝐴, 𝐵⟩})) |
12 | | resabs1 4936 |
. . . . . 6
⊢ ((V
∖ {𝐴}) ⊆ (V
∖ dom {⟨𝐴, 𝐵⟩}) → ((𝑆 ↾ (V ∖ dom
{⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |
14 | | dmres 4928 |
. . . . . . 7
⊢ dom
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) = ((V ∖ {𝐴}) ∩ dom {⟨𝐴, 𝐵⟩}) |
15 | | disj2 3478 |
. . . . . . . 8
⊢ (((V
∖ {𝐴}) ∩ dom
{⟨𝐴, 𝐵⟩}) = ∅ ↔ (V ∖ {𝐴}) ⊆ (V ∖ dom
{⟨𝐴, 𝐵⟩})) |
16 | 11, 15 | sylibr 134 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((V ∖ {𝐴}) ∩ dom {⟨𝐴, 𝐵⟩}) = ∅) |
17 | 14, 16 | eqtrid 2222 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → dom ({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴})) = ∅) |
18 | | relres 4935 |
. . . . . . 7
⊢ Rel
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) |
19 | | reldm0 4845 |
. . . . . . 7
⊢ (Rel
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) → (({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴})) = ∅ ↔ dom
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) =
∅)) |
20 | 18, 19 | ax-mp 5 |
. . . . . 6
⊢
(({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) = ∅ ↔ dom
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) =
∅) |
21 | 17, 20 | sylibr 134 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴})) = ∅) |
22 | 13, 21 | uneq12d 3290 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴}))) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ ∅)) |
23 | | un0 3456 |
. . . 4
⊢ ((𝑆 ↾ (V ∖ {𝐴})) ∪ ∅) = (𝑆 ↾ (V ∖ {𝐴})) |
24 | 22, 23 | eqtrdi 2226 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴}))) = (𝑆 ↾ (V ∖ {𝐴}))) |
25 | 6, 24 | eqtrid 2222 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩}) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |
26 | 5, 25 | eqtrd 2210 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝑆 sSet ⟨𝐴, 𝐵⟩) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |