Step | Hyp | Ref
| Expression |
1 | | df-funpart 31150 |
. . 3
⊢
Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
2 | 1 | fveq1i 6104 |
. 2
⊢
(Funpart𝐹‘𝐴) = ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) |
3 | | fvres 6117 |
. . 3
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = (𝐹‘𝐴)) |
4 | | nfvres 6134 |
. . . 4
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = ∅) |
5 | | funpartlem 31219 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |
6 | | eusn 4209 |
. . . . . . . . 9
⊢
(∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴}) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |
7 | 5, 6 | bitr4i 266 |
. . . . . . . 8
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴})) |
8 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
9 | | elimasng 5410 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑥 ∈ V) → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 〈𝐴, 𝑥〉 ∈ 𝐹)) |
10 | 8, 9 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 〈𝐴, 𝑥〉 ∈ 𝐹)) |
11 | | df-br 4584 |
. . . . . . . . . 10
⊢ (𝐴𝐹𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐹) |
12 | 10, 11 | syl6bbr 277 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 𝐴𝐹𝑥)) |
13 | 12 | eubidv 2478 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴}) ↔ ∃!𝑥 𝐴𝐹𝑥)) |
14 | 7, 13 | syl5bb 271 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃!𝑥 𝐴𝐹𝑥)) |
15 | 14 | notbid 307 |
. . . . . 6
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ¬ ∃!𝑥 𝐴𝐹𝑥)) |
16 | | tz6.12-2 6094 |
. . . . . 6
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) |
17 | 15, 16 | syl6bi 242 |
. . . . 5
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅)) |
18 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
19 | 18 | a1d 25 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅)) |
20 | 17, 19 | pm2.61i 175 |
. . . 4
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅) |
21 | 4, 20 | eqtr4d 2647 |
. . 3
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = (𝐹‘𝐴)) |
22 | 3, 21 | pm2.61i 175 |
. 2
⊢ ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )))‘𝐴) = (𝐹‘𝐴) |
23 | 2, 22 | eqtri 2632 |
1
⊢
(Funpart𝐹‘𝐴) = (𝐹‘𝐴) |