Step | Hyp | Ref
| Expression |
1 | | dmmpt2.1 |
. . . . . 6
⊢ F = (x ∈ A ↦ B) |
2 | | df-mpt 5652 |
. . . . . 6
⊢ (x ∈ A ↦ B) = {〈x, y〉 ∣ (x ∈ A ∧ y = B)} |
3 | 1, 2 | eqtri 2373 |
. . . . 5
⊢ F = {〈x, y〉 ∣ (x ∈ A ∧ y = B)} |
4 | 3 | cnveqi 4887 |
. . . 4
⊢ ◡F =
◡{〈x, y〉 ∣ (x ∈ A ∧ y = B)} |
5 | | cnvopab 5030 |
. . . 4
⊢ ◡{〈x, y〉 ∣ (x ∈ A ∧ y = B)} = {〈y, x〉 ∣ (x ∈ A ∧ y = B)} |
6 | 4, 5 | eqtri 2373 |
. . 3
⊢ ◡F =
{〈y,
x〉 ∣ (x ∈ A ∧ y = B)} |
7 | 6 | imaeq1i 4939 |
. 2
⊢ (◡F
“ C) = ({〈y, x〉 ∣ (x ∈ A ∧ y = B)} “ C) |
8 | | dfima3 4951 |
. . 3
⊢ ({〈y, x〉 ∣ (x ∈ A ∧ y = B)} “ C) =
ran ({〈y,
x〉 ∣ (x ∈ A ∧ y = B)} ↾ C) |
9 | | resopab 4999 |
. . . . 5
⊢ ({〈y, x〉 ∣ (x ∈ A ∧ y = B)} ↾ C) = {〈y, x〉 ∣ (y ∈ C ∧ (x ∈ A ∧ y = B))} |
10 | 9 | rneqi 4957 |
. . . 4
⊢ ran ({〈y, x〉 ∣ (x ∈ A ∧ y = B)} ↾ C) = ran {〈y, x〉 ∣ (y ∈ C ∧ (x ∈ A ∧ y = B))} |
11 | | ancom 437 |
. . . . . . . . 9
⊢ ((y ∈ C ∧ (x ∈ A ∧ y = B)) ↔
((x ∈
A ∧
y = B)
∧ y ∈ C)) |
12 | | anass 630 |
. . . . . . . . 9
⊢ (((x ∈ A ∧ y = B) ∧ y ∈ C) ↔
(x ∈
A ∧
(y = B
∧ y ∈ C))) |
13 | 11, 12 | bitri 240 |
. . . . . . . 8
⊢ ((y ∈ C ∧ (x ∈ A ∧ y = B)) ↔
(x ∈
A ∧
(y = B
∧ y ∈ C))) |
14 | 13 | exbii 1582 |
. . . . . . 7
⊢ (∃y(y ∈ C ∧ (x ∈ A ∧ y = B)) ↔
∃y(x ∈ A ∧ (y = B ∧ y ∈ C))) |
15 | | 19.42v 1905 |
. . . . . . . 8
⊢ (∃y(x ∈ A ∧ (y = B ∧ y ∈ C)) ↔
(x ∈
A ∧ ∃y(y = B ∧ y ∈ C))) |
16 | | df-clel 2349 |
. . . . . . . . . 10
⊢ (B ∈ C ↔ ∃y(y = B ∧ y ∈ C)) |
17 | 16 | bicomi 193 |
. . . . . . . . 9
⊢ (∃y(y = B ∧ y ∈ C) ↔
B ∈
C) |
18 | 17 | anbi2i 675 |
. . . . . . . 8
⊢ ((x ∈ A ∧ ∃y(y = B ∧ y ∈ C)) ↔
(x ∈
A ∧
B ∈
C)) |
19 | 15, 18 | bitri 240 |
. . . . . . 7
⊢ (∃y(x ∈ A ∧ (y = B ∧ y ∈ C)) ↔
(x ∈
A ∧
B ∈
C)) |
20 | 14, 19 | bitri 240 |
. . . . . 6
⊢ (∃y(y ∈ C ∧ (x ∈ A ∧ y = B)) ↔
(x ∈
A ∧
B ∈
C)) |
21 | 20 | abbii 2465 |
. . . . 5
⊢ {x ∣ ∃y(y ∈ C ∧ (x ∈ A ∧ y = B))} =
{x ∣
(x ∈
A ∧
B ∈
C)} |
22 | | rnopab 4967 |
. . . . 5
⊢ ran {〈y, x〉 ∣ (y ∈ C ∧ (x ∈ A ∧ y = B))} = {x ∣ ∃y(y ∈ C ∧ (x ∈ A ∧ y = B))} |
23 | | df-rab 2623 |
. . . . 5
⊢ {x ∈ A ∣ B ∈ C} = {x ∣ (x ∈ A ∧ B ∈ C)} |
24 | 21, 22, 23 | 3eqtr4i 2383 |
. . . 4
⊢ ran {〈y, x〉 ∣ (y ∈ C ∧ (x ∈ A ∧ y = B))} = {x ∈ A ∣ B ∈ C} |
25 | 10, 24 | eqtri 2373 |
. . 3
⊢ ran ({〈y, x〉 ∣ (x ∈ A ∧ y = B)} ↾ C) = {x ∈ A ∣ B ∈ C} |
26 | 8, 25 | eqtri 2373 |
. 2
⊢ ({〈y, x〉 ∣ (x ∈ A ∧ y = B)} “ C) =
{x ∈
A ∣
B ∈
C} |
27 | 7, 26 | eqtri 2373 |
1
⊢ (◡F
“ C) = {x ∈ A ∣ B ∈ C} |