Step | Hyp | Ref
| Expression |
1 | | opelf 6704 |
. . . . . . . 8
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐵})) |
2 | | velsn 4603 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
3 | | velsn 4603 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵) |
4 | 2, 3 | anbi12i 628 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
5 | 1, 4 | sylib 217 |
. . . . . . 7
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
6 | 5 | ex 414 |
. . . . . 6
⊢ (𝐹:{𝐴}⟶{𝐵} → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) |
7 | | fsn.1 |
. . . . . . . . . 10
⊢ 𝐴 ∈ V |
8 | 7 | snid 4623 |
. . . . . . . . 9
⊢ 𝐴 ∈ {𝐴} |
9 | | feu 6719 |
. . . . . . . . 9
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ 𝐴 ∈ {𝐴}) → ∃!𝑦 ∈ {𝐵}⟨𝐴, 𝑦⟩ ∈ 𝐹) |
10 | 8, 9 | mpan2 690 |
. . . . . . . 8
⊢ (𝐹:{𝐴}⟶{𝐵} → ∃!𝑦 ∈ {𝐵}⟨𝐴, 𝑦⟩ ∈ 𝐹) |
11 | 3 | anbi1i 625 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ {𝐵} ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ↔ (𝑦 = 𝐵 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹)) |
12 | | opeq2 4832 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
13 | 12 | eleq1d 2819 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐹)) |
14 | 13 | pm5.32i 576 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝐵 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ↔ (𝑦 = 𝐵 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐹)) |
15 | 14 | biancomi 464 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝐵 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵)) |
16 | 11, 15 | bitr2i 276 |
. . . . . . . . . 10
⊢
((⟨𝐴, 𝐵⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ {𝐵} ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹)) |
17 | 16 | eubii 2580 |
. . . . . . . . 9
⊢
(∃!𝑦(⟨𝐴, 𝐵⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ ∃!𝑦(𝑦 ∈ {𝐵} ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹)) |
18 | | fsn.2 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
19 | 18 | eueqi 3668 |
. . . . . . . . . . 11
⊢
∃!𝑦 𝑦 = 𝐵 |
20 | 19 | biantru 531 |
. . . . . . . . . 10
⊢
(⟨𝐴, 𝐵⟩ ∈ 𝐹 ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐹 ∧ ∃!𝑦 𝑦 = 𝐵)) |
21 | | euanv 2621 |
. . . . . . . . . 10
⊢
(∃!𝑦(⟨𝐴, 𝐵⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐹 ∧ ∃!𝑦 𝑦 = 𝐵)) |
22 | 20, 21 | bitr4i 278 |
. . . . . . . . 9
⊢
(⟨𝐴, 𝐵⟩ ∈ 𝐹 ↔ ∃!𝑦(⟨𝐴, 𝐵⟩ ∈ 𝐹 ∧ 𝑦 = 𝐵)) |
23 | | df-reu 3353 |
. . . . . . . . 9
⊢
(∃!𝑦 ∈
{𝐵}⟨𝐴, 𝑦⟩ ∈ 𝐹 ↔ ∃!𝑦(𝑦 ∈ {𝐵} ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹)) |
24 | 17, 22, 23 | 3bitr4i 303 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ ∈ 𝐹 ↔ ∃!𝑦 ∈ {𝐵}⟨𝐴, 𝑦⟩ ∈ 𝐹) |
25 | 10, 24 | sylibr 233 |
. . . . . . 7
⊢ (𝐹:{𝐴}⟶{𝐵} → ⟨𝐴, 𝐵⟩ ∈ 𝐹) |
26 | | opeq12 4833 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
27 | 26 | eleq1d 2819 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐹)) |
28 | 25, 27 | syl5ibrcom 247 |
. . . . . 6
⊢ (𝐹:{𝐴}⟶{𝐵} → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ⟨𝑥, 𝑦⟩ ∈ 𝐹)) |
29 | 6, 28 | impbid 211 |
. . . . 5
⊢ (𝐹:{𝐴}⟶{𝐵} → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) |
30 | | opex 5422 |
. . . . . . 7
⊢
⟨𝑥, 𝑦⟩ ∈ V |
31 | 30 | elsn 4602 |
. . . . . 6
⊢
(⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩} ↔ ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
32 | 7, 18 | opth2 5438 |
. . . . . 6
⊢
(⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
33 | 31, 32 | bitr2i 276 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩}) |
34 | 29, 33 | bitrdi 287 |
. . . 4
⊢ (𝐹:{𝐴}⟶{𝐵} → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩})) |
35 | 34 | alrimivv 1932 |
. . 3
⊢ (𝐹:{𝐴}⟶{𝐵} → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩})) |
36 | | frel 6674 |
. . . 4
⊢ (𝐹:{𝐴}⟶{𝐵} → Rel 𝐹) |
37 | 7, 18 | relsnop 5762 |
. . . 4
⊢ Rel
{⟨𝐴, 𝐵⟩} |
38 | | eqrel 5741 |
. . . 4
⊢ ((Rel
𝐹 ∧ Rel {⟨𝐴, 𝐵⟩}) → (𝐹 = {⟨𝐴, 𝐵⟩} ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩}))) |
39 | 36, 37, 38 | sylancl 587 |
. . 3
⊢ (𝐹:{𝐴}⟶{𝐵} → (𝐹 = {⟨𝐴, 𝐵⟩} ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝐴, 𝐵⟩}))) |
40 | 35, 39 | mpbird 257 |
. 2
⊢ (𝐹:{𝐴}⟶{𝐵} → 𝐹 = {⟨𝐴, 𝐵⟩}) |
41 | 7, 18 | f1osn 6825 |
. . . 4
⊢
{⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵} |
42 | | f1oeq1 6773 |
. . . 4
⊢ (𝐹 = {⟨𝐴, 𝐵⟩} → (𝐹:{𝐴}–1-1-onto→{𝐵} ↔ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})) |
43 | 41, 42 | mpbiri 258 |
. . 3
⊢ (𝐹 = {⟨𝐴, 𝐵⟩} → 𝐹:{𝐴}–1-1-onto→{𝐵}) |
44 | | f1of 6785 |
. . 3
⊢ (𝐹:{𝐴}–1-1-onto→{𝐵} → 𝐹:{𝐴}⟶{𝐵}) |
45 | 43, 44 | syl 17 |
. 2
⊢ (𝐹 = {⟨𝐴, 𝐵⟩} → 𝐹:{𝐴}⟶{𝐵}) |
46 | 40, 45 | impbii 208 |
1
⊢ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {⟨𝐴, 𝐵⟩}) |