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