Proof of Theorem ffvresb
Step | Hyp | Ref
| Expression |
1 | | fdm 4993 |
. . . . . 6
⊢ ((𝐹 ↾ A):A⟶B
→ dom (𝐹 ↾
A) = A) |
2 | | dmres 4575 |
. . . . . . 7
⊢ dom
(𝐹 ↾ A) = (A ∩
dom 𝐹) |
3 | | inss2 3152 |
. . . . . . 7
⊢ (A ∩ dom 𝐹) ⊆ dom 𝐹 |
4 | 2, 3 | eqsstri 2969 |
. . . . . 6
⊢ dom
(𝐹 ↾ A) ⊆ dom 𝐹 |
5 | 1, 4 | syl6eqssr 2990 |
. . . . 5
⊢ ((𝐹 ↾ A):A⟶B
→ A ⊆ dom 𝐹) |
6 | 5 | sselda 2939 |
. . . 4
⊢ (((𝐹 ↾ A):A⟶B ∧ x ∈ A) →
x ∈ dom
𝐹) |
7 | | fvres 5141 |
. . . . . 6
⊢ (x ∈ A → ((𝐹 ↾ A)‘x) =
(𝐹‘x)) |
8 | 7 | adantl 262 |
. . . . 5
⊢ (((𝐹 ↾ A):A⟶B ∧ x ∈ A) →
((𝐹 ↾ A)‘x) =
(𝐹‘x)) |
9 | | ffvelrn 5243 |
. . . . 5
⊢ (((𝐹 ↾ A):A⟶B ∧ x ∈ A) →
((𝐹 ↾ A)‘x)
∈ B) |
10 | 8, 9 | eqeltrrd 2112 |
. . . 4
⊢ (((𝐹 ↾ A):A⟶B ∧ x ∈ A) →
(𝐹‘x) ∈ B) |
11 | 6, 10 | jca 290 |
. . 3
⊢ (((𝐹 ↾ A):A⟶B ∧ x ∈ A) →
(x ∈ dom
𝐹 ∧ (𝐹‘x) ∈ B)) |
12 | 11 | ralrimiva 2386 |
. 2
⊢ ((𝐹 ↾ A):A⟶B
→ ∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B)) |
13 | | simpl 102 |
. . . . . . 7
⊢
((x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B) → x
∈ dom 𝐹) |
14 | 13 | ralimi 2378 |
. . . . . 6
⊢ (∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B) → ∀x ∈ A x ∈ dom 𝐹) |
15 | | dfss3 2929 |
. . . . . 6
⊢ (A ⊆ dom 𝐹 ↔ ∀x ∈ A x ∈ dom 𝐹) |
16 | 14, 15 | sylibr 137 |
. . . . 5
⊢ (∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B) → A
⊆ dom 𝐹) |
17 | | funfn 4874 |
. . . . . 6
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
18 | | fnssres 4955 |
. . . . . 6
⊢ ((𝐹 Fn dom 𝐹 ∧ A ⊆ dom 𝐹) → (𝐹 ↾ A) Fn A) |
19 | 17, 18 | sylanb 268 |
. . . . 5
⊢ ((Fun
𝐹 ∧ A ⊆ dom
𝐹) → (𝐹 ↾ A) Fn A) |
20 | 16, 19 | sylan2 270 |
. . . 4
⊢ ((Fun
𝐹 ∧ ∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B)) → (𝐹 ↾ A) Fn A) |
21 | | simpr 103 |
. . . . . . . 8
⊢
((x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B) → (𝐹‘x) ∈ B) |
22 | 7 | eleq1d 2103 |
. . . . . . . 8
⊢ (x ∈ A → (((𝐹 ↾ A)‘x)
∈ B
↔ (𝐹‘x) ∈ B)) |
23 | 21, 22 | syl5ibr 145 |
. . . . . . 7
⊢ (x ∈ A → ((x
∈ dom 𝐹 ∧ (𝐹‘x) ∈ B) → ((𝐹 ↾ A)‘x)
∈ B)) |
24 | 23 | ralimia 2376 |
. . . . . 6
⊢ (∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B) → ∀x ∈ A ((𝐹 ↾ A)‘x)
∈ B) |
25 | 24 | adantl 262 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B)) → ∀x ∈ A ((𝐹 ↾ A)‘x)
∈ B) |
26 | | fnfvrnss 5268 |
. . . . 5
⊢ (((𝐹 ↾ A) Fn A ∧ ∀x ∈ A ((𝐹 ↾ A)‘x)
∈ B)
→ ran (𝐹 ↾
A) ⊆ B) |
27 | 20, 25, 26 | syl2anc 391 |
. . . 4
⊢ ((Fun
𝐹 ∧ ∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B)) → ran (𝐹 ↾ A) ⊆ B) |
28 | | df-f 4849 |
. . . 4
⊢ ((𝐹 ↾ A):A⟶B
↔ ((𝐹 ↾ A) Fn A ∧ ran (𝐹 ↾ A) ⊆ B)) |
29 | 20, 27, 28 | sylanbrc 394 |
. . 3
⊢ ((Fun
𝐹 ∧ ∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B)) → (𝐹 ↾ A):A⟶B) |
30 | 29 | ex 108 |
. 2
⊢ (Fun
𝐹 → (∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B) → (𝐹 ↾ A):A⟶B)) |
31 | 12, 30 | impbid2 131 |
1
⊢ (Fun
𝐹 → ((𝐹 ↾ A):A⟶B
↔ ∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B))) |