Proof of Theorem fveqressseq
| Step | Hyp | Ref
| Expression |
| 1 | | fveqdmss.1 |
. . . 4
⊢ 𝐷 = dom 𝐵 |
| 2 | 1 | fveqdmss 7098 |
. . 3
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → 𝐷 ⊆ dom 𝐴) |
| 3 | | dmres 6030 |
. . . . 5
⊢ dom
(𝐴 ↾ 𝐷) = (𝐷 ∩ dom 𝐴) |
| 4 | | incom 4209 |
. . . . . 6
⊢ (𝐷 ∩ dom 𝐴) = (dom 𝐴 ∩ 𝐷) |
| 5 | | sseqin2 4223 |
. . . . . . 7
⊢ (𝐷 ⊆ dom 𝐴 ↔ (dom 𝐴 ∩ 𝐷) = 𝐷) |
| 6 | 5 | biimpi 216 |
. . . . . 6
⊢ (𝐷 ⊆ dom 𝐴 → (dom 𝐴 ∩ 𝐷) = 𝐷) |
| 7 | 4, 6 | eqtrid 2789 |
. . . . 5
⊢ (𝐷 ⊆ dom 𝐴 → (𝐷 ∩ dom 𝐴) = 𝐷) |
| 8 | 3, 7 | eqtrid 2789 |
. . . 4
⊢ (𝐷 ⊆ dom 𝐴 → dom (𝐴 ↾ 𝐷) = 𝐷) |
| 9 | 8, 1 | eqtrdi 2793 |
. . 3
⊢ (𝐷 ⊆ dom 𝐴 → dom (𝐴 ↾ 𝐷) = dom 𝐵) |
| 10 | 2, 9 | syl 17 |
. 2
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → dom (𝐴 ↾ 𝐷) = dom 𝐵) |
| 11 | | fvres 6925 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ((𝐴 ↾ 𝐷)‘𝑥) = (𝐴‘𝑥)) |
| 12 | 11 | adantl 481 |
. . . . . . 7
⊢ (((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) ∧ 𝑥 ∈ 𝐷) → ((𝐴 ↾ 𝐷)‘𝑥) = (𝐴‘𝑥)) |
| 13 | | id 22 |
. . . . . . 7
⊢ ((𝐴‘𝑥) = (𝐵‘𝑥) → (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 14 | 12, 13 | sylan9eq 2797 |
. . . . . 6
⊢ ((((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) ∧ 𝑥 ∈ 𝐷) ∧ (𝐴‘𝑥) = (𝐵‘𝑥)) → ((𝐴 ↾ 𝐷)‘𝑥) = (𝐵‘𝑥)) |
| 15 | 14 | ex 412 |
. . . . 5
⊢ (((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) ∧ 𝑥 ∈ 𝐷) → ((𝐴‘𝑥) = (𝐵‘𝑥) → ((𝐴 ↾ 𝐷)‘𝑥) = (𝐵‘𝑥))) |
| 16 | 15 | ralimdva 3167 |
. . . 4
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) → (∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥) → ∀𝑥 ∈ 𝐷 ((𝐴 ↾ 𝐷)‘𝑥) = (𝐵‘𝑥))) |
| 17 | 16 | 3impia 1118 |
. . 3
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → ∀𝑥 ∈ 𝐷 ((𝐴 ↾ 𝐷)‘𝑥) = (𝐵‘𝑥)) |
| 18 | 2, 7 | syl 17 |
. . . 4
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → (𝐷 ∩ dom 𝐴) = 𝐷) |
| 19 | 3, 18 | eqtrid 2789 |
. . 3
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → dom (𝐴 ↾ 𝐷) = 𝐷) |
| 20 | 17, 19 | raleqtrrdv 3330 |
. 2
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐷)((𝐴 ↾ 𝐷)‘𝑥) = (𝐵‘𝑥)) |
| 21 | | simpll 767 |
. . . . . . . 8
⊢ (((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) ∧ 𝑥 ∈ 𝐷) → Fun 𝐵) |
| 22 | 1 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ dom 𝐵) |
| 23 | 22 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ dom 𝐵) |
| 24 | 23 | adantl 481 |
. . . . . . . 8
⊢ (((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ dom 𝐵) |
| 25 | | simplr 769 |
. . . . . . . 8
⊢ (((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) ∧ 𝑥 ∈ 𝐷) → ∅ ∉ ran 𝐵) |
| 26 | | nelrnfvne 7097 |
. . . . . . . 8
⊢ ((Fun
𝐵 ∧ 𝑥 ∈ dom 𝐵 ∧ ∅ ∉ ran 𝐵) → (𝐵‘𝑥) ≠ ∅) |
| 27 | 21, 24, 25, 26 | syl3anc 1373 |
. . . . . . 7
⊢ (((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) ∧ 𝑥 ∈ 𝐷) → (𝐵‘𝑥) ≠ ∅) |
| 28 | | neeq1 3003 |
. . . . . . 7
⊢ ((𝐴‘𝑥) = (𝐵‘𝑥) → ((𝐴‘𝑥) ≠ ∅ ↔ (𝐵‘𝑥) ≠ ∅)) |
| 29 | 27, 28 | syl5ibrcom 247 |
. . . . . 6
⊢ (((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) ∧ 𝑥 ∈ 𝐷) → ((𝐴‘𝑥) = (𝐵‘𝑥) → (𝐴‘𝑥) ≠ ∅)) |
| 30 | 29 | ralimdva 3167 |
. . . . 5
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵) → (∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥) → ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) ≠ ∅)) |
| 31 | 30 | 3impia 1118 |
. . . 4
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) ≠ ∅) |
| 32 | | fvn0ssdmfun 7094 |
. . . . 5
⊢
(∀𝑥 ∈
𝐷 (𝐴‘𝑥) ≠ ∅ → (𝐷 ⊆ dom 𝐴 ∧ Fun (𝐴 ↾ 𝐷))) |
| 33 | 32 | simprd 495 |
. . . 4
⊢
(∀𝑥 ∈
𝐷 (𝐴‘𝑥) ≠ ∅ → Fun (𝐴 ↾ 𝐷)) |
| 34 | 31, 33 | syl 17 |
. . 3
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → Fun (𝐴 ↾ 𝐷)) |
| 35 | | simp1 1137 |
. . 3
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → Fun 𝐵) |
| 36 | | eqfunfv 7056 |
. . 3
⊢ ((Fun
(𝐴 ↾ 𝐷) ∧ Fun 𝐵) → ((𝐴 ↾ 𝐷) = 𝐵 ↔ (dom (𝐴 ↾ 𝐷) = dom 𝐵 ∧ ∀𝑥 ∈ dom (𝐴 ↾ 𝐷)((𝐴 ↾ 𝐷)‘𝑥) = (𝐵‘𝑥)))) |
| 37 | 34, 35, 36 | syl2anc 584 |
. 2
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → ((𝐴 ↾ 𝐷) = 𝐵 ↔ (dom (𝐴 ↾ 𝐷) = dom 𝐵 ∧ ∀𝑥 ∈ dom (𝐴 ↾ 𝐷)((𝐴 ↾ 𝐷)‘𝑥) = (𝐵‘𝑥)))) |
| 38 | 10, 20, 37 | mpbir2and 713 |
1
⊢ ((Fun
𝐵 ∧ ∅ ∉ ran
𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → (𝐴 ↾ 𝐷) = 𝐵) |