Step | Hyp | Ref
| Expression |
1 | | opelf 5005 |
. . . . . . . 8
⊢ ((𝐹:{A}⟶{B}
∧ 〈x,
y〉 ∈
𝐹) → (x ∈ {A} ∧ y ∈ {B})) |
2 | | elsn 3382 |
. . . . . . . . 9
⊢ (x ∈ {A} ↔ x =
A) |
3 | | elsn 3382 |
. . . . . . . . 9
⊢ (y ∈ {B} ↔ y =
B) |
4 | 2, 3 | anbi12i 433 |
. . . . . . . 8
⊢
((x ∈ {A} ∧ y ∈ {B}) ↔
(x = A
∧ y =
B)) |
5 | 1, 4 | sylib 127 |
. . . . . . 7
⊢ ((𝐹:{A}⟶{B}
∧ 〈x,
y〉 ∈
𝐹) → (x = A ∧ y = B)) |
6 | 5 | ex 108 |
. . . . . 6
⊢ (𝐹:{A}⟶{B}
→ (〈x, y〉 ∈ 𝐹 → (x = A ∧ y = B))) |
7 | | fsn.1 |
. . . . . . . . . 10
⊢ A ∈
V |
8 | 7 | snid 3394 |
. . . . . . . . 9
⊢ A ∈ {A} |
9 | | feu 5015 |
. . . . . . . . 9
⊢ ((𝐹:{A}⟶{B}
∧ A ∈ {A}) →
∃!y
∈ {B}〈A,
y〉 ∈
𝐹) |
10 | 8, 9 | mpan2 401 |
. . . . . . . 8
⊢ (𝐹:{A}⟶{B}
→ ∃!y ∈ {B}〈A,
y〉 ∈
𝐹) |
11 | 3 | anbi1i 431 |
. . . . . . . . . . 11
⊢
((y ∈ {B} ∧ 〈A,
y〉 ∈
𝐹) ↔ (y = B ∧ 〈A,
y〉 ∈
𝐹)) |
12 | | opeq2 3541 |
. . . . . . . . . . . . . 14
⊢ (y = B →
〈A, y〉 = 〈A, B〉) |
13 | 12 | eleq1d 2103 |
. . . . . . . . . . . . 13
⊢ (y = B →
(〈A, y〉 ∈ 𝐹 ↔ 〈A, B〉 ∈ 𝐹)) |
14 | 13 | pm5.32i 427 |
. . . . . . . . . . . 12
⊢
((y = B ∧ 〈A, y〉 ∈ 𝐹) ↔ (y = B ∧ 〈A,
B〉 ∈
𝐹)) |
15 | | ancom 253 |
. . . . . . . . . . . 12
⊢
((〈A, B〉 ∈ 𝐹 ∧ y = B) ↔ (y =
B ∧
〈A, B〉 ∈ 𝐹)) |
16 | 14, 15 | bitr4i 176 |
. . . . . . . . . . 11
⊢
((y = B ∧ 〈A, y〉 ∈ 𝐹) ↔ (〈A, B〉 ∈ 𝐹 ∧ y = B)) |
17 | 11, 16 | bitr2i 174 |
. . . . . . . . . 10
⊢
((〈A, B〉 ∈ 𝐹 ∧ y = B) ↔ (y
∈ {B}
∧ 〈A,
y〉 ∈
𝐹)) |
18 | 17 | eubii 1906 |
. . . . . . . . 9
⊢ (∃!y(〈A,
B〉 ∈
𝐹 ∧ y = B) ↔ ∃!y(y ∈ {B} ∧ 〈A, y〉 ∈ 𝐹)) |
19 | | fsn.2 |
. . . . . . . . . . . 12
⊢ B ∈
V |
20 | 19 | eueq1 2707 |
. . . . . . . . . . 11
⊢ ∃!y y = B |
21 | 20 | biantru 286 |
. . . . . . . . . 10
⊢
(〈A, B〉 ∈ 𝐹 ↔ (〈A, B〉 ∈ 𝐹 ∧ ∃!y y = B)) |
22 | | euanv 1954 |
. . . . . . . . . 10
⊢ (∃!y(〈A,
B〉 ∈
𝐹 ∧ y = B) ↔ (〈A, B〉 ∈ 𝐹 ∧ ∃!y y = B)) |
23 | 21, 22 | bitr4i 176 |
. . . . . . . . 9
⊢
(〈A, B〉 ∈ 𝐹 ↔ ∃!y(〈A,
B〉 ∈
𝐹 ∧ y = B)) |
24 | | df-reu 2307 |
. . . . . . . . 9
⊢ (∃!y ∈ {B}〈A,
y〉 ∈
𝐹 ↔ ∃!y(y ∈ {B} ∧ 〈A, y〉 ∈ 𝐹)) |
25 | 18, 23, 24 | 3bitr4i 201 |
. . . . . . . 8
⊢
(〈A, B〉 ∈ 𝐹 ↔ ∃!y ∈ {B}〈A,
y〉 ∈
𝐹) |
26 | 10, 25 | sylibr 137 |
. . . . . . 7
⊢ (𝐹:{A}⟶{B}
→ 〈A, B〉 ∈ 𝐹) |
27 | | opeq12 3542 |
. . . . . . . 8
⊢
((x = A ∧ y = B) →
〈x, y〉 = 〈A, B〉) |
28 | 27 | eleq1d 2103 |
. . . . . . 7
⊢
((x = A ∧ y = B) →
(〈x, y〉 ∈ 𝐹 ↔ 〈A, B〉 ∈ 𝐹)) |
29 | 26, 28 | syl5ibrcom 146 |
. . . . . 6
⊢ (𝐹:{A}⟶{B}
→ ((x = A ∧ y = B) →
〈x, y〉 ∈ 𝐹)) |
30 | 6, 29 | impbid 120 |
. . . . 5
⊢ (𝐹:{A}⟶{B}
→ (〈x, y〉 ∈ 𝐹 ↔ (x = A ∧ y = B))) |
31 | | vex 2554 |
. . . . . . . 8
⊢ x ∈
V |
32 | | vex 2554 |
. . . . . . . 8
⊢ y ∈
V |
33 | 31, 32 | opex 3957 |
. . . . . . 7
⊢
〈x, y〉 ∈
V |
34 | 33 | elsnc 3390 |
. . . . . 6
⊢
(〈x, y〉 ∈
{〈A, B〉} ↔ 〈x, y〉 =
〈A, B〉) |
35 | 7, 19 | opth2 3968 |
. . . . . 6
⊢
(〈x, y〉 = 〈A, B〉
↔ (x = A ∧ y = B)) |
36 | 34, 35 | bitr2i 174 |
. . . . 5
⊢
((x = A ∧ y = B) ↔
〈x, y〉 ∈
{〈A, B〉}) |
37 | 30, 36 | syl6bb 185 |
. . . 4
⊢ (𝐹:{A}⟶{B}
→ (〈x, y〉 ∈ 𝐹 ↔ 〈x, y〉 ∈ {〈A,
B〉})) |
38 | 37 | alrimivv 1752 |
. . 3
⊢ (𝐹:{A}⟶{B}
→ ∀x∀y(〈x,
y〉 ∈
𝐹 ↔ 〈x, y〉 ∈ {〈A,
B〉})) |
39 | | frel 4992 |
. . . 4
⊢ (𝐹:{A}⟶{B}
→ Rel 𝐹) |
40 | 7, 19 | relsnop 4387 |
. . . 4
⊢ Rel
{〈A, B〉} |
41 | | eqrel 4372 |
. . . 4
⊢ ((Rel
𝐹 ∧ Rel {〈A,
B〉}) → (𝐹 = {〈A, B〉}
↔ ∀x∀y(〈x,
y〉 ∈
𝐹 ↔ 〈x, y〉 ∈ {〈A,
B〉}))) |
42 | 39, 40, 41 | sylancl 392 |
. . 3
⊢ (𝐹:{A}⟶{B}
→ (𝐹 = {〈A, B〉}
↔ ∀x∀y(〈x,
y〉 ∈
𝐹 ↔ 〈x, y〉 ∈ {〈A,
B〉}))) |
43 | 38, 42 | mpbird 156 |
. 2
⊢ (𝐹:{A}⟶{B}
→ 𝐹 = {〈A, B〉}) |
44 | 7, 19 | f1osn 5109 |
. . . 4
⊢
{〈A, B〉}:{A}–1-1-onto→{B} |
45 | | f1oeq1 5060 |
. . . 4
⊢ (𝐹 = {〈A, B〉}
→ (𝐹:{A}–1-1-onto→{B} ↔
{〈A, B〉}:{A}–1-1-onto→{B})) |
46 | 44, 45 | mpbiri 157 |
. . 3
⊢ (𝐹 = {〈A, B〉}
→ 𝐹:{A}–1-1-onto→{B}) |
47 | | f1of 5069 |
. . 3
⊢ (𝐹:{A}–1-1-onto→{B} →
𝐹:{A}⟶{B}) |
48 | 46, 47 | syl 14 |
. 2
⊢ (𝐹 = {〈A, B〉}
→ 𝐹:{A}⟶{B}) |
49 | 43, 48 | impbii 117 |
1
⊢ (𝐹:{A}⟶{B}
↔ 𝐹 = {〈A, B〉}) |