Step | Hyp | Ref
| Expression |
1 | | relres 5426 |
. 2
⊢ Rel
(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
2 | | vex 3203 |
. . . . . . 7
⊢ 𝑧 ∈ V |
3 | 2 | brres 5402 |
. . . . . 6
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧 ↔ (𝑥𝐹𝑧 ∧ 𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))) |
4 | 3 | simplbi 476 |
. . . . 5
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧 → 𝑥𝐹𝑧) |
5 | | vex 3203 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
6 | 5 | brres 5402 |
. . . . . . 7
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ↔ (𝑥𝐹𝑦 ∧ 𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))) |
7 | | ancom 466 |
. . . . . . . 8
⊢ ((𝑥𝐹𝑦 ∧ 𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))) ↔ (𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ∧ 𝑥𝐹𝑦)) |
8 | | funpartlem 32049 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑤(𝐹 “ {𝑥}) = {𝑤}) |
9 | 8 | anbi1i 731 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ∧ 𝑥𝐹𝑦) ↔ (∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦)) |
10 | 7, 9 | bitri 264 |
. . . . . . 7
⊢ ((𝑥𝐹𝑦 ∧ 𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))) ↔ (∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦)) |
11 | 6, 10 | bitri 264 |
. . . . . 6
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ↔ (∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦)) |
12 | | df-br 4654 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝐹) |
13 | | df-br 4654 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑧 ↔ 〈𝑥, 𝑧〉 ∈ 𝐹) |
14 | 12, 13 | anbi12i 733 |
. . . . . . . . . 10
⊢ ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) ↔ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹)) |
15 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
16 | 15, 5 | elimasn 5490 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐹 “ {𝑥}) ↔ 〈𝑥, 𝑦〉 ∈ 𝐹) |
17 | 15, 2 | elimasn 5490 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐹 “ {𝑥}) ↔ 〈𝑥, 𝑧〉 ∈ 𝐹) |
18 | 16, 17 | anbi12i 733 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) ↔ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹)) |
19 | 14, 18 | bitr4i 267 |
. . . . . . . . 9
⊢ ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) ↔ (𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥}))) |
20 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ ((𝐹 “ {𝑥}) = {𝑤} → (𝑦 ∈ (𝐹 “ {𝑥}) ↔ 𝑦 ∈ {𝑤})) |
21 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ ((𝐹 “ {𝑥}) = {𝑤} → (𝑧 ∈ (𝐹 “ {𝑥}) ↔ 𝑧 ∈ {𝑤})) |
22 | 20, 21 | anbi12d 747 |
. . . . . . . . . 10
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) ↔ (𝑦 ∈ {𝑤} ∧ 𝑧 ∈ {𝑤}))) |
23 | | velsn 4193 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤) |
24 | | velsn 4193 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑤} ↔ 𝑧 = 𝑤) |
25 | | equtr2 1954 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑤) → 𝑦 = 𝑧) |
26 | 23, 24, 25 | syl2anb 496 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ {𝑤} ∧ 𝑧 ∈ {𝑤}) → 𝑦 = 𝑧) |
27 | 22, 26 | syl6bi 243 |
. . . . . . . . 9
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) → 𝑦 = 𝑧)) |
28 | 19, 27 | syl5bi 232 |
. . . . . . . 8
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧)) |
29 | 28 | exlimiv 1858 |
. . . . . . 7
⊢
(∃𝑤(𝐹 “ {𝑥}) = {𝑤} → ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧)) |
30 | 29 | impl 650 |
. . . . . 6
⊢
(((∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦) ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧) |
31 | 11, 30 | sylanb 489 |
. . . . 5
⊢ ((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧) |
32 | 4, 31 | sylan2 491 |
. . . 4
⊢ ((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧) |
33 | 32 | gen2 1723 |
. . 3
⊢
∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧) |
34 | 33 | ax-gen 1722 |
. 2
⊢
∀𝑥∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧) |
35 | | df-funpart 31981 |
. . . 4
⊢
Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
36 | 35 | funeqi 5909 |
. . 3
⊢ (Fun
Funpart𝐹 ↔ Fun (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )))) |
37 | | dffun2 5898 |
. . 3
⊢ (Fun
(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) ↔ (Rel (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) ∧ ∀𝑥∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧))) |
38 | 36, 37 | bitri 264 |
. 2
⊢ (Fun
Funpart𝐹 ↔ (Rel (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) ∧ ∀𝑥∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧))) |
39 | 1, 34, 38 | mpbir2an 955 |
1
⊢ Fun
Funpart𝐹 |