Step | Hyp | Ref
| Expression |
1 | | claut 38856 |
. 2
class
LAut |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3475 |
. . 3
class
V |
4 | 2 | cv 1541 |
. . . . . . 7
class π |
5 | | cbs 17144 |
. . . . . . 7
class
Base |
6 | 4, 5 | cfv 6544 |
. . . . . 6
class
(Baseβπ) |
7 | | vf |
. . . . . . 7
setvar π |
8 | 7 | cv 1541 |
. . . . . 6
class π |
9 | 6, 6, 8 | wf1o 6543 |
. . . . 5
wff π:(Baseβπ)β1-1-ontoβ(Baseβπ) |
10 | | vx |
. . . . . . . . . 10
setvar π₯ |
11 | 10 | cv 1541 |
. . . . . . . . 9
class π₯ |
12 | | vy |
. . . . . . . . . 10
setvar π¦ |
13 | 12 | cv 1541 |
. . . . . . . . 9
class π¦ |
14 | | cple 17204 |
. . . . . . . . . 10
class
le |
15 | 4, 14 | cfv 6544 |
. . . . . . . . 9
class
(leβπ) |
16 | 11, 13, 15 | wbr 5149 |
. . . . . . . 8
wff π₯(leβπ)π¦ |
17 | 11, 8 | cfv 6544 |
. . . . . . . . 9
class (πβπ₯) |
18 | 13, 8 | cfv 6544 |
. . . . . . . . 9
class (πβπ¦) |
19 | 17, 18, 15 | wbr 5149 |
. . . . . . . 8
wff (πβπ₯)(leβπ)(πβπ¦) |
20 | 16, 19 | wb 205 |
. . . . . . 7
wff (π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)) |
21 | 20, 12, 6 | wral 3062 |
. . . . . 6
wff
βπ¦ β
(Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)) |
22 | 21, 10, 6 | wral 3062 |
. . . . 5
wff
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)) |
23 | 9, 22 | wa 397 |
. . . 4
wff (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦))) |
24 | 23, 7 | cab 2710 |
. . 3
class {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)))} |
25 | 2, 3, 24 | cmpt 5232 |
. 2
class (π β V β¦ {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)))}) |
26 | 1, 25 | wceq 1542 |
1
wff LAut =
(π β V β¦ {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)))}) |