Step | Hyp | Ref
| Expression |
1 | | relres 5346 |
. 2
⊢ Rel
(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) |
2 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘𝑥) ∈ V |
3 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑧 = (𝐹‘𝑥) → (𝑦 = 𝑧 ↔ 𝑦 = (𝐹‘𝑥))) |
4 | 3 | imbi2d 329 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝑥) → ((𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = 𝑧) ↔ (𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = (𝐹‘𝑥)))) |
5 | 4 | albidv 1836 |
. . . . 5
⊢ (𝑧 = (𝐹‘𝑥) → (∀𝑦(𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = 𝑧) ↔ ∀𝑦(𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = (𝐹‘𝑥)))) |
6 | 2, 5 | spcev 3273 |
. . . 4
⊢
(∀𝑦(𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = (𝐹‘𝑥)) → ∃𝑧∀𝑦(𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = 𝑧)) |
7 | | vex 3176 |
. . . . . 6
⊢ 𝑦 ∈ V |
8 | 7 | brres 5323 |
. . . . 5
⊢ (𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 ↔ (𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})) |
9 | | abid 2598 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} ↔ ∃!𝑦 𝑥𝐹𝑦) |
10 | | tz6.12-1 6120 |
. . . . . . 7
⊢ ((𝑥𝐹𝑦 ∧ ∃!𝑦 𝑥𝐹𝑦) → (𝐹‘𝑥) = 𝑦) |
11 | 9, 10 | sylan2b 491 |
. . . . . 6
⊢ ((𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) → (𝐹‘𝑥) = 𝑦) |
12 | 11 | eqcomd 2616 |
. . . . 5
⊢ ((𝑥𝐹𝑦 ∧ 𝑥 ∈ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) → 𝑦 = (𝐹‘𝑥)) |
13 | 8, 12 | sylbi 206 |
. . . 4
⊢ (𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = (𝐹‘𝑥)) |
14 | 6, 13 | mpg 1715 |
. . 3
⊢
∃𝑧∀𝑦(𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = 𝑧) |
15 | 14 | ax-gen 1713 |
. 2
⊢
∀𝑥∃𝑧∀𝑦(𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = 𝑧) |
16 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑥𝐹 |
17 | | nfab1 2753 |
. . . 4
⊢
Ⅎ𝑥{𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} |
18 | 16, 17 | nfres 5319 |
. . 3
⊢
Ⅎ𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) |
19 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑦𝐹 |
20 | | nfeu1 2468 |
. . . . 5
⊢
Ⅎ𝑦∃!𝑦 𝑥𝐹𝑦 |
21 | 20 | nfab 2755 |
. . . 4
⊢
Ⅎ𝑦{𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} |
22 | 19, 21 | nfres 5319 |
. . 3
⊢
Ⅎ𝑦(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) |
23 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑧(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) |
24 | 18, 22, 23 | dffun3f 42227 |
. 2
⊢ (Fun
(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) ↔ (Rel (𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) ∧ ∀𝑥∃𝑧∀𝑦(𝑥(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦})𝑦 → 𝑦 = 𝑧))) |
25 | 1, 15, 24 | mpbir2an 957 |
1
⊢ Fun
(𝐹 ↾ {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}) |