Step | Hyp | Ref
| Expression |
1 | | funimage 32943 |
. . 3
⊢ Fun
Image𝑅 |
2 | | funrel 6234 |
. . 3
⊢ (Fun
Image𝑅 → Rel
Image𝑅) |
3 | 1, 2 | ax-mp 5 |
. 2
⊢ Rel
Image𝑅 |
4 | | mptrel 5575 |
. 2
⊢ Rel
(𝑥 ∈ V ↦ (𝑅 “ 𝑥)) |
5 | | vex 3435 |
. . . . 5
⊢ 𝑦 ∈ V |
6 | | vex 3435 |
. . . . 5
⊢ 𝑧 ∈ V |
7 | 5, 6 | breldm 5655 |
. . . 4
⊢ (𝑦Image𝑅𝑧 → 𝑦 ∈ dom Image𝑅) |
8 | | fnimage 32944 |
. . . . 5
⊢
Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
9 | | fndm 6317 |
. . . . 5
⊢
(Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} → dom Image𝑅 = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) |
10 | 8, 9 | ax-mp 5 |
. . . 4
⊢ dom
Image𝑅 = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
11 | 7, 10 | syl6eleq 2891 |
. . 3
⊢ (𝑦Image𝑅𝑧 → 𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) |
12 | 5, 6 | breldm 5655 |
. . . 4
⊢ (𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧 → 𝑦 ∈ dom (𝑥 ∈ V ↦ (𝑅 “ 𝑥))) |
13 | | eqid 2793 |
. . . . . 6
⊢ (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) = (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) |
14 | 13 | dmmpt 5961 |
. . . . 5
⊢ dom
(𝑥 ∈ V ↦ (𝑅 “ 𝑥)) = {𝑥 ∈ V ∣ (𝑅 “ 𝑥) ∈ V} |
15 | | rabab 3461 |
. . . . 5
⊢ {𝑥 ∈ V ∣ (𝑅 “ 𝑥) ∈ V} = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
16 | 14, 15 | eqtri 2817 |
. . . 4
⊢ dom
(𝑥 ∈ V ↦ (𝑅 “ 𝑥)) = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
17 | 12, 16 | syl6eleq 2891 |
. . 3
⊢ (𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧 → 𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) |
18 | | imaeq2 5794 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑅 “ 𝑥) = (𝑅 “ 𝑦)) |
19 | 18 | eleq1d 2865 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑅 “ 𝑥) ∈ V ↔ (𝑅 “ 𝑦) ∈ V)) |
20 | 5, 19 | elab 3600 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} ↔ (𝑅 “ 𝑦) ∈ V) |
21 | 5, 6 | brimage 32941 |
. . . . 5
⊢ (𝑦Image𝑅𝑧 ↔ 𝑧 = (𝑅 “ 𝑦)) |
22 | | eqcom 2800 |
. . . . . 6
⊢ (𝑧 = (𝑅 “ 𝑦) ↔ (𝑅 “ 𝑦) = 𝑧) |
23 | 18, 13 | fvmptg 6624 |
. . . . . . . . 9
⊢ ((𝑦 ∈ V ∧ (𝑅 “ 𝑦) ∈ V) → ((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = (𝑅 “ 𝑦)) |
24 | 5, 23 | mpan 686 |
. . . . . . . 8
⊢ ((𝑅 “ 𝑦) ∈ V → ((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = (𝑅 “ 𝑦)) |
25 | 24 | eqeq1d 2795 |
. . . . . . 7
⊢ ((𝑅 “ 𝑦) ∈ V → (((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = 𝑧 ↔ (𝑅 “ 𝑦) = 𝑧)) |
26 | | funmpt 6255 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ V ↦ (𝑅 “ 𝑥)) |
27 | | df-fn 6220 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ↦ (𝑅 “ 𝑥)) Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} ↔ (Fun (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) ∧ dom (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V})) |
28 | 26, 16, 27 | mpbir2an 707 |
. . . . . . . 8
⊢ (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
29 | 20 | biimpri 229 |
. . . . . . . 8
⊢ ((𝑅 “ 𝑦) ∈ V → 𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) |
30 | | fnbrfvb 6578 |
. . . . . . . 8
⊢ (((𝑥 ∈ V ↦ (𝑅 “ 𝑥)) Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} ∧ 𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) → (((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = 𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
31 | 28, 29, 30 | sylancr 587 |
. . . . . . 7
⊢ ((𝑅 “ 𝑦) ∈ V → (((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = 𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
32 | 25, 31 | bitr3d 282 |
. . . . . 6
⊢ ((𝑅 “ 𝑦) ∈ V → ((𝑅 “ 𝑦) = 𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
33 | 22, 32 | syl5bb 284 |
. . . . 5
⊢ ((𝑅 “ 𝑦) ∈ V → (𝑧 = (𝑅 “ 𝑦) ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
34 | 21, 33 | syl5bb 284 |
. . . 4
⊢ ((𝑅 “ 𝑦) ∈ V → (𝑦Image𝑅𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
35 | 20, 34 | sylbi 218 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} → (𝑦Image𝑅𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
36 | 11, 17, 35 | pm5.21nii 380 |
. 2
⊢ (𝑦Image𝑅𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧) |
37 | 3, 4, 36 | eqbrriv 5542 |
1
⊢
Image𝑅 = (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) |