| Step | Hyp | Ref
| Expression |
| 1 | | funfn 6596 |
. . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
| 2 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹)) |
| 3 | 2 | biancomi 462 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵)) |
| 4 | 3 | anbi1i 624 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴)) |
| 5 | | fvres 6925 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑥) = (𝐹‘𝑥)) |
| 6 | 5 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴 ↔ (𝐹‘𝑥) ∈ 𝐴)) |
| 7 | 6 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) → (((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴 ↔ (𝐹‘𝑥) ∈ 𝐴)) |
| 8 | 7 | pm5.32i 574 |
. . . . . . 7
⊢ (((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴)) |
| 9 | 4, 8 | bitri 275 |
. . . . . 6
⊢ ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴)) |
| 10 | 9 | a1i 11 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴))) |
| 11 | | an32 646 |
. . . . 5
⊢ (((𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵)) |
| 12 | 10, 11 | bitrdi 287 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
| 13 | | fnfun 6668 |
. . . . . . 7
⊢ (𝐹 Fn dom 𝐹 → Fun 𝐹) |
| 14 | 13 | funresd 6609 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → Fun (𝐹 ↾ 𝐵)) |
| 15 | | dmres 6030 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹) |
| 16 | | df-fn 6564 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝐵) ∧ dom (𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹))) |
| 17 | 14, 15, 16 | sylanblrc 590 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → (𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹)) |
| 18 | | elpreima 7078 |
. . . . 5
⊢ ((𝐹 ↾ 𝐵) Fn (𝐵 ∩ dom 𝐹) → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴))) |
| 19 | 17, 18 | syl 17 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ (𝑥 ∈ (𝐵 ∩ dom 𝐹) ∧ ((𝐹 ↾ 𝐵)‘𝑥) ∈ 𝐴))) |
| 20 | | elin 3967 |
. . . . 5
⊢ (𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵) ↔ (𝑥 ∈ (◡𝐹 “ 𝐴) ∧ 𝑥 ∈ 𝐵)) |
| 21 | | elpreima 7078 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡𝐹 “ 𝐴) ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴))) |
| 22 | 21 | anbi1d 631 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((𝑥 ∈ (◡𝐹 “ 𝐴) ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
| 23 | 20, 22 | bitrid 283 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐴) ∧ 𝑥 ∈ 𝐵))) |
| 24 | 12, 19, 23 | 3bitr4d 311 |
. . 3
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ 𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵))) |
| 25 | 1, 24 | sylbi 217 |
. 2
⊢ (Fun
𝐹 → (𝑥 ∈ (◡(𝐹 ↾ 𝐵) “ 𝐴) ↔ 𝑥 ∈ ((◡𝐹 “ 𝐴) ∩ 𝐵))) |
| 26 | 25 | eqrdv 2735 |
1
⊢ (Fun
𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) |