Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → 𝐴 ∈ V) |
2 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
3 | 2 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → 𝑦 ∈ V) |
4 | | df-br 5054 |
. . . . . . . . . 10
⊢ (𝐴𝐹𝑦 ↔ 〈𝐴, 𝑦〉 ∈ 𝐹) |
5 | 4 | biimpri 231 |
. . . . . . . . 9
⊢
(〈𝐴, 𝑦〉 ∈ 𝐹 → 𝐴𝐹𝑦) |
6 | 5 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → 𝐴𝐹𝑦) |
7 | | breldmg 5778 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝑦 ∈ V ∧ 𝐴𝐹𝑦) → 𝐴 ∈ dom 𝐹) |
8 | 1, 3, 6, 7 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → 𝐴 ∈ dom 𝐹) |
9 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → 𝐴 ∈ dom 𝐹) |
10 | | velsn 4557 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
11 | | breq1 5056 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = 𝑥 → (𝐴𝐹𝑦 ↔ 𝑥𝐹𝑦)) |
12 | 4, 11 | bitr3id 288 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = 𝑥 → (〈𝐴, 𝑦〉 ∈ 𝐹 ↔ 𝑥𝐹𝑦)) |
13 | 12 | eqcoms 2745 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐴 → (〈𝐴, 𝑦〉 ∈ 𝐹 ↔ 𝑥𝐹𝑦)) |
14 | 13 | eubidv 2585 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 ↔ ∃!𝑦 𝑥𝐹𝑦)) |
15 | 14 | biimpd 232 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦)) |
16 | 10, 15 | sylbi 220 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {𝐴} → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦)) |
17 | 16 | com12 32 |
. . . . . . . . . . . 12
⊢
(∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦)) |
18 | 17 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦)) |
19 | 18 | ralrimiv 3104 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦) |
20 | | fnres 6504 |
. . . . . . . . . . 11
⊢ ((𝐹 ↾ {𝐴}) Fn {𝐴} ↔ ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦) |
21 | | fnfun 6479 |
. . . . . . . . . . 11
⊢ ((𝐹 ↾ {𝐴}) Fn {𝐴} → Fun (𝐹 ↾ {𝐴})) |
22 | 20, 21 | sylbir 238 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
{𝐴}∃!𝑦 𝑥𝐹𝑦 → Fun (𝐹 ↾ {𝐴})) |
23 | 19, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → Fun (𝐹 ↾ {𝐴})) |
24 | 9, 23 | jca 515 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) |
25 | 24 | ex 416 |
. . . . . . 7
⊢ (𝐴 ∈ dom 𝐹 → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))) |
26 | 8, 25 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))) |
27 | 26 | impr 458 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) |
28 | | df-dfat 44283 |
. . . . . 6
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) |
29 | | afvfundmfveq 44302 |
. . . . . 6
⊢ (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹‘𝐴)) |
30 | 28, 29 | sylbir 238 |
. . . . 5
⊢ ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐹'''𝐴) = (𝐹‘𝐴)) |
31 | 27, 30 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (𝐹'''𝐴) = (𝐹‘𝐴)) |
32 | | tz6.12 6740 |
. . . . 5
⊢
((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹‘𝐴) = 𝑦) |
33 | 32 | adantl 485 |
. . . 4
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (𝐹‘𝐴) = 𝑦) |
34 | 31, 33 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (𝐹'''𝐴) = 𝑦) |
35 | 34 | ex 416 |
. 2
⊢ (𝐴 ∈ V → ((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹'''𝐴) = 𝑦)) |
36 | | eu2ndop1stv 44289 |
. . . . 5
⊢
(∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → 𝐴 ∈ V) |
37 | 36 | pm2.24d 154 |
. . . 4
⊢
(∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → (¬ 𝐴 ∈ V → (𝐹'''𝐴) = 𝑦)) |
38 | 37 | adantl 485 |
. . 3
⊢
((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (¬ 𝐴 ∈ V → (𝐹'''𝐴) = 𝑦)) |
39 | 38 | com12 32 |
. 2
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹'''𝐴) = 𝑦)) |
40 | 35, 39 | pm2.61i 185 |
1
⊢
((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹'''𝐴) = 𝑦) |