Step | Hyp | Ref
| Expression |
1 | | cmps 21456 |
. 2
class
mPwSer |
2 | | vi |
. . 3
setvar π |
3 | | vr |
. . 3
setvar π |
4 | | cvv 3474 |
. . 3
class
V |
5 | | vd |
. . . 4
setvar π |
6 | | vh |
. . . . . . . . 9
setvar β |
7 | 6 | cv 1540 |
. . . . . . . 8
class β |
8 | 7 | ccnv 5675 |
. . . . . . 7
class β‘β |
9 | | cn 12211 |
. . . . . . 7
class
β |
10 | 8, 9 | cima 5679 |
. . . . . 6
class (β‘β β β) |
11 | | cfn 8938 |
. . . . . 6
class
Fin |
12 | 10, 11 | wcel 2106 |
. . . . 5
wff (β‘β β β) β Fin |
13 | | cn0 12471 |
. . . . . 6
class
β0 |
14 | 2 | cv 1540 |
. . . . . 6
class π |
15 | | cmap 8819 |
. . . . . 6
class
βm |
16 | 13, 14, 15 | co 7408 |
. . . . 5
class
(β0 βm π) |
17 | 12, 6, 16 | crab 3432 |
. . . 4
class {β β (β0
βm π)
β£ (β‘β β β) β Fin} |
18 | | vb |
. . . . 5
setvar π |
19 | 3 | cv 1540 |
. . . . . . 7
class π |
20 | | cbs 17143 |
. . . . . . 7
class
Base |
21 | 19, 20 | cfv 6543 |
. . . . . 6
class
(Baseβπ) |
22 | 5 | cv 1540 |
. . . . . 6
class π |
23 | 21, 22, 15 | co 7408 |
. . . . 5
class
((Baseβπ)
βm π) |
24 | | cnx 17125 |
. . . . . . . . 9
class
ndx |
25 | 24, 20 | cfv 6543 |
. . . . . . . 8
class
(Baseβndx) |
26 | 18 | cv 1540 |
. . . . . . . 8
class π |
27 | 25, 26 | cop 4634 |
. . . . . . 7
class
β¨(Baseβndx), πβ© |
28 | | cplusg 17196 |
. . . . . . . . 9
class
+g |
29 | 24, 28 | cfv 6543 |
. . . . . . . 8
class
(+gβndx) |
30 | 19, 28 | cfv 6543 |
. . . . . . . . . 10
class
(+gβπ) |
31 | 30 | cof 7667 |
. . . . . . . . 9
class
βf (+gβπ) |
32 | 26, 26 | cxp 5674 |
. . . . . . . . 9
class (π Γ π) |
33 | 31, 32 | cres 5678 |
. . . . . . . 8
class (
βf (+gβπ) βΎ (π Γ π)) |
34 | 29, 33 | cop 4634 |
. . . . . . 7
class
β¨(+gβndx), ( βf
(+gβπ)
βΎ (π Γ π))β© |
35 | | cmulr 17197 |
. . . . . . . . 9
class
.r |
36 | 24, 35 | cfv 6543 |
. . . . . . . 8
class
(.rβndx) |
37 | | vf |
. . . . . . . . 9
setvar π |
38 | | vg |
. . . . . . . . 9
setvar π |
39 | | vk |
. . . . . . . . . 10
setvar π |
40 | | vx |
. . . . . . . . . . . 12
setvar π₯ |
41 | | vy |
. . . . . . . . . . . . . . 15
setvar π¦ |
42 | 41 | cv 1540 |
. . . . . . . . . . . . . 14
class π¦ |
43 | 39 | cv 1540 |
. . . . . . . . . . . . . 14
class π |
44 | | cle 11248 |
. . . . . . . . . . . . . . 15
class
β€ |
45 | 44 | cofr 7668 |
. . . . . . . . . . . . . 14
class
βr β€ |
46 | 42, 43, 45 | wbr 5148 |
. . . . . . . . . . . . 13
wff π¦ βr β€ π |
47 | 46, 41, 22 | crab 3432 |
. . . . . . . . . . . 12
class {π¦ β π β£ π¦ βr β€ π} |
48 | 40 | cv 1540 |
. . . . . . . . . . . . . 14
class π₯ |
49 | 37 | cv 1540 |
. . . . . . . . . . . . . 14
class π |
50 | 48, 49 | cfv 6543 |
. . . . . . . . . . . . 13
class (πβπ₯) |
51 | | cmin 11443 |
. . . . . . . . . . . . . . . 16
class
β |
52 | 51 | cof 7667 |
. . . . . . . . . . . . . . 15
class
βf β |
53 | 43, 48, 52 | co 7408 |
. . . . . . . . . . . . . 14
class (π βf β
π₯) |
54 | 38 | cv 1540 |
. . . . . . . . . . . . . 14
class π |
55 | 53, 54 | cfv 6543 |
. . . . . . . . . . . . 13
class (πβ(π βf β π₯)) |
56 | 19, 35 | cfv 6543 |
. . . . . . . . . . . . 13
class
(.rβπ) |
57 | 50, 55, 56 | co 7408 |
. . . . . . . . . . . 12
class ((πβπ₯)(.rβπ)(πβ(π βf β π₯))) |
58 | 40, 47, 57 | cmpt 5231 |
. . . . . . . . . . 11
class (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))) |
59 | | cgsu 17385 |
. . . . . . . . . . 11
class
Ξ£g |
60 | 19, 58, 59 | co 7408 |
. . . . . . . . . 10
class (π Ξ£g
(π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯))))) |
61 | 39, 22, 60 | cmpt 5231 |
. . . . . . . . 9
class (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))))) |
62 | 37, 38, 26, 26, 61 | cmpo 7410 |
. . . . . . . 8
class (π β π, π β π β¦ (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯))))))) |
63 | 36, 62 | cop 4634 |
. . . . . . 7
class
β¨(.rβndx), (π β π, π β π β¦ (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))))))β© |
64 | 27, 34, 63 | ctp 4632 |
. . . . . 6
class
{β¨(Baseβndx), πβ©, β¨(+gβndx), (
βf (+gβπ) βΎ (π Γ π))β©, β¨(.rβndx),
(π β π, π β π β¦ (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))))))β©} |
65 | | csca 17199 |
. . . . . . . . 9
class
Scalar |
66 | 24, 65 | cfv 6543 |
. . . . . . . 8
class
(Scalarβndx) |
67 | 66, 19 | cop 4634 |
. . . . . . 7
class
β¨(Scalarβndx), πβ© |
68 | | cvsca 17200 |
. . . . . . . . 9
class
Β·π |
69 | 24, 68 | cfv 6543 |
. . . . . . . 8
class (
Β·π βndx) |
70 | 48 | csn 4628 |
. . . . . . . . . . 11
class {π₯} |
71 | 22, 70 | cxp 5674 |
. . . . . . . . . 10
class (π Γ {π₯}) |
72 | 56 | cof 7667 |
. . . . . . . . . 10
class
βf (.rβπ) |
73 | 71, 49, 72 | co 7408 |
. . . . . . . . 9
class ((π Γ {π₯}) βf
(.rβπ)π) |
74 | 40, 37, 21, 26, 73 | cmpo 7410 |
. . . . . . . 8
class (π₯ β (Baseβπ), π β π β¦ ((π Γ {π₯}) βf
(.rβπ)π)) |
75 | 69, 74 | cop 4634 |
. . . . . . 7
class β¨(
Β·π βndx), (π₯ β (Baseβπ), π β π β¦ ((π Γ {π₯}) βf
(.rβπ)π))β© |
76 | | cts 17202 |
. . . . . . . . 9
class
TopSet |
77 | 24, 76 | cfv 6543 |
. . . . . . . 8
class
(TopSetβndx) |
78 | | ctopn 17366 |
. . . . . . . . . . . 12
class
TopOpen |
79 | 19, 78 | cfv 6543 |
. . . . . . . . . . 11
class
(TopOpenβπ) |
80 | 79 | csn 4628 |
. . . . . . . . . 10
class
{(TopOpenβπ)} |
81 | 22, 80 | cxp 5674 |
. . . . . . . . 9
class (π Γ {(TopOpenβπ)}) |
82 | | cpt 17383 |
. . . . . . . . 9
class
βt |
83 | 81, 82 | cfv 6543 |
. . . . . . . 8
class
(βtβ(π Γ {(TopOpenβπ)})) |
84 | 77, 83 | cop 4634 |
. . . . . . 7
class
β¨(TopSetβndx), (βtβ(π Γ {(TopOpenβπ)}))β© |
85 | 67, 75, 84 | ctp 4632 |
. . . . . 6
class
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), (π₯ β (Baseβπ), π β π β¦ ((π Γ {π₯}) βf
(.rβπ)π))β©, β¨(TopSetβndx),
(βtβ(π Γ {(TopOpenβπ)}))β©} |
86 | 64, 85 | cun 3946 |
. . . . 5
class
({β¨(Baseβndx), πβ©, β¨(+gβndx), (
βf (+gβπ) βΎ (π Γ π))β©, β¨(.rβndx),
(π β π, π β π β¦ (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), (π₯ β (Baseβπ), π β π β¦ ((π Γ {π₯}) βf
(.rβπ)π))β©, β¨(TopSetβndx),
(βtβ(π Γ {(TopOpenβπ)}))β©}) |
87 | 18, 23, 86 | csb 3893 |
. . . 4
class
β¦((Baseβπ) βm π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), ( βf
(+gβπ)
βΎ (π Γ π))β©,
β¨(.rβndx), (π β π, π β π β¦ (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), (π₯ β (Baseβπ), π β π β¦ ((π Γ {π₯}) βf
(.rβπ)π))β©, β¨(TopSetβndx),
(βtβ(π Γ {(TopOpenβπ)}))β©}) |
88 | 5, 17, 87 | csb 3893 |
. . 3
class
β¦{β
β (β0 βm π) β£ (β‘β β β) β Fin} / πβ¦β¦((Baseβπ) βm π) / πβ¦({β¨(Baseβndx), πβ©,
β¨(+gβndx), ( βf (+gβπ) βΎ (π Γ π))β©, β¨(.rβndx),
(π β π, π β π β¦ (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β (Baseβπ), π β π β¦ ((π Γ {π₯}) βf
(.rβπ)π))β©, β¨(TopSetβndx),
(βtβ(π
Γ {(TopOpenβπ)}))β©}) |
89 | 2, 3, 4, 4, 88 | cmpo 7410 |
. 2
class (π β V, π β V β¦ β¦{β β (β0
βm π)
β£ (β‘β β β) β Fin} / πβ¦β¦((Baseβπ) βm π) / πβ¦({β¨(Baseβndx), πβ©,
β¨(+gβndx), ( βf (+gβπ) βΎ (π Γ π))β©, β¨(.rβndx),
(π β π, π β π β¦ (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β (Baseβπ), π β π β¦ ((π Γ {π₯}) βf
(.rβπ)π))β©, β¨(TopSetβndx),
(βtβ(π
Γ {(TopOpenβπ)}))β©})) |
90 | 1, 89 | wceq 1541 |
1
wff mPwSer =
(π β V, π β V β¦
β¦{β β
(β0 βm π) β£ (β‘β β β) β Fin} / πβ¦β¦((Baseβπ) βm π) / πβ¦({β¨(Baseβndx), πβ©,
β¨(+gβndx), ( βf (+gβπ) βΎ (π Γ π))β©, β¨(.rβndx),
(π β π, π β π β¦ (π β π β¦ (π Ξ£g (π₯ β {π¦ β π β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ)(πβ(π βf β π₯)))))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β (Baseβπ), π β π β¦ ((π Γ {π₯}) βf
(.rβπ)π))β©, β¨(TopSetβndx),
(βtβ(π
Γ {(TopOpenβπ)}))β©})) |