Step | Hyp | Ref
| Expression |
1 | | df-funpart 34488 |
. . 3
⊢
Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
2 | 1 | fveq1i 6848 |
. 2
⊢
(Funpart𝐹‘𝐴) = ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) |
3 | | fvres 6866 |
. . 3
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = (𝐹‘𝐴)) |
4 | | nfvres 6888 |
. . . 4
⊢ (¬
𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → ((𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))‘𝐴) = ∅) |
5 | | funpartlem 34556 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |
6 | | eusn 4696 |
. . . . . . . . 9
⊢
(∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴}) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) |
7 | 5, 6 | bitr4i 278 |
. . . . . . . 8
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃!𝑥 𝑥 ∈ (𝐹 “ {𝐴})) |
8 | | elimasng 6045 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑥 ∈ V) → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ ⟨𝐴, 𝑥⟩ ∈ 𝐹)) |
9 | 8 | elvd 3455 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ ⟨𝐴, 𝑥⟩ ∈ 𝐹)) |
10 | | df-br 5111 |
. . . . . . . . . 10
⊢ (𝐴𝐹𝑥 ↔ ⟨𝐴, 𝑥⟩ ∈ 𝐹) |
11 | 9, 10 | bitr4di 289 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 𝐴𝐹𝑥)) |
12 | 11 | eubidv 2585 |
. . . . . . . 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 6835 |
. . . . . 6
⊢ (¬
∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) |
16 | 14, 15 | syl6bi 253 |
. . . . 5
⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) → (𝐹‘𝐴) = ∅)) |
17 | | fvprc 6839 |
. . . . . 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𝐹‘𝐴) = (𝐹‘𝐴) |