Step | Hyp | Ref
| Expression |
1 | | relres 5967 |
. 2
⊢ Rel
(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
2 | | vex 3448 |
. . . . . . 7
⊢ 𝑧 ∈ V |
3 | 2 | brresi 5947 |
. . . . . 6
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧 ↔ (𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ∧ 𝑥𝐹𝑧)) |
4 | 3 | simprbi 498 |
. . . . 5
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧 → 𝑥𝐹𝑧) |
5 | | vex 3448 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
6 | 5 | brresi 5947 |
. . . . . . 7
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ↔ (𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ∧ 𝑥𝐹𝑦)) |
7 | | funpartlem 34573 |
. . . . . . . 8
⊢ (𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑤(𝐹 “ {𝑥}) = {𝑤}) |
8 | 7 | anbi1i 625 |
. . . . . . 7
⊢ ((𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ∧ 𝑥𝐹𝑦) ↔ (∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦)) |
9 | 6, 8 | bitri 275 |
. . . . . 6
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ↔ (∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦)) |
10 | | df-br 5107 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹) |
11 | | df-br 5107 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹) |
12 | 10, 11 | anbi12i 628 |
. . . . . . . . . 10
⊢ ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) |
13 | | vex 3448 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
14 | 13, 5 | elimasn 6042 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐹 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹) |
15 | 13, 2 | elimasn 6042 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐹 “ {𝑥}) ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐹) |
16 | 14, 15 | anbi12i 628 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) |
17 | 12, 16 | bitr4i 278 |
. . . . . . . . 9
⊢ ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) ↔ (𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥}))) |
18 | | eleq2 2823 |
. . . . . . . . . . 11
⊢ ((𝐹 “ {𝑥}) = {𝑤} → (𝑦 ∈ (𝐹 “ {𝑥}) ↔ 𝑦 ∈ {𝑤})) |
19 | | eleq2 2823 |
. . . . . . . . . . 11
⊢ ((𝐹 “ {𝑥}) = {𝑤} → (𝑧 ∈ (𝐹 “ {𝑥}) ↔ 𝑧 ∈ {𝑤})) |
20 | 18, 19 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) ↔ (𝑦 ∈ {𝑤} ∧ 𝑧 ∈ {𝑤}))) |
21 | | velsn 4603 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤) |
22 | | velsn 4603 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑤} ↔ 𝑧 = 𝑤) |
23 | | equtr2 2031 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑤) → 𝑦 = 𝑧) |
24 | 21, 22, 23 | syl2anb 599 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ {𝑤} ∧ 𝑧 ∈ {𝑤}) → 𝑦 = 𝑧) |
25 | 20, 24 | syl6bi 253 |
. . . . . . . . 9
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) → 𝑦 = 𝑧)) |
26 | 17, 25 | biimtrid 241 |
. . . . . . . 8
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧)) |
27 | 26 | exlimiv 1934 |
. . . . . . 7
⊢
(∃𝑤(𝐹 “ {𝑥}) = {𝑤} → ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧)) |
28 | 27 | impl 457 |
. . . . . 6
⊢
(((∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦) ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧) |
29 | 9, 28 | sylanb 582 |
. . . . 5
⊢ ((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧) |
30 | 4, 29 | sylan2 594 |
. . . 4
⊢ ((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧) |
31 | 30 | gen2 1799 |
. . 3
⊢
∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧) |
32 | 31 | ax-gen 1798 |
. 2
⊢
∀𝑥∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧) |
33 | | df-funpart 34505 |
. . . 4
⊢
Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
34 | 33 | funeqi 6523 |
. . 3
⊢ (Fun
Funpart𝐹 ↔ Fun (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )))) |
35 | | dffun2 6507 |
. . 3
⊢ (Fun
(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) ↔ (Rel (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) ∧ ∀𝑥∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧))) |
36 | 34, 35 | bitri 275 |
. 2
⊢ (Fun
Funpart𝐹 ↔ (Rel (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) ∧ ∀𝑥∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧))) |
37 | 1, 32, 36 | mpbir2an 710 |
1
⊢ Fun
Funpart𝐹 |