Step | Hyp | Ref
| Expression |
1 | | df-funpart 33328 |
. . 3
⊢
Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
2 | 1 | fveq1i 6664 |
. 2
⊢
(Funpart𝐹‘𝐴) = ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) |
3 | | fvres 6682 |
. . 3
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = (𝐹‘𝐴)) |
4 | | nfvres 6699 |
. . . 4
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = ∅) |
5 | | funpartlem 33396 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |
6 | | eusn 4658 |
. . . . . . . . 9
⊢
(∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴}) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |
7 | 5, 6 | bitr4i 280 |
. . . . . . . 8
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴})) |
8 | | elimasng 5948 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑥 ∈ V) → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 〈𝐴, 𝑥〉 ∈ 𝐹)) |
9 | 8 | elvd 3499 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 〈𝐴, 𝑥〉 ∈ 𝐹)) |
10 | | df-br 5058 |
. . . . . . . . . 10
⊢ (𝐴𝐹𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐹) |
11 | 9, 10 | syl6bbr 291 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 𝐴𝐹𝑥)) |
12 | 11 | eubidv 2666 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴}) ↔ ∃!𝑥 𝐴𝐹𝑥)) |
13 | 7, 12 | syl5bb 285 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃!𝑥 𝐴𝐹𝑥)) |
14 | 13 | notbid 320 |
. . . . . 6
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ¬ ∃!𝑥 𝐴𝐹𝑥)) |
15 | | tz6.12-2 6653 |
. . . . . 6
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) |
16 | 14, 15 | syl6bi 255 |
. . . . 5
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅)) |
17 | | fvprc 6656 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
18 | 17 | a1d 25 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅)) |
19 | 16, 18 | pm2.61i 184 |
. . . 4
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅) |
20 | 4, 19 | eqtr4d 2857 |
. . 3
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = (𝐹‘𝐴)) |
21 | 3, 20 | pm2.61i 184 |
. 2
⊢ ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )))‘𝐴) = (𝐹‘𝐴) |
22 | 2, 21 | eqtri 2842 |
1
⊢
(Funpart𝐹‘𝐴) = (𝐹‘𝐴) |