Step | Hyp | Ref
| Expression |
1 | | opex 5425 |
. . . 4
⊢
⟨𝐴, 𝐵⟩ ∈ V |
2 | | setsvalg 17046 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ ⟨𝐴, 𝐵⟩ ∈ V) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩})) |
3 | 1, 2 | mpan2 690 |
. . 3
⊢ (𝑆 ∈ 𝑉 → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩})) |
4 | 3 | reseq1d 5940 |
. 2
⊢ (𝑆 ∈ 𝑉 → ((𝑆 sSet ⟨𝐴, 𝐵⟩) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩}) ↾ (V ∖ {𝐴}))) |
5 | | resundir 5956 |
. . 3
⊢ (((𝑆 ↾ (V ∖ dom
{⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ dom {⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴}))) |
6 | | dmsnopss 6170 |
. . . . . . 7
⊢ dom
{⟨𝐴, 𝐵⟩} ⊆ {𝐴} |
7 | | sscon 4102 |
. . . . . . 7
⊢ (dom
{⟨𝐴, 𝐵⟩} ⊆ {𝐴} → (V ∖ {𝐴}) ⊆ (V ∖ dom {⟨𝐴, 𝐵⟩})) |
8 | 6, 7 | ax-mp 5 |
. . . . . 6
⊢ (V
∖ {𝐴}) ⊆ (V
∖ dom {⟨𝐴, 𝐵⟩}) |
9 | | resabs1 5971 |
. . . . . 6
⊢ ((V
∖ {𝐴}) ⊆ (V
∖ dom {⟨𝐴, 𝐵⟩}) → ((𝑆 ↾ (V ∖ dom
{⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |
10 | 8, 9 | ax-mp 5 |
. . . . 5
⊢ ((𝑆 ↾ (V ∖ dom
{⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴})) |
11 | | dmres 5963 |
. . . . . . 7
⊢ dom
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) = ((V ∖ {𝐴}) ∩ dom {⟨𝐴, 𝐵⟩}) |
12 | | disj2 4421 |
. . . . . . . 8
⊢ (((V
∖ {𝐴}) ∩ dom
{⟨𝐴, 𝐵⟩}) = ∅ ↔ (V ∖ {𝐴}) ⊆ (V ∖ dom
{⟨𝐴, 𝐵⟩})) |
13 | 8, 12 | mpbir 230 |
. . . . . . 7
⊢ ((V
∖ {𝐴}) ∩ dom
{⟨𝐴, 𝐵⟩}) = ∅ |
14 | 11, 13 | eqtri 2761 |
. . . . . 6
⊢ dom
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) =
∅ |
15 | | relres 5970 |
. . . . . . 7
⊢ Rel
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) |
16 | | reldm0 5887 |
. . . . . . 7
⊢ (Rel
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) → (({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴})) = ∅ ↔ dom
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) =
∅)) |
17 | 15, 16 | ax-mp 5 |
. . . . . 6
⊢
(({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) = ∅ ↔ dom
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) =
∅) |
18 | 14, 17 | mpbir 230 |
. . . . 5
⊢
({⟨𝐴, 𝐵⟩} ↾ (V ∖
{𝐴})) =
∅ |
19 | 10, 18 | uneq12i 4125 |
. . . 4
⊢ (((𝑆 ↾ (V ∖ dom
{⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴}))) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ ∅) |
20 | | un0 4354 |
. . . 4
⊢ ((𝑆 ↾ (V ∖ {𝐴})) ∪ ∅) = (𝑆 ↾ (V ∖ {𝐴})) |
21 | 19, 20 | eqtri 2761 |
. . 3
⊢ (((𝑆 ↾ (V ∖ dom
{⟨𝐴, 𝐵⟩})) ↾ (V ∖ {𝐴})) ∪ ({⟨𝐴, 𝐵⟩} ↾ (V ∖ {𝐴}))) = (𝑆 ↾ (V ∖ {𝐴})) |
22 | 5, 21 | eqtri 2761 |
. 2
⊢ (((𝑆 ↾ (V ∖ dom
{⟨𝐴, 𝐵⟩})) ∪ {⟨𝐴, 𝐵⟩}) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴})) |
23 | 4, 22 | eqtrdi 2789 |
1
⊢ (𝑆 ∈ 𝑉 → ((𝑆 sSet ⟨𝐴, 𝐵⟩) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |