Step | Hyp | Ref
| Expression |
1 | | cmsr 34132 |
. 2
class
mStRed |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vs |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . 5
class π‘ |
6 | | cmpst 34131 |
. . . . 5
class
mPreSt |
7 | 5, 6 | cfv 6500 |
. . . 4
class
(mPreStβπ‘) |
8 | | vh |
. . . . 5
setvar β |
9 | 4 | cv 1541 |
. . . . . . 7
class π |
10 | | c1st 7923 |
. . . . . . 7
class
1st |
11 | 9, 10 | cfv 6500 |
. . . . . 6
class
(1st βπ ) |
12 | | c2nd 7924 |
. . . . . 6
class
2nd |
13 | 11, 12 | cfv 6500 |
. . . . 5
class
(2nd β(1st βπ )) |
14 | | va |
. . . . . 6
setvar π |
15 | 9, 12 | cfv 6500 |
. . . . . 6
class
(2nd βπ ) |
16 | 11, 10 | cfv 6500 |
. . . . . . . 8
class
(1st β(1st βπ )) |
17 | | vz |
. . . . . . . . 9
setvar π§ |
18 | | cmvrs 34127 |
. . . . . . . . . . . 12
class
mVars |
19 | 5, 18 | cfv 6500 |
. . . . . . . . . . 11
class
(mVarsβπ‘) |
20 | 8 | cv 1541 |
. . . . . . . . . . . 12
class β |
21 | 14 | cv 1541 |
. . . . . . . . . . . . 13
class π |
22 | 21 | csn 4590 |
. . . . . . . . . . . 12
class {π} |
23 | 20, 22 | cun 3912 |
. . . . . . . . . . 11
class (β βͺ {π}) |
24 | 19, 23 | cima 5640 |
. . . . . . . . . 10
class
((mVarsβπ‘)
β (β βͺ {π})) |
25 | 24 | cuni 4869 |
. . . . . . . . 9
class βͺ ((mVarsβπ‘) β (β βͺ {π})) |
26 | 17 | cv 1541 |
. . . . . . . . . 10
class π§ |
27 | 26, 26 | cxp 5635 |
. . . . . . . . 9
class (π§ Γ π§) |
28 | 17, 25, 27 | csb 3859 |
. . . . . . . 8
class
β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§) |
29 | 16, 28 | cin 3913 |
. . . . . . 7
class
((1st β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)) |
30 | 29, 20, 21 | cotp 4598 |
. . . . . 6
class
β¨((1st β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© |
31 | 14, 15, 30 | csb 3859 |
. . . . 5
class
β¦(2nd βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© |
32 | 8, 13, 31 | csb 3859 |
. . . 4
class
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© |
33 | 4, 7, 32 | cmpt 5192 |
. . 3
class (π β (mPreStβπ‘) β¦
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |
34 | 2, 3, 33 | cmpt 5192 |
. 2
class (π‘ β V β¦ (π β (mPreStβπ‘) β¦
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) |
35 | 1, 34 | wceq 1542 |
1
wff mStRed =
(π‘ β V β¦ (π β (mPreStβπ‘) β¦
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ ((mVarsβπ‘) β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) |