Step | Hyp | Ref
| Expression |
1 | | funfn 4874 |
. . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
2 | | elin 3120 |
. . . . . . . . 9
⊢ (x ∈ (B ∩ dom 𝐹) ↔ (x ∈ B ∧ x ∈ dom 𝐹)) |
3 | | ancom 253 |
. . . . . . . . 9
⊢
((x ∈ B ∧ x ∈ dom 𝐹) ↔ (x ∈ dom 𝐹 ∧ x ∈ B)) |
4 | 2, 3 | bitri 173 |
. . . . . . . 8
⊢ (x ∈ (B ∩ dom 𝐹) ↔ (x ∈ dom 𝐹 ∧ x ∈ B)) |
5 | 4 | anbi1i 431 |
. . . . . . 7
⊢
((x ∈ (B ∩ dom
𝐹) ∧ ((𝐹 ↾ B)‘x)
∈ A)
↔ ((x ∈ dom 𝐹 ∧ x ∈ B) ∧ ((𝐹 ↾ B)‘x)
∈ A)) |
6 | | fvres 5141 |
. . . . . . . . . 10
⊢ (x ∈ B → ((𝐹 ↾ B)‘x) =
(𝐹‘x)) |
7 | 6 | eleq1d 2103 |
. . . . . . . . 9
⊢ (x ∈ B → (((𝐹 ↾ B)‘x)
∈ A
↔ (𝐹‘x) ∈ A)) |
8 | 7 | adantl 262 |
. . . . . . . 8
⊢
((x ∈ dom 𝐹 ∧ x ∈ B) → (((𝐹 ↾ B)‘x)
∈ A
↔ (𝐹‘x) ∈ A)) |
9 | 8 | pm5.32i 427 |
. . . . . . 7
⊢
(((x ∈ dom 𝐹 ∧ x ∈ B) ∧ ((𝐹 ↾ B)‘x)
∈ A)
↔ ((x ∈ dom 𝐹 ∧ x ∈ B) ∧ (𝐹‘x) ∈ A)) |
10 | 5, 9 | bitri 173 |
. . . . . 6
⊢
((x ∈ (B ∩ dom
𝐹) ∧ ((𝐹 ↾ B)‘x)
∈ A)
↔ ((x ∈ dom 𝐹 ∧ x ∈ B) ∧ (𝐹‘x) ∈ A)) |
11 | 10 | a1i 9 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((x ∈ (B ∩ dom 𝐹) ∧ ((𝐹 ↾ B)‘x)
∈ A)
↔ ((x ∈ dom 𝐹 ∧ x ∈ B) ∧ (𝐹‘x) ∈ A))) |
12 | | an32 496 |
. . . . 5
⊢
(((x ∈ dom 𝐹 ∧ x ∈ B) ∧ (𝐹‘x) ∈ A) ↔ ((x
∈ dom 𝐹 ∧ (𝐹‘x) ∈ A) ∧ x ∈ B)) |
13 | 11, 12 | syl6bb 185 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → ((x ∈ (B ∩ dom 𝐹) ∧ ((𝐹 ↾ B)‘x)
∈ A)
↔ ((x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ A) ∧ x ∈ B))) |
14 | | fnfun 4939 |
. . . . . . . 8
⊢ (𝐹 Fn dom 𝐹 → Fun 𝐹) |
15 | | funres 4884 |
. . . . . . . 8
⊢ (Fun
𝐹 → Fun (𝐹 ↾ B)) |
16 | 14, 15 | syl 14 |
. . . . . . 7
⊢ (𝐹 Fn dom 𝐹 → Fun (𝐹 ↾ B)) |
17 | | dmres 4575 |
. . . . . . 7
⊢ dom
(𝐹 ↾ B) = (B ∩
dom 𝐹) |
18 | 16, 17 | jctir 296 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → (Fun (𝐹 ↾ B) ∧ dom (𝐹 ↾ B) = (B ∩
dom 𝐹))) |
19 | | df-fn 4848 |
. . . . . 6
⊢ ((𝐹 ↾ B) Fn (B ∩
dom 𝐹) ↔ (Fun (𝐹 ↾ B) ∧ dom (𝐹 ↾ B) = (B ∩
dom 𝐹))) |
20 | 18, 19 | sylibr 137 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → (𝐹 ↾ B) Fn (B ∩
dom 𝐹)) |
21 | | elpreima 5229 |
. . . . 5
⊢ ((𝐹 ↾ B) Fn (B ∩
dom 𝐹) → (x ∈ (◡(𝐹 ↾ B) “ A)
↔ (x ∈ (B ∩ dom
𝐹) ∧ ((𝐹 ↾ B)‘x)
∈ A))) |
22 | 20, 21 | syl 14 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (x ∈ (◡(𝐹 ↾ B) “ A)
↔ (x ∈ (B ∩ dom
𝐹) ∧ ((𝐹 ↾ B)‘x)
∈ A))) |
23 | | elin 3120 |
. . . . 5
⊢ (x ∈ ((◡𝐹 “ A) ∩ B)
↔ (x ∈ (◡𝐹 “ A) ∧ x ∈ B)) |
24 | | elpreima 5229 |
. . . . . 6
⊢ (𝐹 Fn dom 𝐹 → (x ∈ (◡𝐹 “ A) ↔ (x
∈ dom 𝐹 ∧ (𝐹‘x) ∈ A))) |
25 | 24 | anbi1d 438 |
. . . . 5
⊢ (𝐹 Fn dom 𝐹 → ((x ∈ (◡𝐹 “ A) ∧ x ∈ B) ↔ ((x
∈ dom 𝐹 ∧ (𝐹‘x) ∈ A) ∧ x ∈ B))) |
26 | 23, 25 | syl5bb 181 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (x ∈ ((◡𝐹 “ A) ∩ B)
↔ ((x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ A) ∧ x ∈ B))) |
27 | 13, 22, 26 | 3bitr4d 209 |
. . 3
⊢ (𝐹 Fn dom 𝐹 → (x ∈ (◡(𝐹 ↾ B) “ A)
↔ x ∈ ((◡𝐹 “ A) ∩ B))) |
28 | 1, 27 | sylbi 114 |
. 2
⊢ (Fun
𝐹 → (x ∈ (◡(𝐹 ↾ B) “ A)
↔ x ∈ ((◡𝐹 “ A) ∩ B))) |
29 | 28 | eqrdv 2035 |
1
⊢ (Fun
𝐹 → (◡(𝐹 ↾ B) “ A) =
((◡𝐹 “ A) ∩ B)) |