Proof of Theorem setsres
Step | Hyp | Ref
| Expression |
1 | | opex 5166 |
. . . 4
⊢
〈𝐴, 𝐵〉 ∈ V |
2 | | setsvalg 16288 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 〈𝐴, 𝐵〉 ∈ V) → (𝑆 sSet 〈𝐴, 𝐵〉) = ((𝑆 ↾ (V ∖ dom {〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉})) |
3 | 1, 2 | mpan2 681 |
. . 3
⊢ (𝑆 ∈ 𝑉 → (𝑆 sSet 〈𝐴, 𝐵〉) = ((𝑆 ↾ (V ∖ dom {〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉})) |
4 | 3 | reseq1d 5643 |
. 2
⊢ (𝑆 ∈ 𝑉 → ((𝑆 sSet 〈𝐴, 𝐵〉) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ dom {〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉}) ↾ (V ∖ {𝐴}))) |
5 | | resundir 5663 |
. . 3
⊢ (((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ dom {〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) ∪ ({〈𝐴, 𝐵〉} ↾ (V ∖ {𝐴}))) |
6 | | dmsnopss 5863 |
. . . . . . 7
⊢ dom
{〈𝐴, 𝐵〉} ⊆ {𝐴} |
7 | | sscon 3967 |
. . . . . . 7
⊢ (dom
{〈𝐴, 𝐵〉} ⊆ {𝐴} → (V ∖ {𝐴}) ⊆ (V ∖ dom {〈𝐴, 𝐵〉})) |
8 | 6, 7 | ax-mp 5 |
. . . . . 6
⊢ (V
∖ {𝐴}) ⊆ (V
∖ dom {〈𝐴, 𝐵〉}) |
9 | | resabs1 5678 |
. . . . . 6
⊢ ((V
∖ {𝐴}) ⊆ (V
∖ dom {〈𝐴, 𝐵〉}) → ((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |
10 | 8, 9 | ax-mp 5 |
. . . . 5
⊢ ((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴})) |
11 | | dmres 5670 |
. . . . . . 7
⊢ dom
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) = ((V ∖ {𝐴}) ∩ dom {〈𝐴, 𝐵〉}) |
12 | | disj2 4250 |
. . . . . . . 8
⊢ (((V
∖ {𝐴}) ∩ dom
{〈𝐴, 𝐵〉}) = ∅ ↔ (V ∖ {𝐴}) ⊆ (V ∖ dom
{〈𝐴, 𝐵〉})) |
13 | 8, 12 | mpbir 223 |
. . . . . . 7
⊢ ((V
∖ {𝐴}) ∩ dom
{〈𝐴, 𝐵〉}) = ∅ |
14 | 11, 13 | eqtri 2802 |
. . . . . 6
⊢ dom
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) =
∅ |
15 | | relres 5677 |
. . . . . . 7
⊢ Rel
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) |
16 | | reldm0 5590 |
. . . . . . 7
⊢ (Rel
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) → (({〈𝐴, 𝐵〉} ↾ (V ∖ {𝐴})) = ∅ ↔ dom
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) =
∅)) |
17 | 15, 16 | ax-mp 5 |
. . . . . 6
⊢
(({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) = ∅ ↔ dom
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) =
∅) |
18 | 14, 17 | mpbir 223 |
. . . . 5
⊢
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) =
∅ |
19 | 10, 18 | uneq12i 3988 |
. . . 4
⊢ (((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) ∪ ({〈𝐴, 𝐵〉} ↾ (V ∖ {𝐴}))) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ ∅) |
20 | | un0 4193 |
. . . 4
⊢ ((𝑆 ↾ (V ∖ {𝐴})) ∪ ∅) = (𝑆 ↾ (V ∖ {𝐴})) |
21 | 19, 20 | eqtri 2802 |
. . 3
⊢ (((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) ∪ ({〈𝐴, 𝐵〉} ↾ (V ∖ {𝐴}))) = (𝑆 ↾ (V ∖ {𝐴})) |
22 | 5, 21 | eqtri 2802 |
. 2
⊢ (((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉}) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴})) |
23 | 4, 22 | syl6eq 2830 |
1
⊢ (𝑆 ∈ 𝑉 → ((𝑆 sSet 〈𝐴, 𝐵〉) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |