| Step | Hyp | Ref
| Expression |
| 1 | | df-funpart 35875 |
. . 3
⊢
Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
| 2 | 1 | fveq1i 6907 |
. 2
⊢
(Funpart𝐹‘𝐴) = ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) |
| 3 | | fvres 6925 |
. . 3
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = (𝐹‘𝐴)) |
| 4 | | nfvres 6947 |
. . . 4
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = ∅) |
| 5 | | funpartlem 35943 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |
| 6 | | eusn 4730 |
. . . . . . . . 9
⊢
(∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴}) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |
| 7 | 5, 6 | bitr4i 278 |
. . . . . . . 8
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴})) |
| 8 | | elimasng 6107 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑥 ∈ V) → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 〈𝐴, 𝑥〉 ∈ 𝐹)) |
| 9 | 8 | elvd 3486 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 〈𝐴, 𝑥〉 ∈ 𝐹)) |
| 10 | | df-br 5144 |
. . . . . . . . . 10
⊢ (𝐴𝐹𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐹) |
| 11 | 9, 10 | bitr4di 289 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 𝐴𝐹𝑥)) |
| 12 | 11 | eubidv 2586 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴}) ↔ ∃!𝑥 𝐴𝐹𝑥)) |
| 13 | 7, 12 | bitrid 283 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃!𝑥 𝐴𝐹𝑥)) |
| 14 | 13 | notbid 318 |
. . . . . 6
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ¬ ∃!𝑥 𝐴𝐹𝑥)) |
| 15 | | tz6.12-2 6894 |
. . . . . 6
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) |
| 16 | 14, 15 | biimtrdi 253 |
. . . . 5
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅)) |
| 17 | | fvprc 6898 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
| 18 | 17 | a1d 25 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅)) |
| 19 | 16, 18 | pm2.61i 182 |
. . . 4
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅) |
| 20 | 4, 19 | eqtr4d 2780 |
. . 3
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = (𝐹‘𝐴)) |
| 21 | 3, 20 | pm2.61i 182 |
. 2
⊢ ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )))‘𝐴) = (𝐹‘𝐴) |
| 22 | 2, 21 | eqtri 2765 |
1
⊢
(Funpart𝐹‘𝐴) = (𝐹‘𝐴) |