| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → 𝐴 ∈ V) | 
| 2 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 3 | 2 | a1i 11 | . . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → 𝑦 ∈ V) | 
| 4 |  | df-br 5143 | . . . . . . . . . . 11
⊢ (𝐴𝐹𝑦 ↔ 〈𝐴, 𝑦〉 ∈ 𝐹) | 
| 5 | 4 | biimpri 228 | . . . . . . . . . 10
⊢
(〈𝐴, 𝑦〉 ∈ 𝐹 → 𝐴𝐹𝑦) | 
| 6 | 5 | adantl 481 | . . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → 𝐴𝐹𝑦) | 
| 7 |  | breldmg 5919 | . . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝑦 ∈ V ∧ 𝐴𝐹𝑦) → 𝐴 ∈ dom 𝐹) | 
| 8 | 1, 3, 6, 7 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → 𝐴 ∈ dom 𝐹) | 
| 9 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → 𝐴 ∈ dom 𝐹) | 
| 10 |  | velsn 4641 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | 
| 11 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 = 𝑥 → (𝐴𝐹𝑦 ↔ 𝑥𝐹𝑦)) | 
| 12 | 4, 11 | bitr3id 285 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = 𝑥 → (〈𝐴, 𝑦〉 ∈ 𝐹 ↔ 𝑥𝐹𝑦)) | 
| 13 | 12 | eqcoms 2744 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐴 → (〈𝐴, 𝑦〉 ∈ 𝐹 ↔ 𝑥𝐹𝑦)) | 
| 14 | 13 | eubidv 2585 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐴 → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 ↔ ∃!𝑦 𝑥𝐹𝑦)) | 
| 15 | 14 | biimpd 229 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦)) | 
| 16 | 10, 15 | sylbi 217 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝐴} → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦)) | 
| 17 | 16 | com12 32 | . . . . . . . . . . . . 13
⊢
(∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦)) | 
| 18 | 17 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦)) | 
| 19 | 18 | ralrimiv 3144 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦) | 
| 20 |  | fnres 6694 | . . . . . . . . . . . 12
⊢ ((𝐹 ↾ {𝐴}) Fn {𝐴} ↔ ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦) | 
| 21 |  | fnfun 6667 | . . . . . . . . . . . 12
⊢ ((𝐹 ↾ {𝐴}) Fn {𝐴} → Fun (𝐹 ↾ {𝐴})) | 
| 22 | 20, 21 | sylbir 235 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
{𝐴}∃!𝑦 𝑥𝐹𝑦 → Fun (𝐹 ↾ {𝐴})) | 
| 23 | 19, 22 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → Fun (𝐹 ↾ {𝐴})) | 
| 24 | 9, 23 | jca 511 | . . . . . . . . 9
⊢ ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) | 
| 25 | 24 | ex 412 | . . . . . . . 8
⊢ (𝐴 ∈ dom 𝐹 → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))) | 
| 26 | 8, 25 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ V ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) → (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))) | 
| 27 | 26 | impr 454 | . . . . . 6
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) | 
| 28 |  | df-dfat 47136 | . . . . . 6
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) | 
| 29 | 27, 28 | sylibr 234 | . . . . 5
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → 𝐹 defAt 𝐴) | 
| 30 |  | dfatafv2iota 47227 | . . . . 5
⊢ (𝐹 defAt 𝐴 → (𝐹''''𝐴) = (℩𝑦𝐴𝐹𝑦)) | 
| 31 | 29, 30 | syl 17 | . . . 4
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (𝐹''''𝐴) = (℩𝑦𝐴𝐹𝑦)) | 
| 32 | 4 | bicomi 224 | . . . . . . . . 9
⊢
(〈𝐴, 𝑦〉 ∈ 𝐹 ↔ 𝐴𝐹𝑦) | 
| 33 | 32 | eubii 2584 | . . . . . . . 8
⊢
(∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 ↔ ∃!𝑦 𝐴𝐹𝑦) | 
| 34 | 33 | biimpi 216 | . . . . . . 7
⊢
(∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → ∃!𝑦 𝐴𝐹𝑦) | 
| 35 | 5, 34 | anim12i 613 | . . . . . 6
⊢
((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦)) | 
| 36 | 35 | adantl 481 | . . . . 5
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦)) | 
| 37 |  | iota1 6537 | . . . . . 6
⊢
(∃!𝑦 𝐴𝐹𝑦 → (𝐴𝐹𝑦 ↔ (℩𝑦𝐴𝐹𝑦) = 𝑦)) | 
| 38 | 37 | biimpac 478 | . . . . 5
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (℩𝑦𝐴𝐹𝑦) = 𝑦) | 
| 39 | 36, 38 | syl 17 | . . . 4
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (℩𝑦𝐴𝐹𝑦) = 𝑦) | 
| 40 | 31, 39 | eqtrd 2776 | . . 3
⊢ ((𝐴 ∈ V ∧ (〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹)) → (𝐹''''𝐴) = 𝑦) | 
| 41 | 40 | ex 412 | . 2
⊢ (𝐴 ∈ V → ((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹''''𝐴) = 𝑦)) | 
| 42 |  | eu2ndop1stv 47142 | . . . . 5
⊢
(∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → 𝐴 ∈ V) | 
| 43 | 42 | pm2.24d 151 | . . . 4
⊢
(∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹 → (¬ 𝐴 ∈ V → (𝐹''''𝐴) = 𝑦)) | 
| 44 | 43 | adantl 481 | . . 3
⊢
((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (¬ 𝐴 ∈ V → (𝐹''''𝐴) = 𝑦)) | 
| 45 | 44 | com12 32 | . 2
⊢ (¬
𝐴 ∈ V →
((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹''''𝐴) = 𝑦)) | 
| 46 | 41, 45 | pm2.61i 182 | 1
⊢
((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹''''𝐴) = 𝑦) |