Step | Hyp | Ref
| Expression |
1 | | funfn 6354 |
. . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
2 | | elin 3897 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹)) |
3 | 2 | biancomi 466 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵)) |
4 | 3 | anbi1i 626 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴)) |
5 | | fvres 6664 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑥) = (𝐹‘𝑥)) |
6 | 5 | eleq1d 2874 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴 ↔ (𝐹‘𝑥) ∈ 𝐴)) |
7 | 6 | adantl 485 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) → (((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴 ↔ (𝐹‘𝑥) ∈ 𝐴)) |
8 | 7 | pm5.32i 578 |
. . . . . . 7
⊢ (((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴)) |
9 | 4, 8 | bitri 278 |
. . . . . 6
⊢ ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴)) |
10 | 9 | a1i 11 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴))) |
11 | | an32 645 |
. . . . 5
⊢ (((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵)) |
12 | 10, 11 | syl6bb 290 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
13 | | fnfun 6423 |
. . . . . . 7
⊢ (𝐹 Fn dom 𝐹 → Fun 𝐹) |
14 | | funres 6366 |
. . . . . . 7
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐵)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → Fun (𝐹 ↾ 𝐵)) |
16 | | dmres 5840 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹) |
17 | | df-fn 6327 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝐵) ∧ dom (𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹))) |
18 | 15, 16, 17 | sylanblrc 593 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → (𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹)) |
19 | | elpreima 6805 |
. . . . 5
⊢ ((𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹) → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴))) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴))) |
21 | | elin 3897 |
. . . . 5
⊢ (𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵) ↔ (𝑥 ∈ (◡𝐹 “ 𝐴) ∧ 𝑥 ∈ 𝐵)) |
22 | | elpreima 6805 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡𝐹 “ 𝐴) ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴))) |
23 | 22 | anbi1d 632 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (◡𝐹 “ 𝐴) ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
24 | 21, 23 | syl5bb 286 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
25 | 12, 20, 24 | 3bitr4d 314 |
. . 3
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ 𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵))) |
26 | 1, 25 | sylbi 220 |
. 2
⊢ (Fun
𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ 𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵))) |
27 | 26 | eqrdv 2796 |
1
⊢ (Fun
𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) |