Step | Hyp | Ref
| Expression |
1 | | funfn 5201 |
. . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
2 | | elin 3290 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹)) |
3 | | ancom 264 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵)) |
4 | 2, 3 | bitri 183 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵)) |
5 | 4 | anbi1i 454 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴)) |
6 | | fvres 5493 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑥) = (𝐹‘𝑥)) |
7 | 6 | eleq1d 2226 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴 ↔ (𝐹‘𝑥) ∈ 𝐴)) |
8 | 7 | adantl 275 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) → (((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴 ↔ (𝐹‘𝑥) ∈ 𝐴)) |
9 | 8 | pm5.32i 450 |
. . . . . . 7
⊢ (((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴)) |
10 | 5, 9 | bitri 183 |
. . . . . 6
⊢ ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴)) |
11 | 10 | a1i 9 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴))) |
12 | | an32 552 |
. . . . 5
⊢ (((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵)) |
13 | 11, 12 | bitrdi 195 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
14 | | fnfun 5268 |
. . . . . . . 8
⊢ (𝐹 Fn dom 𝐹 → Fun 𝐹) |
15 | | funres 5212 |
. . . . . . . 8
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐵)) |
16 | 14, 15 | syl 14 |
. . . . . . 7
⊢ (𝐹 Fn dom 𝐹 → Fun (𝐹 ↾ 𝐵)) |
17 | | dmres 4888 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹) |
18 | 16, 17 | jctir 311 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → (Fun (𝐹 ↾ 𝐵) ∧ dom (𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹))) |
19 | | df-fn 5174 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝐵) ∧ dom (𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹))) |
20 | 18, 19 | sylibr 133 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → (𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹)) |
21 | | elpreima 5587 |
. . . . 5
⊢ ((𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹) → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴))) |
22 | 20, 21 | syl 14 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴))) |
23 | | elin 3290 |
. . . . 5
⊢ (𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵) ↔ (𝑥 ∈ (◡𝐹 “ 𝐴) ∧ 𝑥 ∈ 𝐵)) |
24 | | elpreima 5587 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡𝐹 “ 𝐴) ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴))) |
25 | 24 | anbi1d 461 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (◡𝐹 “ 𝐴) ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
26 | 23, 25 | syl5bb 191 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
27 | 13, 22, 26 | 3bitr4d 219 |
. . 3
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ 𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵))) |
28 | 1, 27 | sylbi 120 |
. 2
⊢ (Fun
𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ 𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵))) |
29 | 28 | eqrdv 2155 |
1
⊢ (Fun
𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) |