Step | Hyp | Ref
| Expression |
1 | | relres 5885 |
. 2
⊢ Rel
(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
2 | | vex 3500 |
. . . . . . 7
⊢ 𝑧 ∈ V |
3 | 2 | brresi 5865 |
. . . . . 6
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧 ↔ (𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ∧ 𝑥𝐹𝑧)) |
4 | 3 | simprbi 499 |
. . . . 5
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧 → 𝑥𝐹𝑧) |
5 | | vex 3500 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
6 | 5 | brresi 5865 |
. . . . . . 7
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ↔ (𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ∧ 𝑥𝐹𝑦)) |
7 | | funpartlem 33407 |
. . . . . . . 8
⊢ (𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ↔ ∃𝑤(𝐹 “ {𝑥}) = {𝑤}) |
8 | 7 | anbi1i 625 |
. . . . . . 7
⊢ ((𝑥 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )) ∧ 𝑥𝐹𝑦) ↔ (∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦)) |
9 | 6, 8 | bitri 277 |
. . . . . 6
⊢ (𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ↔ (∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦)) |
10 | | df-br 5070 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝐹) |
11 | | df-br 5070 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑧 ↔ 〈𝑥, 𝑧〉 ∈ 𝐹) |
12 | 10, 11 | anbi12i 628 |
. . . . . . . . . 10
⊢ ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) ↔ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹)) |
13 | | vex 3500 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
14 | 13, 5 | elimasn 5957 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐹 “ {𝑥}) ↔ 〈𝑥, 𝑦〉 ∈ 𝐹) |
15 | 13, 2 | elimasn 5957 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐹 “ {𝑥}) ↔ 〈𝑥, 𝑧〉 ∈ 𝐹) |
16 | 14, 15 | anbi12i 628 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) ↔ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹)) |
17 | 12, 16 | bitr4i 280 |
. . . . . . . . 9
⊢ ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) ↔ (𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥}))) |
18 | | eleq2 2904 |
. . . . . . . . . . 11
⊢ ((𝐹 “ {𝑥}) = {𝑤} → (𝑦 ∈ (𝐹 “ {𝑥}) ↔ 𝑦 ∈ {𝑤})) |
19 | | eleq2 2904 |
. . . . . . . . . . 11
⊢ ((𝐹 “ {𝑥}) = {𝑤} → (𝑧 ∈ (𝐹 “ {𝑥}) ↔ 𝑧 ∈ {𝑤})) |
20 | 18, 19 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) ↔ (𝑦 ∈ {𝑤} ∧ 𝑧 ∈ {𝑤}))) |
21 | | velsn 4586 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤) |
22 | | velsn 4586 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑤} ↔ 𝑧 = 𝑤) |
23 | | equtr2 2033 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑤) → 𝑦 = 𝑧) |
24 | 21, 22, 23 | syl2anb 599 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ {𝑤} ∧ 𝑧 ∈ {𝑤}) → 𝑦 = 𝑧) |
25 | 20, 24 | syl6bi 255 |
. . . . . . . . 9
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑦 ∈ (𝐹 “ {𝑥}) ∧ 𝑧 ∈ (𝐹 “ {𝑥})) → 𝑦 = 𝑧)) |
26 | 17, 25 | syl5bi 244 |
. . . . . . . 8
⊢ ((𝐹 “ {𝑥}) = {𝑤} → ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧)) |
27 | 26 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑤(𝐹 “ {𝑥}) = {𝑤} → ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧)) |
28 | 27 | impl 458 |
. . . . . 6
⊢
(((∃𝑤(𝐹 “ {𝑥}) = {𝑤} ∧ 𝑥𝐹𝑦) ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧) |
29 | 9, 28 | sylanb 583 |
. . . . 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 1796 |
. . 3
⊢
∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧) |
32 | 31 | ax-gen 1795 |
. 2
⊢
∀𝑥∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧) |
33 | | df-funpart 33339 |
. . . 4
⊢
Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) |
34 | 33 | funeqi 6379 |
. . 3
⊢ (Fun
Funpart𝐹 ↔ Fun (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons )))) |
35 | | dffun2 6368 |
. . 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 277 |
. 2
⊢ (Fun
Funpart𝐹 ↔ (Rel (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
× Singletons ))) ∧ ∀𝑥∀𝑦∀𝑧((𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑦 ∧ 𝑥(𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))𝑧) → 𝑦 = 𝑧))) |
37 | 1, 32, 36 | mpbir2an 709 |
1
⊢ Fun
Funpart𝐹 |