Step | Hyp | Ref
| Expression |
1 | | cmcls 34135 |
. 2
class
mCls |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vd |
. . . 4
setvar π |
5 | | vh |
. . . 4
setvar β |
6 | 2 | cv 1541 |
. . . . . 6
class π‘ |
7 | | cmdv 34126 |
. . . . . 6
class
mDV |
8 | 6, 7 | cfv 6500 |
. . . . 5
class
(mDVβπ‘) |
9 | 8 | cpw 4564 |
. . . 4
class π«
(mDVβπ‘) |
10 | | cmex 34125 |
. . . . . 6
class
mEx |
11 | 6, 10 | cfv 6500 |
. . . . 5
class
(mExβπ‘) |
12 | 11 | cpw 4564 |
. . . 4
class π«
(mExβπ‘) |
13 | 5 | cv 1541 |
. . . . . . . . 9
class β |
14 | | cmvh 34130 |
. . . . . . . . . . 11
class
mVH |
15 | 6, 14 | cfv 6500 |
. . . . . . . . . 10
class
(mVHβπ‘) |
16 | 15 | crn 5638 |
. . . . . . . . 9
class ran
(mVHβπ‘) |
17 | 13, 16 | cun 3912 |
. . . . . . . 8
class (β βͺ ran (mVHβπ‘)) |
18 | | vc |
. . . . . . . . 9
setvar π |
19 | 18 | cv 1541 |
. . . . . . . 8
class π |
20 | 17, 19 | wss 3914 |
. . . . . . 7
wff (β βͺ ran (mVHβπ‘)) β π |
21 | | vm |
. . . . . . . . . . . . . 14
setvar π |
22 | 21 | cv 1541 |
. . . . . . . . . . . . 13
class π |
23 | | vo |
. . . . . . . . . . . . . 14
setvar π |
24 | 23 | cv 1541 |
. . . . . . . . . . . . 13
class π |
25 | | vp |
. . . . . . . . . . . . . 14
setvar π |
26 | 25 | cv 1541 |
. . . . . . . . . . . . 13
class π |
27 | 22, 24, 26 | cotp 4598 |
. . . . . . . . . . . 12
class
β¨π, π, πβ© |
28 | | cmax 34123 |
. . . . . . . . . . . . 13
class
mAx |
29 | 6, 28 | cfv 6500 |
. . . . . . . . . . . 12
class
(mAxβπ‘) |
30 | 27, 29 | wcel 2107 |
. . . . . . . . . . 11
wff β¨π, π, πβ© β (mAxβπ‘) |
31 | | vs |
. . . . . . . . . . . . . . . . 17
setvar π |
32 | 31 | cv 1541 |
. . . . . . . . . . . . . . . 16
class π |
33 | 24, 16 | cun 3912 |
. . . . . . . . . . . . . . . 16
class (π βͺ ran (mVHβπ‘)) |
34 | 32, 33 | cima 5640 |
. . . . . . . . . . . . . . 15
class (π β (π βͺ ran (mVHβπ‘))) |
35 | 34, 19 | wss 3914 |
. . . . . . . . . . . . . 14
wff (π β (π βͺ ran (mVHβπ‘))) β π |
36 | | vx |
. . . . . . . . . . . . . . . . . . 19
setvar π₯ |
37 | 36 | cv 1541 |
. . . . . . . . . . . . . . . . . 18
class π₯ |
38 | | vy |
. . . . . . . . . . . . . . . . . . 19
setvar π¦ |
39 | 38 | cv 1541 |
. . . . . . . . . . . . . . . . . 18
class π¦ |
40 | 37, 39, 22 | wbr 5109 |
. . . . . . . . . . . . . . . . 17
wff π₯ππ¦ |
41 | 37, 15 | cfv 6500 |
. . . . . . . . . . . . . . . . . . . . 21
class
((mVHβπ‘)βπ₯) |
42 | 41, 32 | cfv 6500 |
. . . . . . . . . . . . . . . . . . . 20
class (π β((mVHβπ‘)βπ₯)) |
43 | | cmvrs 34127 |
. . . . . . . . . . . . . . . . . . . . 21
class
mVars |
44 | 6, 43 | cfv 6500 |
. . . . . . . . . . . . . . . . . . . 20
class
(mVarsβπ‘) |
45 | 42, 44 | cfv 6500 |
. . . . . . . . . . . . . . . . . . 19
class
((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) |
46 | 39, 15 | cfv 6500 |
. . . . . . . . . . . . . . . . . . . . 21
class
((mVHβπ‘)βπ¦) |
47 | 46, 32 | cfv 6500 |
. . . . . . . . . . . . . . . . . . . 20
class (π β((mVHβπ‘)βπ¦)) |
48 | 47, 44 | cfv 6500 |
. . . . . . . . . . . . . . . . . . 19
class
((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦))) |
49 | 45, 48 | cxp 5635 |
. . . . . . . . . . . . . . . . . 18
class
(((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) |
50 | 4 | cv 1541 |
. . . . . . . . . . . . . . . . . 18
class π |
51 | 49, 50 | wss 3914 |
. . . . . . . . . . . . . . . . 17
wff
(((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π |
52 | 40, 51 | wi 4 |
. . . . . . . . . . . . . . . 16
wff (π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π) |
53 | 52, 38 | wal 1540 |
. . . . . . . . . . . . . . 15
wff
βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π) |
54 | 53, 36 | wal 1540 |
. . . . . . . . . . . . . 14
wff
βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π) |
55 | 35, 54 | wa 397 |
. . . . . . . . . . . . 13
wff ((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) |
56 | 26, 32 | cfv 6500 |
. . . . . . . . . . . . . 14
class (π βπ) |
57 | 56, 19 | wcel 2107 |
. . . . . . . . . . . . 13
wff (π βπ) β π |
58 | 55, 57 | wi 4 |
. . . . . . . . . . . 12
wff (((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π) |
59 | | cmsub 34129 |
. . . . . . . . . . . . . 14
class
mSubst |
60 | 6, 59 | cfv 6500 |
. . . . . . . . . . . . 13
class
(mSubstβπ‘) |
61 | 60 | crn 5638 |
. . . . . . . . . . . 12
class ran
(mSubstβπ‘) |
62 | 58, 31, 61 | wral 3061 |
. . . . . . . . . . 11
wff
βπ β ran
(mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π) |
63 | 30, 62 | wi 4 |
. . . . . . . . . 10
wff
(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)) |
64 | 63, 25 | wal 1540 |
. . . . . . . . 9
wff
βπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)) |
65 | 64, 23 | wal 1540 |
. . . . . . . 8
wff
βπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)) |
66 | 65, 21 | wal 1540 |
. . . . . . 7
wff
βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)) |
67 | 20, 66 | wa 397 |
. . . . . 6
wff ((β βͺ ran (mVHβπ‘)) β π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π))) |
68 | 67, 18 | cab 2710 |
. . . . 5
class {π β£ ((β βͺ ran (mVHβπ‘)) β π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))} |
69 | 68 | cint 4911 |
. . . 4
class β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))} |
70 | 4, 5, 9, 12, 69 | cmpo 7363 |
. . 3
class (π β π«
(mDVβπ‘), β β π«
(mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))}) |
71 | 2, 3, 70 | cmpt 5192 |
. 2
class (π‘ β V β¦ (π β π«
(mDVβπ‘), β β π«
(mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))})) |
72 | 1, 71 | wceq 1542 |
1
wff mCls =
(π‘ β V β¦ (π β π«
(mDVβπ‘), β β π«
(mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))})) |