Step | Hyp | Ref
| Expression |
1 | | opelf 5236 |
. . . . . . 7
⊢ ((F:{A}–→{B} ∧ ⟨x, y⟩ ∈ F) →
(x ∈
{A} ∧
y ∈
{B})) |
2 | | elsn 3749 |
. . . . . . . 8
⊢ (x ∈ {A} ↔ x =
A) |
3 | | elsn 3749 |
. . . . . . . 8
⊢ (y ∈ {B} ↔ y =
B) |
4 | 2, 3 | anbi12i 678 |
. . . . . . 7
⊢ ((x ∈ {A} ∧ y ∈ {B}) ↔ (x =
A ∧
y = B)) |
5 | 1, 4 | sylib 188 |
. . . . . 6
⊢ ((F:{A}–→{B} ∧ ⟨x, y⟩ ∈ F) →
(x = A
∧ y =
B)) |
6 | 5 | ex 423 |
. . . . 5
⊢ (F:{A}–→{B} → (⟨x, y⟩ ∈ F →
(x = A
∧ y =
B))) |
7 | | fsn.1 |
. . . . . . . . 9
⊢ A ∈
V |
8 | 7 | snid 3761 |
. . . . . . . 8
⊢ A ∈ {A} |
9 | | feu 5243 |
. . . . . . . 8
⊢ ((F:{A}–→{B} ∧ A ∈ {A}) → ∃!y ∈ {B}⟨A, y⟩ ∈ F) |
10 | 8, 9 | mpan2 652 |
. . . . . . 7
⊢ (F:{A}–→{B} → ∃!y ∈ {B}⟨A, y⟩ ∈ F) |
11 | 3 | anbi1i 676 |
. . . . . . . . . 10
⊢ ((y ∈ {B} ∧ ⟨A, y⟩ ∈ F) ↔
(y = B
∧ ⟨A, y⟩ ∈ F)) |
12 | | opeq2 4580 |
. . . . . . . . . . . . 13
⊢ (y = B →
⟨A,
y⟩ =
⟨A,
B⟩) |
13 | 12 | eleq1d 2419 |
. . . . . . . . . . . 12
⊢ (y = B →
(⟨A,
y⟩ ∈ F ↔
⟨A,
B⟩ ∈ F)) |
14 | 13 | pm5.32i 618 |
. . . . . . . . . . 11
⊢ ((y = B ∧ ⟨A, y⟩ ∈ F) ↔ (y =
B ∧ ⟨A, B⟩ ∈ F)) |
15 | | ancom 437 |
. . . . . . . . . . 11
⊢ ((⟨A, B⟩ ∈ F ∧ y = B) ↔ (y =
B ∧ ⟨A, B⟩ ∈ F)) |
16 | 14, 15 | bitr4i 243 |
. . . . . . . . . 10
⊢ ((y = B ∧ ⟨A, y⟩ ∈ F) ↔ (⟨A, B⟩ ∈ F ∧ y = B)) |
17 | 11, 16 | bitr2i 241 |
. . . . . . . . 9
⊢ ((⟨A, B⟩ ∈ F ∧ y = B) ↔ (y
∈ {B}
∧ ⟨A, y⟩ ∈ F)) |
18 | 17 | eubii 2213 |
. . . . . . . 8
⊢ (∃!y(⟨A, B⟩ ∈ F ∧ y = B) ↔ ∃!y(y ∈ {B} ∧ ⟨A, y⟩ ∈ F)) |
19 | | fsn.2 |
. . . . . . . . . . 11
⊢ B ∈
V |
20 | 19 | eueq1 3010 |
. . . . . . . . . 10
⊢ ∃!y y = B |
21 | 20 | biantru 491 |
. . . . . . . . 9
⊢ (⟨A, B⟩ ∈ F ↔
(⟨A,
B⟩ ∈ F ∧ ∃!y y = B)) |
22 | | euanv 2265 |
. . . . . . . . 9
⊢ (∃!y(⟨A, B⟩ ∈ F ∧ y = B) ↔ (⟨A, B⟩ ∈ F ∧ ∃!y y = B)) |
23 | 21, 22 | bitr4i 243 |
. . . . . . . 8
⊢ (⟨A, B⟩ ∈ F ↔
∃!y(⟨A, B⟩ ∈ F ∧ y = B)) |
24 | | df-reu 2622 |
. . . . . . . 8
⊢ (∃!y ∈ {B}⟨A, y⟩ ∈ F ↔
∃!y(y ∈ {B} ∧ ⟨A, y⟩ ∈ F)) |
25 | 18, 23, 24 | 3bitr4i 268 |
. . . . . . 7
⊢ (⟨A, B⟩ ∈ F ↔
∃!y
∈ {B}⟨A, y⟩ ∈ F) |
26 | 10, 25 | sylibr 203 |
. . . . . 6
⊢ (F:{A}–→{B} → ⟨A, B⟩ ∈ F) |
27 | | opeq12 4581 |
. . . . . . 7
⊢ ((x = A ∧ y = B) → ⟨x, y⟩ = ⟨A, B⟩) |
28 | 27 | eleq1d 2419 |
. . . . . 6
⊢ ((x = A ∧ y = B) → (⟨x, y⟩ ∈ F ↔
⟨A,
B⟩ ∈ F)) |
29 | 26, 28 | syl5ibrcom 213 |
. . . . 5
⊢ (F:{A}–→{B} → ((x =
A ∧
y = B)
→ ⟨x, y⟩ ∈ F)) |
30 | 6, 29 | impbid 183 |
. . . 4
⊢ (F:{A}–→{B} → (⟨x, y⟩ ∈ F ↔
(x = A
∧ y =
B))) |
31 | | vex 2863 |
. . . . . . 7
⊢ x ∈
V |
32 | | vex 2863 |
. . . . . . 7
⊢ y ∈
V |
33 | 31, 32 | opex 4589 |
. . . . . 6
⊢ ⟨x, y⟩ ∈ V |
34 | 33 | elsnc 3757 |
. . . . 5
⊢ (⟨x, y⟩ ∈ {⟨A, B⟩} ↔ ⟨x, y⟩ = ⟨A, B⟩) |
35 | | opth 4603 |
. . . . 5
⊢ (⟨x, y⟩ = ⟨A, B⟩ ↔
(x = A
∧ y =
B)) |
36 | 34, 35 | bitr2i 241 |
. . . 4
⊢ ((x = A ∧ y = B) ↔ ⟨x, y⟩ ∈ {⟨A, B⟩}) |
37 | 30, 36 | syl6bb 252 |
. . 3
⊢ (F:{A}–→{B} → (⟨x, y⟩ ∈ F ↔
⟨x,
y⟩ ∈ {⟨A, B⟩})) |
38 | 37 | eqrelrdv 4853 |
. 2
⊢ (F:{A}–→{B} → F =
{⟨A,
B⟩}) |
39 | 7, 19 | f1osn 5323 |
. . . 4
⊢ {⟨A, B⟩}:{A}–1-1-onto→{B} |
40 | | f1oeq1 5282 |
. . . 4
⊢ (F = {⟨A, B⟩} → (F:{A}–1-1-onto→{B} ↔
{⟨A,
B⟩}:{A}–1-1-onto→{B})) |
41 | 39, 40 | mpbiri 224 |
. . 3
⊢ (F = {⟨A, B⟩} → F:{A}–1-1-onto→{B}) |
42 | | f1of 5288 |
. . 3
⊢ (F:{A}–1-1-onto→{B} →
F:{A}–→{B}) |
43 | 41, 42 | syl 15 |
. 2
⊢ (F = {⟨A, B⟩} → F:{A}–→{B}) |
44 | 38, 43 | impbii 180 |
1
⊢ (F:{A}–→{B} ↔ F =
{⟨A,
B⟩}) |