Step | Hyp | Ref
| Expression |
1 | | dmmpt2.1 |
. . . . . 6
⊢ 𝐹 = (x ∈ A ↦ B) |
2 | | df-mpt 3811 |
. . . . . 6
⊢ (x ∈ A ↦ B) =
{〈x, y〉 ∣ (x ∈ A ∧ y = B)} |
3 | 1, 2 | eqtri 2057 |
. . . . 5
⊢ 𝐹 = {〈x, y〉
∣ (x ∈ A ∧ y = B)} |
4 | 3 | cnveqi 4453 |
. . . 4
⊢ ◡𝐹 = ◡{〈x, y〉
∣ (x ∈ A ∧ y = B)} |
5 | | cnvopab 4669 |
. . . 4
⊢ ◡{〈x, y〉
∣ (x ∈ A ∧ y = B)} = {〈y,
x〉 ∣ (x ∈ A ∧ y = B)} |
6 | 4, 5 | eqtri 2057 |
. . 3
⊢ ◡𝐹 = {〈y, x〉
∣ (x ∈ A ∧ y = B)} |
7 | 6 | imaeq1i 4608 |
. 2
⊢ (◡𝐹 “ 𝐶) = ({〈y, x〉
∣ (x ∈ A ∧ y = B)} “ 𝐶) |
8 | | df-ima 4301 |
. . 3
⊢
({〈y, x〉 ∣ (x ∈ A ∧ y = B)} “
𝐶) = ran ({〈y, x〉
∣ (x ∈ A ∧ y = B)} ↾ 𝐶) |
9 | | resopab 4595 |
. . . . 5
⊢
({〈y, x〉 ∣ (x ∈ A ∧ y = B)} ↾
𝐶) = {〈y, x〉
∣ (y ∈ 𝐶 ∧
(x ∈
A ∧
y = B))} |
10 | 9 | rneqi 4505 |
. . . 4
⊢ ran
({〈y, x〉 ∣ (x ∈ A ∧ y = B)} ↾
𝐶) = ran {〈y, x〉
∣ (y ∈ 𝐶 ∧
(x ∈
A ∧
y = B))} |
11 | | ancom 253 |
. . . . . . . . 9
⊢
((y ∈ 𝐶 ∧
(x ∈
A ∧
y = B))
↔ ((x ∈ A ∧ y = B) ∧ y ∈ 𝐶)) |
12 | | anass 381 |
. . . . . . . . 9
⊢
(((x ∈ A ∧ y = B) ∧ y ∈ 𝐶) ↔ (x ∈ A ∧ (y = B ∧ y ∈ 𝐶))) |
13 | 11, 12 | bitri 173 |
. . . . . . . 8
⊢
((y ∈ 𝐶 ∧
(x ∈
A ∧
y = B))
↔ (x ∈ A ∧ (y = B ∧ y ∈ 𝐶))) |
14 | 13 | exbii 1493 |
. . . . . . 7
⊢ (∃y(y ∈ 𝐶 ∧ (x ∈ A ∧ y = B)) ↔ ∃y(x ∈ A ∧ (y = B ∧ y ∈ 𝐶))) |
15 | | 19.42v 1783 |
. . . . . . . 8
⊢ (∃y(x ∈ A ∧ (y = B ∧ y ∈ 𝐶)) ↔ (x ∈ A ∧ ∃y(y = B ∧ y ∈ 𝐶))) |
16 | | df-clel 2033 |
. . . . . . . . . 10
⊢ (B ∈ 𝐶 ↔ ∃y(y = B ∧ y ∈ 𝐶)) |
17 | 16 | bicomi 123 |
. . . . . . . . 9
⊢ (∃y(y = B ∧ y ∈ 𝐶) ↔ B ∈ 𝐶) |
18 | 17 | anbi2i 430 |
. . . . . . . 8
⊢
((x ∈ A ∧ ∃y(y = B ∧ y ∈ 𝐶)) ↔ (x ∈ A ∧ B ∈ 𝐶)) |
19 | 15, 18 | bitri 173 |
. . . . . . 7
⊢ (∃y(x ∈ A ∧ (y = B ∧ y ∈ 𝐶)) ↔ (x ∈ A ∧ B ∈ 𝐶)) |
20 | 14, 19 | bitri 173 |
. . . . . 6
⊢ (∃y(y ∈ 𝐶 ∧ (x ∈ A ∧ y = B)) ↔ (x
∈ A ∧ B ∈ 𝐶)) |
21 | 20 | abbii 2150 |
. . . . 5
⊢ {x ∣ ∃y(y ∈ 𝐶 ∧ (x ∈ A ∧ y = B))} = {x
∣ (x ∈ A ∧ B ∈ 𝐶)} |
22 | | rnopab 4524 |
. . . . 5
⊢ ran
{〈y, x〉 ∣ (y ∈ 𝐶 ∧ (x ∈ A ∧ y = B))} = {x
∣ ∃y(y ∈ 𝐶 ∧
(x ∈
A ∧
y = B))} |
23 | | df-rab 2309 |
. . . . 5
⊢ {x ∈ A ∣ B
∈ 𝐶} = {x
∣ (x ∈ A ∧ B ∈ 𝐶)} |
24 | 21, 22, 23 | 3eqtr4i 2067 |
. . . 4
⊢ ran
{〈y, x〉 ∣ (y ∈ 𝐶 ∧ (x ∈ A ∧ y = B))} = {x ∈ A ∣
B ∈ 𝐶} |
25 | 10, 24 | eqtri 2057 |
. . 3
⊢ ran
({〈y, x〉 ∣ (x ∈ A ∧ y = B)} ↾
𝐶) = {x ∈ A ∣ B
∈ 𝐶} |
26 | 8, 25 | eqtri 2057 |
. 2
⊢
({〈y, x〉 ∣ (x ∈ A ∧ y = B)} “
𝐶) = {x ∈ A ∣ B
∈ 𝐶} |
27 | 7, 26 | eqtri 2057 |
1
⊢ (◡𝐹 “ 𝐶) = {x
∈ A
∣ B ∈ 𝐶} |