Step | Hyp | Ref
| Expression |
1 | | ssv 3291 |
. . . . . 6
⊢ F ⊆
V |
2 | | 1stfo 5505 |
. . . . . . 7
⊢ 1st
:V–onto→V |
3 | | fofn 5271 |
. . . . . . 7
⊢ (1st
:V–onto→V → 1st
Fn V) |
4 | | fnssresb 5195 |
. . . . . . 7
⊢ (1st Fn
V → ((1st ↾ F) Fn F ↔
F ⊆
V)) |
5 | 2, 3, 4 | mp2b 9 |
. . . . . 6
⊢ ((1st
↾ F) Fn
F ↔ F ⊆
V) |
6 | 1, 5 | mpbir 200 |
. . . . 5
⊢ (1st
↾ F) Fn
F |
7 | 6 | a1i 10 |
. . . 4
⊢ (Fun F → (1st ↾ F) Fn
F) |
8 | | brcnv 4892 |
. . . . . . . . . . 11
⊢ (x◡(1st ↾ F)y ↔ y(1st ↾ F)x) |
9 | | brres 4949 |
. . . . . . . . . . 11
⊢ (y(1st ↾ F)x ↔ (y1st x ∧ y ∈ F)) |
10 | | vex 2862 |
. . . . . . . . . . . . . 14
⊢ x ∈
V |
11 | 10 | br1st 4858 |
. . . . . . . . . . . . 13
⊢ (y1st x ↔ ∃a y = 〈x, a〉) |
12 | 11 | anbi1i 676 |
. . . . . . . . . . . 12
⊢ ((y1st x ∧ y ∈ F) ↔ (∃a y = 〈x, a〉 ∧ y ∈ F)) |
13 | | 19.41v 1901 |
. . . . . . . . . . . 12
⊢ (∃a(y = 〈x, a〉 ∧ y ∈ F) ↔ (∃a y = 〈x, a〉 ∧ y ∈ F)) |
14 | 12, 13 | bitr4i 243 |
. . . . . . . . . . 11
⊢ ((y1st x ∧ y ∈ F) ↔ ∃a(y = 〈x, a〉 ∧ y ∈ F)) |
15 | 8, 9, 14 | 3bitri 262 |
. . . . . . . . . 10
⊢ (x◡(1st ↾ F)y ↔ ∃a(y = 〈x, a〉 ∧ y ∈ F)) |
16 | | brcnv 4892 |
. . . . . . . . . . . 12
⊢ (x◡(1st ↾ F)z ↔ z(1st ↾ F)x) |
17 | | brres 4949 |
. . . . . . . . . . . 12
⊢ (z(1st ↾ F)x ↔ (z1st x ∧ z ∈ F)) |
18 | 10 | br1st 4858 |
. . . . . . . . . . . . 13
⊢ (z1st x ↔ ∃b z = 〈x, b〉) |
19 | 18 | anbi1i 676 |
. . . . . . . . . . . 12
⊢ ((z1st x ∧ z ∈ F) ↔ (∃b z = 〈x, b〉 ∧ z ∈ F)) |
20 | 16, 17, 19 | 3bitri 262 |
. . . . . . . . . . 11
⊢ (x◡(1st ↾ F)z ↔ (∃b z = 〈x, b〉 ∧ z ∈ F)) |
21 | | 19.41v 1901 |
. . . . . . . . . . 11
⊢ (∃b(z = 〈x, b〉 ∧ z ∈ F) ↔ (∃b z = 〈x, b〉 ∧ z ∈ F)) |
22 | 20, 21 | bitr4i 243 |
. . . . . . . . . 10
⊢ (x◡(1st ↾ F)z ↔ ∃b(z = 〈x, b〉 ∧ z ∈ F)) |
23 | 15, 22 | anbi12i 678 |
. . . . . . . . 9
⊢ ((x◡(1st ↾ F)y ∧ x◡(1st ↾ F)z) ↔ (∃a(y = 〈x, a〉 ∧ y ∈ F) ∧ ∃b(z = 〈x, b〉 ∧ z ∈ F))) |
24 | | eeanv 1913 |
. . . . . . . . 9
⊢ (∃a∃b((y = 〈x, a〉 ∧ y ∈ F) ∧ (z = 〈x, b〉 ∧ z ∈ F)) ↔ (∃a(y = 〈x, a〉 ∧ y ∈ F) ∧ ∃b(z = 〈x, b〉 ∧ z ∈ F))) |
25 | 23, 24 | bitr4i 243 |
. . . . . . . 8
⊢ ((x◡(1st ↾ F)y ∧ x◡(1st ↾ F)z) ↔ ∃a∃b((y = 〈x, a〉 ∧ y ∈ F) ∧ (z = 〈x, b〉 ∧ z ∈ F))) |
26 | | an4 797 |
. . . . . . . . . 10
⊢ (((y = 〈x, a〉 ∧ y ∈ F) ∧ (z = 〈x, b〉 ∧ z ∈ F)) ↔ ((y =
〈x,
a〉 ∧ z = 〈x, b〉) ∧ (y ∈ F ∧ z ∈ F))) |
27 | | dffun4 5121 |
. . . . . . . . . . . . 13
⊢ (Fun F ↔ ∀x∀a∀b((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → a =
b)) |
28 | | sp 1747 |
. . . . . . . . . . . . . . 15
⊢ (∀b((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → a =
b) → ((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → a =
b)) |
29 | 28 | sps 1754 |
. . . . . . . . . . . . . 14
⊢ (∀a∀b((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → a =
b) → ((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → a =
b)) |
30 | 29 | sps 1754 |
. . . . . . . . . . . . 13
⊢ (∀x∀a∀b((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → a =
b) → ((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → a =
b)) |
31 | 27, 30 | sylbi 187 |
. . . . . . . . . . . 12
⊢ (Fun F → ((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → a =
b)) |
32 | | opeq2 4579 |
. . . . . . . . . . . 12
⊢ (a = b →
〈x,
a〉 =
〈x,
b〉) |
33 | 31, 32 | syl6 29 |
. . . . . . . . . . 11
⊢ (Fun F → ((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → 〈x, a〉 = 〈x, b〉)) |
34 | | eleq1 2413 |
. . . . . . . . . . . . . . 15
⊢ (y = 〈x, a〉 → (y
∈ F
↔ 〈x, a〉 ∈ F)) |
35 | | eleq1 2413 |
. . . . . . . . . . . . . . 15
⊢ (z = 〈x, b〉 → (z
∈ F
↔ 〈x, b〉 ∈ F)) |
36 | 34, 35 | bi2anan9 843 |
. . . . . . . . . . . . . 14
⊢ ((y = 〈x, a〉 ∧ z = 〈x, b〉) → ((y
∈ F ∧ z ∈ F) ↔
(〈x,
a〉 ∈ F ∧ 〈x, b〉 ∈ F))) |
37 | | eqeq12 2365 |
. . . . . . . . . . . . . 14
⊢ ((y = 〈x, a〉 ∧ z = 〈x, b〉) → (y =
z ↔ 〈x, a〉 = 〈x, b〉)) |
38 | 36, 37 | imbi12d 311 |
. . . . . . . . . . . . 13
⊢ ((y = 〈x, a〉 ∧ z = 〈x, b〉) → (((y
∈ F ∧ z ∈ F) →
y = z)
↔ ((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) →
〈x,
a〉 =
〈x,
b〉))) |
39 | 38 | biimprcd 216 |
. . . . . . . . . . . 12
⊢ (((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → 〈x, a〉 = 〈x, b〉) →
((y = 〈x, a〉 ∧ z = 〈x, b〉) →
((y ∈
F ∧
z ∈
F) → y = z))) |
40 | 39 | imp3a 420 |
. . . . . . . . . . 11
⊢ (((〈x, a〉 ∈ F ∧ 〈x, b〉 ∈ F) → 〈x, a〉 = 〈x, b〉) →
(((y = 〈x, a〉 ∧ z = 〈x, b〉) ∧ (y ∈ F ∧ z ∈ F)) →
y = z)) |
41 | 33, 40 | syl 15 |
. . . . . . . . . 10
⊢ (Fun F → (((y =
〈x,
a〉 ∧ z = 〈x, b〉) ∧ (y ∈ F ∧ z ∈ F)) →
y = z)) |
42 | 26, 41 | syl5bi 208 |
. . . . . . . . 9
⊢ (Fun F → (((y =
〈x,
a〉 ∧ y ∈ F) ∧ (z = 〈x, b〉 ∧ z ∈ F)) →
y = z)) |
43 | 42 | exlimdvv 1637 |
. . . . . . . 8
⊢ (Fun F → (∃a∃b((y = 〈x, a〉 ∧ y ∈ F) ∧ (z = 〈x, b〉 ∧ z ∈ F)) → y =
z)) |
44 | 25, 43 | syl5bi 208 |
. . . . . . 7
⊢ (Fun F → ((x◡(1st ↾ F)y ∧ x◡(1st ↾ F)z) → y =
z)) |
45 | 44 | alrimiv 1631 |
. . . . . 6
⊢ (Fun F → ∀z((x◡(1st ↾ F)y ∧ x◡(1st ↾ F)z) → y =
z)) |
46 | 45 | alrimivv 1632 |
. . . . 5
⊢ (Fun F → ∀x∀y∀z((x◡(1st ↾ F)y ∧ x◡(1st ↾ F)z) → y =
z)) |
47 | | dffun2 5119 |
. . . . 5
⊢ (Fun ◡(1st ↾ F) ↔
∀x∀y∀z((x◡(1st ↾ F)y ∧ x◡(1st ↾ F)z) → y =
z)) |
48 | 46, 47 | sylibr 203 |
. . . 4
⊢ (Fun F → Fun ◡(1st ↾ F)) |
49 | | dfdm4 5507 |
. . . . . 6
⊢ dom F = (1st “ F) |
50 | | dfima3 4951 |
. . . . . 6
⊢ (1st
“ F) = ran (1st ↾ F) |
51 | 49, 50 | eqtr2i 2374 |
. . . . 5
⊢ ran (1st
↾ F) =
dom F |
52 | 51 | a1i 10 |
. . . 4
⊢ (Fun F → ran (1st ↾ F) = dom
F) |
53 | | dff1o2 5291 |
. . . 4
⊢ ((1st
↾ F):F–1-1-onto→dom F
↔ ((1st ↾ F) Fn F ∧ Fun ◡(1st ↾ F) ∧ ran (1st ↾ F) = dom
F)) |
54 | 7, 48, 52, 53 | syl3anbrc 1136 |
. . 3
⊢ (Fun F → (1st ↾ F):F–1-1-onto→dom
F) |
55 | | 1stex 4739 |
. . . . 5
⊢ 1st
∈ V |
56 | | fundmen.1 |
. . . . 5
⊢ F ∈
V |
57 | 55, 56 | resex 5117 |
. . . 4
⊢ (1st
↾ F)
∈ V |
58 | 57 | f1oen 6033 |
. . 3
⊢ ((1st
↾ F):F–1-1-onto→dom F
→ F ≈ dom F) |
59 | 54, 58 | syl 15 |
. 2
⊢ (Fun F → F
≈ dom F) |
60 | | ensym 6037 |
. 2
⊢ (F ≈ dom F
↔ dom F ≈ F) |
61 | 59, 60 | sylib 188 |
1
⊢ (Fun F → dom F
≈ F) |