Step | Hyp | Ref
| Expression |
1 | | funimage 31205 |
. . 3
⊢ Fun
Image𝑅 |
2 | | funrel 5821 |
. . 3
⊢ (Fun
Image𝑅 → Rel
Image𝑅) |
3 | 1, 2 | ax-mp 5 |
. 2
⊢ Rel
Image𝑅 |
4 | | mptrel 5170 |
. 2
⊢ Rel
(𝑥 ∈ V ↦ (𝑅 “ 𝑥)) |
5 | | vex 3176 |
. . . . 5
⊢ 𝑦 ∈ V |
6 | | vex 3176 |
. . . . 5
⊢ 𝑧 ∈ V |
7 | 5, 6 | breldm 5251 |
. . . 4
⊢ (𝑦Image𝑅𝑧 → 𝑦 ∈ dom Image𝑅) |
8 | | fnimage 31206 |
. . . . 5
⊢
Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
9 | | fndm 5904 |
. . . . 5
⊢
(Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} → dom Image𝑅 = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) |
10 | 8, 9 | ax-mp 5 |
. . . 4
⊢ dom
Image𝑅 = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
11 | 7, 10 | syl6eleq 2698 |
. . 3
⊢ (𝑦Image𝑅𝑧 → 𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) |
12 | 5, 6 | breldm 5251 |
. . . 4
⊢ (𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧 → 𝑦 ∈ dom (𝑥 ∈ V ↦ (𝑅 “ 𝑥))) |
13 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) = (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) |
14 | 13 | dmmpt 5547 |
. . . . 5
⊢ dom
(𝑥 ∈ V ↦ (𝑅 “ 𝑥)) = {𝑥 ∈ V ∣ (𝑅 “ 𝑥) ∈ V} |
15 | | rabab 3196 |
. . . . 5
⊢ {𝑥 ∈ V ∣ (𝑅 “ 𝑥) ∈ V} = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
16 | 14, 15 | eqtri 2632 |
. . . 4
⊢ dom
(𝑥 ∈ V ↦ (𝑅 “ 𝑥)) = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
17 | 12, 16 | syl6eleq 2698 |
. . 3
⊢ (𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧 → 𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) |
18 | | imaeq2 5381 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑅 “ 𝑥) = (𝑅 “ 𝑦)) |
19 | 18 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑅 “ 𝑥) ∈ V ↔ (𝑅 “ 𝑦) ∈ V)) |
20 | 5, 19 | elab 3319 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} ↔ (𝑅 “ 𝑦) ∈ V) |
21 | 5, 6 | brimage 31203 |
. . . . 5
⊢ (𝑦Image𝑅𝑧 ↔ 𝑧 = (𝑅 “ 𝑦)) |
22 | | eqcom 2617 |
. . . . . 6
⊢ (𝑧 = (𝑅 “ 𝑦) ↔ (𝑅 “ 𝑦) = 𝑧) |
23 | 18, 13 | fvmptg 6189 |
. . . . . . . . 9
⊢ ((𝑦 ∈ V ∧ (𝑅 “ 𝑦) ∈ V) → ((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = (𝑅 “ 𝑦)) |
24 | 5, 23 | mpan 702 |
. . . . . . . 8
⊢ ((𝑅 “ 𝑦) ∈ V → ((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = (𝑅 “ 𝑦)) |
25 | 24 | eqeq1d 2612 |
. . . . . . 7
⊢ ((𝑅 “ 𝑦) ∈ V → (((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = 𝑧 ↔ (𝑅 “ 𝑦) = 𝑧)) |
26 | | funmpt 5840 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ V ↦ (𝑅 “ 𝑥)) |
27 | | df-fn 5807 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ↦ (𝑅 “ 𝑥)) Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} ↔ (Fun (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) ∧ dom (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) = {𝑥 ∣ (𝑅 “ 𝑥) ∈ V})) |
28 | 26, 16, 27 | mpbir2an 957 |
. . . . . . . 8
⊢ (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} |
29 | 20 | biimpri 217 |
. . . . . . . 8
⊢ ((𝑅 “ 𝑦) ∈ V → 𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) |
30 | | fnbrfvb 6146 |
. . . . . . . 8
⊢ (((𝑥 ∈ V ↦ (𝑅 “ 𝑥)) Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} ∧ 𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}) → (((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = 𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
31 | 28, 29, 30 | sylancr 694 |
. . . . . . 7
⊢ ((𝑅 “ 𝑦) ∈ V → (((𝑥 ∈ V ↦ (𝑅 “ 𝑥))‘𝑦) = 𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
32 | 25, 31 | bitr3d 269 |
. . . . . 6
⊢ ((𝑅 “ 𝑦) ∈ V → ((𝑅 “ 𝑦) = 𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
33 | 22, 32 | syl5bb 271 |
. . . . 5
⊢ ((𝑅 “ 𝑦) ∈ V → (𝑧 = (𝑅 “ 𝑦) ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
34 | 21, 33 | syl5bb 271 |
. . . 4
⊢ ((𝑅 “ 𝑦) ∈ V → (𝑦Image𝑅𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
35 | 20, 34 | sylbi 206 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} → (𝑦Image𝑅𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧)) |
36 | 11, 17, 35 | pm5.21nii 367 |
. 2
⊢ (𝑦Image𝑅𝑧 ↔ 𝑦(𝑥 ∈ V ↦ (𝑅 “ 𝑥))𝑧) |
37 | 3, 4, 36 | eqbrriv 5138 |
1
⊢
Image𝑅 = (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) |