Proof of Theorem setsres
| Step | Hyp | Ref
| Expression |
| 1 | | opex 5469 |
. . . 4
⊢
〈𝐴, 𝐵〉 ∈ V |
| 2 | | setsvalg 17203 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 〈𝐴, 𝐵〉 ∈ V) → (𝑆 sSet 〈𝐴, 𝐵〉) = ((𝑆 ↾ (V ∖ dom {〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉})) |
| 3 | 1, 2 | mpan2 691 |
. . 3
⊢ (𝑆 ∈ 𝑉 → (𝑆 sSet 〈𝐴, 𝐵〉) = ((𝑆 ↾ (V ∖ dom {〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉})) |
| 4 | 3 | reseq1d 5996 |
. 2
⊢ (𝑆 ∈ 𝑉 → ((𝑆 sSet 〈𝐴, 𝐵〉) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ dom {〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉}) ↾ (V ∖ {𝐴}))) |
| 5 | | resundir 6012 |
. . 3
⊢ (((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ dom {〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) ∪ ({〈𝐴, 𝐵〉} ↾ (V ∖ {𝐴}))) |
| 6 | | dmsnopss 6234 |
. . . . . . 7
⊢ dom
{〈𝐴, 𝐵〉} ⊆ {𝐴} |
| 7 | | sscon 4143 |
. . . . . . 7
⊢ (dom
{〈𝐴, 𝐵〉} ⊆ {𝐴} → (V ∖ {𝐴}) ⊆ (V ∖ dom {〈𝐴, 𝐵〉})) |
| 8 | 6, 7 | ax-mp 5 |
. . . . . 6
⊢ (V
∖ {𝐴}) ⊆ (V
∖ dom {〈𝐴, 𝐵〉}) |
| 9 | | resabs1 6024 |
. . . . . 6
⊢ ((V
∖ {𝐴}) ⊆ (V
∖ dom {〈𝐴, 𝐵〉}) → ((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |
| 10 | 8, 9 | ax-mp 5 |
. . . . 5
⊢ ((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴})) |
| 11 | | dmres 6030 |
. . . . . . 7
⊢ dom
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) = ((V ∖ {𝐴}) ∩ dom {〈𝐴, 𝐵〉}) |
| 12 | | disj2 4458 |
. . . . . . . 8
⊢ (((V
∖ {𝐴}) ∩ dom
{〈𝐴, 𝐵〉}) = ∅ ↔ (V ∖ {𝐴}) ⊆ (V ∖ dom
{〈𝐴, 𝐵〉})) |
| 13 | 8, 12 | mpbir 231 |
. . . . . . 7
⊢ ((V
∖ {𝐴}) ∩ dom
{〈𝐴, 𝐵〉}) = ∅ |
| 14 | 11, 13 | eqtri 2765 |
. . . . . 6
⊢ dom
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) =
∅ |
| 15 | | relres 6023 |
. . . . . . 7
⊢ Rel
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) |
| 16 | | reldm0 5938 |
. . . . . . 7
⊢ (Rel
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) → (({〈𝐴, 𝐵〉} ↾ (V ∖ {𝐴})) = ∅ ↔ dom
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) =
∅)) |
| 17 | 15, 16 | ax-mp 5 |
. . . . . 6
⊢
(({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) = ∅ ↔ dom
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) =
∅) |
| 18 | 14, 17 | mpbir 231 |
. . . . 5
⊢
({〈𝐴, 𝐵〉} ↾ (V ∖
{𝐴})) =
∅ |
| 19 | 10, 18 | uneq12i 4166 |
. . . 4
⊢ (((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) ∪ ({〈𝐴, 𝐵〉} ↾ (V ∖ {𝐴}))) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ ∅) |
| 20 | | un0 4394 |
. . . 4
⊢ ((𝑆 ↾ (V ∖ {𝐴})) ∪ ∅) = (𝑆 ↾ (V ∖ {𝐴})) |
| 21 | 19, 20 | eqtri 2765 |
. . 3
⊢ (((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ↾ (V ∖ {𝐴})) ∪ ({〈𝐴, 𝐵〉} ↾ (V ∖ {𝐴}))) = (𝑆 ↾ (V ∖ {𝐴})) |
| 22 | 5, 21 | eqtri 2765 |
. 2
⊢ (((𝑆 ↾ (V ∖ dom
{〈𝐴, 𝐵〉})) ∪ {〈𝐴, 𝐵〉}) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴})) |
| 23 | 4, 22 | eqtrdi 2793 |
1
⊢ (𝑆 ∈ 𝑉 → ((𝑆 sSet 〈𝐴, 𝐵〉) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) |