Step | Hyp | Ref
| Expression |
1 | | funfn 4931 |
. . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
2 | | elin 3126 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹)) |
3 | | ancom 253 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵)) |
4 | 2, 3 | bitri 173 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵)) |
5 | 4 | anbi1i 431 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴)) |
6 | | fvres 5198 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑥) = (𝐹‘𝑥)) |
7 | 6 | eleq1d 2106 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴 ↔ (𝐹‘𝑥) ∈ 𝐴)) |
8 | 7 | adantl 262 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) → (((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴 ↔ (𝐹‘𝑥) ∈ 𝐴)) |
9 | 8 | pm5.32i 427 |
. . . . . . 7
⊢ (((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴)) |
10 | 5, 9 | bitri 173 |
. . . . . 6
⊢ ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴)) |
11 | 10 | a1i 9 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴))) |
12 | | an32 496 |
. . . . 5
⊢ (((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵)) |
13 | 11, 12 | syl6bb 185 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
14 | | fnfun 4996 |
. . . . . . . 8
⊢ (𝐹 Fn dom 𝐹 → Fun 𝐹) |
15 | | funres 4941 |
. . . . . . . 8
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐵)) |
16 | 14, 15 | syl 14 |
. . . . . . 7
⊢ (𝐹 Fn dom 𝐹 → Fun (𝐹 ↾ 𝐵)) |
17 | | dmres 4632 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹) |
18 | 16, 17 | jctir 296 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → (Fun (𝐹 ↾ 𝐵) ∧ dom (𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹))) |
19 | | df-fn 4905 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝐵) ∧ dom (𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹))) |
20 | 18, 19 | sylibr 137 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → (𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹)) |
21 | | elpreima 5286 |
. . . . 5
⊢ ((𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹) → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴))) |
22 | 20, 21 | syl 14 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴))) |
23 | | elin 3126 |
. . . . 5
⊢ (𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵) ↔ (𝑥 ∈ (◡𝐹 “ 𝐴) ∧ 𝑥 ∈ 𝐵)) |
24 | | elpreima 5286 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡𝐹 “ 𝐴) ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴))) |
25 | 24 | anbi1d 438 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (◡𝐹 “ 𝐴) ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
26 | 23, 25 | syl5bb 181 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
27 | 13, 22, 26 | 3bitr4d 209 |
. . 3
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ 𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵))) |
28 | 1, 27 | sylbi 114 |
. 2
⊢ (Fun
𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ 𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵))) |
29 | 28 | eqrdv 2038 |
1
⊢ (Fun
𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) |