Proof of Theorem fvsnun1
Step | Hyp | Ref
| Expression |
1 | | fvsnun.3 |
. . . . 5
⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
2 | 1 | reseq1i 5313 |
. . . 4
⊢ (𝐺 ↾ {𝐴}) = (({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ {𝐴}) |
3 | | resundir 5331 |
. . . . 5
⊢
(({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ {𝐴}) = (({〈𝐴, 𝐵〉} ↾ {𝐴}) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ {𝐴})) |
4 | | incom 3767 |
. . . . . . . . 9
⊢ ((𝐶 ∖ {𝐴}) ∩ {𝐴}) = ({𝐴} ∩ (𝐶 ∖ {𝐴})) |
5 | | disjdif 3992 |
. . . . . . . . 9
⊢ ({𝐴} ∩ (𝐶 ∖ {𝐴})) = ∅ |
6 | 4, 5 | eqtri 2632 |
. . . . . . . 8
⊢ ((𝐶 ∖ {𝐴}) ∩ {𝐴}) = ∅ |
7 | | resdisj 5482 |
. . . . . . . 8
⊢ (((𝐶 ∖ {𝐴}) ∩ {𝐴}) = ∅ → ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ {𝐴}) = ∅) |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ {𝐴}) = ∅ |
9 | 8 | uneq2i 3726 |
. . . . . 6
⊢
(({〈𝐴, 𝐵〉} ↾ {𝐴}) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ {𝐴})) = (({〈𝐴, 𝐵〉} ↾ {𝐴}) ∪ ∅) |
10 | | un0 3919 |
. . . . . 6
⊢
(({〈𝐴, 𝐵〉} ↾ {𝐴}) ∪ ∅) =
({〈𝐴, 𝐵〉} ↾ {𝐴}) |
11 | 9, 10 | eqtri 2632 |
. . . . 5
⊢
(({〈𝐴, 𝐵〉} ↾ {𝐴}) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ {𝐴})) = ({〈𝐴, 𝐵〉} ↾ {𝐴}) |
12 | 3, 11 | eqtri 2632 |
. . . 4
⊢
(({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ {𝐴}) = ({〈𝐴, 𝐵〉} ↾ {𝐴}) |
13 | 2, 12 | eqtri 2632 |
. . 3
⊢ (𝐺 ↾ {𝐴}) = ({〈𝐴, 𝐵〉} ↾ {𝐴}) |
14 | 13 | fveq1i 6104 |
. 2
⊢ ((𝐺 ↾ {𝐴})‘𝐴) = (({〈𝐴, 𝐵〉} ↾ {𝐴})‘𝐴) |
15 | | fvsnun.1 |
. . . 4
⊢ 𝐴 ∈ V |
16 | 15 | snid 4155 |
. . 3
⊢ 𝐴 ∈ {𝐴} |
17 | | fvres 6117 |
. . 3
⊢ (𝐴 ∈ {𝐴} → ((𝐺 ↾ {𝐴})‘𝐴) = (𝐺‘𝐴)) |
18 | 16, 17 | ax-mp 5 |
. 2
⊢ ((𝐺 ↾ {𝐴})‘𝐴) = (𝐺‘𝐴) |
19 | | fvres 6117 |
. . . 4
⊢ (𝐴 ∈ {𝐴} → (({〈𝐴, 𝐵〉} ↾ {𝐴})‘𝐴) = ({〈𝐴, 𝐵〉}‘𝐴)) |
20 | 16, 19 | ax-mp 5 |
. . 3
⊢
(({〈𝐴, 𝐵〉} ↾ {𝐴})‘𝐴) = ({〈𝐴, 𝐵〉}‘𝐴) |
21 | | fvsnun.2 |
. . . 4
⊢ 𝐵 ∈ V |
22 | 15, 21 | fvsn 6351 |
. . 3
⊢
({〈𝐴, 𝐵〉}‘𝐴) = 𝐵 |
23 | 20, 22 | eqtri 2632 |
. 2
⊢
(({〈𝐴, 𝐵〉} ↾ {𝐴})‘𝐴) = 𝐵 |
24 | 14, 18, 23 | 3eqtr3i 2640 |
1
⊢ (𝐺‘𝐴) = 𝐵 |