Step | Hyp | Ref
| Expression |
1 | | opelf 5369 |
. . . . . . . 8
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐵})) |
2 | | velsn 3600 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
3 | | velsn 3600 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵) |
4 | 2, 3 | anbi12i 457 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
5 | 1, 4 | sylib 121 |
. . . . . . 7
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
6 | 5 | ex 114 |
. . . . . 6
⊢ (𝐹:{𝐴}⟶{𝐵} → (〈𝑥, 𝑦〉 ∈ 𝐹 → (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) |
7 | | fsn.1 |
. . . . . . . . . 10
⊢ 𝐴 ∈ V |
8 | 7 | snid 3614 |
. . . . . . . . 9
⊢ 𝐴 ∈ {𝐴} |
9 | | feu 5380 |
. . . . . . . . 9
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ 𝐴 ∈ {𝐴}) → ∃!𝑦 ∈ {𝐵}〈𝐴, 𝑦〉 ∈ 𝐹) |
10 | 8, 9 | mpan2 423 |
. . . . . . . 8
⊢ (𝐹:{𝐴}⟶{𝐵} → ∃!𝑦 ∈ {𝐵}〈𝐴, 𝑦〉 ∈ 𝐹) |
11 | 3 | anbi1i 455 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ {𝐵} ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (𝑦 = 𝐵 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) |
12 | | opeq2 3766 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) |
13 | 12 | eleq1d 2239 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (〈𝐴, 𝑦〉 ∈ 𝐹 ↔ 〈𝐴, 𝐵〉 ∈ 𝐹)) |
14 | 13 | pm5.32i 451 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝐵 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (𝑦 = 𝐵 ∧ 〈𝐴, 𝐵〉 ∈ 𝐹)) |
15 | | ancom 264 |
. . . . . . . . . . . 12
⊢
((〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ (𝑦 = 𝐵 ∧ 〈𝐴, 𝐵〉 ∈ 𝐹)) |
16 | 14, 15 | bitr4i 186 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝐵 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵)) |
17 | 11, 16 | bitr2i 184 |
. . . . . . . . . 10
⊢
((〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ {𝐵} ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) |
18 | 17 | eubii 2028 |
. . . . . . . . 9
⊢
(∃!𝑦(〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ ∃!𝑦(𝑦 ∈ {𝐵} ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) |
19 | | fsn.2 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
20 | 19 | eueq1 2902 |
. . . . . . . . . . 11
⊢
∃!𝑦 𝑦 = 𝐵 |
21 | 20 | biantru 300 |
. . . . . . . . . 10
⊢
(〈𝐴, 𝐵〉 ∈ 𝐹 ↔ (〈𝐴, 𝐵〉 ∈ 𝐹 ∧ ∃!𝑦 𝑦 = 𝐵)) |
22 | | euanv 2076 |
. . . . . . . . . 10
⊢
(∃!𝑦(〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ (〈𝐴, 𝐵〉 ∈ 𝐹 ∧ ∃!𝑦 𝑦 = 𝐵)) |
23 | 21, 22 | bitr4i 186 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 ∈ 𝐹 ↔ ∃!𝑦(〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵)) |
24 | | df-reu 2455 |
. . . . . . . . 9
⊢
(∃!𝑦 ∈
{𝐵}〈𝐴, 𝑦〉 ∈ 𝐹 ↔ ∃!𝑦(𝑦 ∈ {𝐵} ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) |
25 | 18, 23, 24 | 3bitr4i 211 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ 𝐹 ↔ ∃!𝑦 ∈ {𝐵}〈𝐴, 𝑦〉 ∈ 𝐹) |
26 | 10, 25 | sylibr 133 |
. . . . . . 7
⊢ (𝐹:{𝐴}⟶{𝐵} → 〈𝐴, 𝐵〉 ∈ 𝐹) |
27 | | opeq12 3767 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
28 | 27 | eleq1d 2239 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝐴, 𝐵〉 ∈ 𝐹)) |
29 | 26, 28 | syl5ibrcom 156 |
. . . . . 6
⊢ (𝐹:{𝐴}⟶{𝐵} → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝐹)) |
30 | 6, 29 | impbid 128 |
. . . . 5
⊢ (𝐹:{𝐴}⟶{𝐵} → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) |
31 | | vex 2733 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
32 | | vex 2733 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
33 | 31, 32 | opex 4214 |
. . . . . . 7
⊢
〈𝑥, 𝑦〉 ∈ V |
34 | 33 | elsn 3599 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉} ↔ 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
35 | 7, 19 | opth2 4225 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
36 | 34, 35 | bitr2i 184 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉}) |
37 | 30, 36 | bitrdi 195 |
. . . 4
⊢ (𝐹:{𝐴}⟶{𝐵} → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉})) |
38 | 37 | alrimivv 1868 |
. . 3
⊢ (𝐹:{𝐴}⟶{𝐵} → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉})) |
39 | | frel 5352 |
. . . 4
⊢ (𝐹:{𝐴}⟶{𝐵} → Rel 𝐹) |
40 | 7, 19 | relsnop 4717 |
. . . 4
⊢ Rel
{〈𝐴, 𝐵〉} |
41 | | eqrel 4700 |
. . . 4
⊢ ((Rel
𝐹 ∧ Rel {〈𝐴, 𝐵〉}) → (𝐹 = {〈𝐴, 𝐵〉} ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉}))) |
42 | 39, 40, 41 | sylancl 411 |
. . 3
⊢ (𝐹:{𝐴}⟶{𝐵} → (𝐹 = {〈𝐴, 𝐵〉} ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉}))) |
43 | 38, 42 | mpbird 166 |
. 2
⊢ (𝐹:{𝐴}⟶{𝐵} → 𝐹 = {〈𝐴, 𝐵〉}) |
44 | 7, 19 | f1osn 5482 |
. . . 4
⊢
{〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵} |
45 | | f1oeq1 5431 |
. . . 4
⊢ (𝐹 = {〈𝐴, 𝐵〉} → (𝐹:{𝐴}–1-1-onto→{𝐵} ↔ {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵})) |
46 | 44, 45 | mpbiri 167 |
. . 3
⊢ (𝐹 = {〈𝐴, 𝐵〉} → 𝐹:{𝐴}–1-1-onto→{𝐵}) |
47 | | f1of 5442 |
. . 3
⊢ (𝐹:{𝐴}–1-1-onto→{𝐵} → 𝐹:{𝐴}⟶{𝐵}) |
48 | 46, 47 | syl 14 |
. 2
⊢ (𝐹 = {〈𝐴, 𝐵〉} → 𝐹:{𝐴}⟶{𝐵}) |
49 | 43, 48 | impbii 125 |
1
⊢ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉}) |