Step | Hyp | Ref
| Expression |
1 | | cmdl 34597 |
. 2
class
mMdl |
2 | | vu |
. . . . . . . . . . . 12
setvar π’ |
3 | 2 | cv 1540 |
. . . . . . . . . . 11
class π’ |
4 | | vt |
. . . . . . . . . . . . . 14
setvar π‘ |
5 | 4 | cv 1540 |
. . . . . . . . . . . . 13
class π‘ |
6 | | cmtc 34450 |
. . . . . . . . . . . . 13
class
mTC |
7 | 5, 6 | cfv 6543 |
. . . . . . . . . . . 12
class
(mTCβπ‘) |
8 | | cvv 3474 |
. . . . . . . . . . . 12
class
V |
9 | 7, 8 | cxp 5674 |
. . . . . . . . . . 11
class
((mTCβπ‘)
Γ V) |
10 | 3, 9 | wss 3948 |
. . . . . . . . . 10
wff π’ β ((mTCβπ‘) Γ V) |
11 | | vf |
. . . . . . . . . . . 12
setvar π |
12 | 11 | cv 1540 |
. . . . . . . . . . 11
class π |
13 | | cmfr 34595 |
. . . . . . . . . . . 12
class
mFRel |
14 | 5, 13 | cfv 6543 |
. . . . . . . . . . 11
class
(mFRelβπ‘) |
15 | 12, 14 | wcel 2106 |
. . . . . . . . . 10
wff π β (mFRelβπ‘) |
16 | | vn |
. . . . . . . . . . . 12
setvar π |
17 | 16 | cv 1540 |
. . . . . . . . . . 11
class π |
18 | | vv |
. . . . . . . . . . . . . 14
setvar π£ |
19 | 18 | cv 1540 |
. . . . . . . . . . . . 13
class π£ |
20 | | cmex 34453 |
. . . . . . . . . . . . . 14
class
mEx |
21 | 5, 20 | cfv 6543 |
. . . . . . . . . . . . 13
class
(mExβπ‘) |
22 | 19, 21 | cxp 5674 |
. . . . . . . . . . . 12
class (π£ Γ (mExβπ‘)) |
23 | | cpm 8820 |
. . . . . . . . . . . 12
class
βpm |
24 | 3, 22, 23 | co 7408 |
. . . . . . . . . . 11
class (π’ βpm (π£ Γ (mExβπ‘))) |
25 | 17, 24 | wcel 2106 |
. . . . . . . . . 10
wff π β (π’ βpm (π£ Γ (mExβπ‘))) |
26 | 10, 15, 25 | w3a 1087 |
. . . . . . . . 9
wff (π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) |
27 | | vm |
. . . . . . . . . . . . . . . . . 18
setvar π |
28 | 27 | cv 1540 |
. . . . . . . . . . . . . . . . 17
class π |
29 | | ve |
. . . . . . . . . . . . . . . . . 18
setvar π |
30 | 29 | cv 1540 |
. . . . . . . . . . . . . . . . 17
class π |
31 | 28, 30 | cop 4634 |
. . . . . . . . . . . . . . . 16
class
β¨π, πβ© |
32 | 31 | csn 4628 |
. . . . . . . . . . . . . . 15
class
{β¨π, πβ©} |
33 | 17, 32 | cima 5679 |
. . . . . . . . . . . . . 14
class (π β {β¨π, πβ©}) |
34 | | c1st 7972 |
. . . . . . . . . . . . . . . . 17
class
1st |
35 | 30, 34 | cfv 6543 |
. . . . . . . . . . . . . . . 16
class
(1st βπ) |
36 | 35 | csn 4628 |
. . . . . . . . . . . . . . 15
class
{(1st βπ)} |
37 | 3, 36 | cima 5679 |
. . . . . . . . . . . . . 14
class (π’ β {(1st
βπ)}) |
38 | 33, 37 | wss 3948 |
. . . . . . . . . . . . 13
wff (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) |
39 | | vx |
. . . . . . . . . . . . . 14
setvar π₯ |
40 | 39 | cv 1540 |
. . . . . . . . . . . . 13
class π₯ |
41 | 38, 29, 40 | wral 3061 |
. . . . . . . . . . . 12
wff
βπ β
π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) |
42 | | vy |
. . . . . . . . . . . . . . . . 17
setvar π¦ |
43 | 42 | cv 1540 |
. . . . . . . . . . . . . . . 16
class π¦ |
44 | | cmvh 34458 |
. . . . . . . . . . . . . . . . 17
class
mVH |
45 | 5, 44 | cfv 6543 |
. . . . . . . . . . . . . . . 16
class
(mVHβπ‘) |
46 | 43, 45 | cfv 6543 |
. . . . . . . . . . . . . . 15
class
((mVHβπ‘)βπ¦) |
47 | 28, 46 | cop 4634 |
. . . . . . . . . . . . . 14
class
β¨π,
((mVHβπ‘)βπ¦)β© |
48 | 43, 28 | cfv 6543 |
. . . . . . . . . . . . . 14
class (πβπ¦) |
49 | 47, 48, 17 | wbr 5148 |
. . . . . . . . . . . . 13
wff β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) |
50 | | cmvar 34447 |
. . . . . . . . . . . . . 14
class
mVR |
51 | 5, 50 | cfv 6543 |
. . . . . . . . . . . . 13
class
(mVRβπ‘) |
52 | 49, 42, 51 | wral 3061 |
. . . . . . . . . . . 12
wff
βπ¦ β
(mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) |
53 | | vd |
. . . . . . . . . . . . . . . . . . 19
setvar π |
54 | 53 | cv 1540 |
. . . . . . . . . . . . . . . . . 18
class π |
55 | | vh |
. . . . . . . . . . . . . . . . . . 19
setvar β |
56 | 55 | cv 1540 |
. . . . . . . . . . . . . . . . . 18
class β |
57 | | va |
. . . . . . . . . . . . . . . . . . 19
setvar π |
58 | 57 | cv 1540 |
. . . . . . . . . . . . . . . . . 18
class π |
59 | 54, 56, 58 | cotp 4636 |
. . . . . . . . . . . . . . . . 17
class
β¨π, β, πβ© |
60 | | cmax 34451 |
. . . . . . . . . . . . . . . . . 18
class
mAx |
61 | 5, 60 | cfv 6543 |
. . . . . . . . . . . . . . . . 17
class
(mAxβπ‘) |
62 | 59, 61 | wcel 2106 |
. . . . . . . . . . . . . . . 16
wff β¨π, β, πβ© β (mAxβπ‘) |
63 | | vz |
. . . . . . . . . . . . . . . . . . . . . . 23
setvar π§ |
64 | 63 | cv 1540 |
. . . . . . . . . . . . . . . . . . . . . 22
class π§ |
65 | 43, 64, 54 | wbr 5148 |
. . . . . . . . . . . . . . . . . . . . 21
wff π¦ππ§ |
66 | 64, 28 | cfv 6543 |
. . . . . . . . . . . . . . . . . . . . . 22
class (πβπ§) |
67 | 48, 66, 12 | wbr 5148 |
. . . . . . . . . . . . . . . . . . . . 21
wff (πβπ¦)π(πβπ§) |
68 | 65, 67 | wi 4 |
. . . . . . . . . . . . . . . . . . . 20
wff (π¦ππ§ β (πβπ¦)π(πβπ§)) |
69 | 68, 63 | wal 1539 |
. . . . . . . . . . . . . . . . . . 19
wff
βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) |
70 | 69, 42 | wal 1539 |
. . . . . . . . . . . . . . . . . 18
wff
βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) |
71 | 17 | cdm 5676 |
. . . . . . . . . . . . . . . . . . . 20
class dom π |
72 | 28 | csn 4628 |
. . . . . . . . . . . . . . . . . . . 20
class {π} |
73 | 71, 72 | cima 5679 |
. . . . . . . . . . . . . . . . . . 19
class (dom
π β {π}) |
74 | 56, 73 | wss 3948 |
. . . . . . . . . . . . . . . . . 18
wff β β (dom π β {π}) |
75 | 70, 74 | wa 396 |
. . . . . . . . . . . . . . . . 17
wff
(βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) |
76 | 28, 58, 71 | wbr 5148 |
. . . . . . . . . . . . . . . . 17
wff πdom π π |
77 | 75, 76 | wi 4 |
. . . . . . . . . . . . . . . 16
wff
((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π) |
78 | 62, 77 | wi 4 |
. . . . . . . . . . . . . . 15
wff
(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π)) |
79 | 78, 57 | wal 1539 |
. . . . . . . . . . . . . 14
wff
βπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π)) |
80 | 79, 55 | wal 1539 |
. . . . . . . . . . . . 13
wff
βββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π)) |
81 | 80, 53 | wal 1539 |
. . . . . . . . . . . 12
wff
βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π)) |
82 | 41, 52, 81 | w3a 1087 |
. . . . . . . . . . 11
wff
(βπ β
π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) |
83 | | vs |
. . . . . . . . . . . . . . . . . . 19
setvar π |
84 | 83 | cv 1540 |
. . . . . . . . . . . . . . . . . 18
class π |
85 | 84, 28 | cop 4634 |
. . . . . . . . . . . . . . . . 17
class
β¨π , πβ© |
86 | | cmvsb 34593 |
. . . . . . . . . . . . . . . . . 18
class
mVSubst |
87 | 5, 86 | cfv 6543 |
. . . . . . . . . . . . . . . . 17
class
(mVSubstβπ‘) |
88 | 85, 43, 87 | wbr 5148 |
. . . . . . . . . . . . . . . 16
wff β¨π , πβ©(mVSubstβπ‘)π¦ |
89 | 30, 84 | cfv 6543 |
. . . . . . . . . . . . . . . . . . . 20
class (π βπ) |
90 | 28, 89 | cop 4634 |
. . . . . . . . . . . . . . . . . . 19
class
β¨π, (π βπ)β© |
91 | 90 | csn 4628 |
. . . . . . . . . . . . . . . . . 18
class
{β¨π, (π βπ)β©} |
92 | 17, 91 | cima 5679 |
. . . . . . . . . . . . . . . . 17
class (π β {β¨π, (π βπ)β©}) |
93 | 43, 30 | cop 4634 |
. . . . . . . . . . . . . . . . . . 19
class
β¨π¦, πβ© |
94 | 93 | csn 4628 |
. . . . . . . . . . . . . . . . . 18
class
{β¨π¦, πβ©} |
95 | 17, 94 | cima 5679 |
. . . . . . . . . . . . . . . . 17
class (π β {β¨π¦, πβ©}) |
96 | 92, 95 | wceq 1541 |
. . . . . . . . . . . . . . . 16
wff (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©}) |
97 | 88, 96 | wi 4 |
. . . . . . . . . . . . . . 15
wff
(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) |
98 | 97, 42 | wal 1539 |
. . . . . . . . . . . . . 14
wff
βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) |
99 | 98, 29, 21 | wral 3061 |
. . . . . . . . . . . . 13
wff
βπ β
(mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) |
100 | | cmsub 34457 |
. . . . . . . . . . . . . . 15
class
mSubst |
101 | 5, 100 | cfv 6543 |
. . . . . . . . . . . . . 14
class
(mSubstβπ‘) |
102 | 101 | crn 5677 |
. . . . . . . . . . . . 13
class ran
(mSubstβπ‘) |
103 | 99, 83, 102 | wral 3061 |
. . . . . . . . . . . 12
wff
βπ β ran
(mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) |
104 | | cmvrs 34455 |
. . . . . . . . . . . . . . . . . . 19
class
mVars |
105 | 5, 104 | cfv 6543 |
. . . . . . . . . . . . . . . . . 18
class
(mVarsβπ‘) |
106 | 30, 105 | cfv 6543 |
. . . . . . . . . . . . . . . . 17
class
((mVarsβπ‘)βπ) |
107 | 28, 106 | cres 5678 |
. . . . . . . . . . . . . . . 16
class (π βΎ ((mVarsβπ‘)βπ)) |
108 | | vp |
. . . . . . . . . . . . . . . . . 18
setvar π |
109 | 108 | cv 1540 |
. . . . . . . . . . . . . . . . 17
class π |
110 | 109, 106 | cres 5678 |
. . . . . . . . . . . . . . . 16
class (π βΎ ((mVarsβπ‘)βπ)) |
111 | 107, 110 | wceq 1541 |
. . . . . . . . . . . . . . 15
wff (π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) |
112 | 109, 30 | cop 4634 |
. . . . . . . . . . . . . . . . . 18
class
β¨π, πβ© |
113 | 112 | csn 4628 |
. . . . . . . . . . . . . . . . 17
class
{β¨π, πβ©} |
114 | 17, 113 | cima 5679 |
. . . . . . . . . . . . . . . 16
class (π β {β¨π, πβ©}) |
115 | 33, 114 | wceq 1541 |
. . . . . . . . . . . . . . 15
wff (π β {β¨π, πβ©}) = (π β {β¨π, πβ©}) |
116 | 111, 115 | wi 4 |
. . . . . . . . . . . . . 14
wff ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) |
117 | 116, 29, 40 | wral 3061 |
. . . . . . . . . . . . 13
wff
βπ β
π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) |
118 | 117, 108,
19 | wral 3061 |
. . . . . . . . . . . 12
wff
βπ β
π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) |
119 | 28, 106 | cima 5679 |
. . . . . . . . . . . . . . . 16
class (π β ((mVarsβπ‘)βπ)) |
120 | 43 | csn 4628 |
. . . . . . . . . . . . . . . . 17
class {π¦} |
121 | 12, 120 | cima 5679 |
. . . . . . . . . . . . . . . 16
class (π β {π¦}) |
122 | 119, 121 | wss 3948 |
. . . . . . . . . . . . . . 15
wff (π β ((mVarsβπ‘)βπ)) β (π β {π¦}) |
123 | 33, 121 | wss 3948 |
. . . . . . . . . . . . . . 15
wff (π β {β¨π, πβ©}) β (π β {π¦}) |
124 | 122, 123 | wi 4 |
. . . . . . . . . . . . . 14
wff ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})) |
125 | 124, 29, 40 | wral 3061 |
. . . . . . . . . . . . 13
wff
βπ β
π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})) |
126 | 125, 42, 3 | wral 3061 |
. . . . . . . . . . . 12
wff
βπ¦ β
π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})) |
127 | 103, 118,
126 | w3a 1087 |
. . . . . . . . . . 11
wff
(βπ β
ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦}))) |
128 | 82, 127 | wa 396 |
. . . . . . . . . 10
wff
((βπ β
π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})))) |
129 | 128, 27, 19 | wral 3061 |
. . . . . . . . 9
wff
βπ β
π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})))) |
130 | 26, 129 | wa 396 |
. . . . . . . 8
wff ((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦}))))) |
131 | | cmfsh 34594 |
. . . . . . . . 9
class
mFresh |
132 | 5, 131 | cfv 6543 |
. . . . . . . 8
class
(mFreshβπ‘) |
133 | 130, 11, 132 | wsbc 3777 |
. . . . . . 7
wff
[(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦}))))) |
134 | | cmevl 34596 |
. . . . . . . 8
class
mEval |
135 | 5, 134 | cfv 6543 |
. . . . . . 7
class
(mEvalβπ‘) |
136 | 133, 16, 135 | wsbc 3777 |
. . . . . 6
wff
[(mEvalβπ‘) / π][(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦}))))) |
137 | | cmvl 34592 |
. . . . . . 7
class
mVL |
138 | 5, 137 | cfv 6543 |
. . . . . 6
class
(mVLβπ‘) |
139 | 136, 18, 138 | wsbc 3777 |
. . . . 5
wff
[(mVLβπ‘) / π£][(mEvalβπ‘) / π][(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦}))))) |
140 | 139, 39, 21 | wsbc 3777 |
. . . 4
wff
[(mExβπ‘) / π₯][(mVLβπ‘) / π£][(mEvalβπ‘) / π][(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦}))))) |
141 | | cmuv 34591 |
. . . . 5
class
mUV |
142 | 5, 141 | cfv 6543 |
. . . 4
class
(mUVβπ‘) |
143 | 140, 2, 142 | wsbc 3777 |
. . 3
wff
[(mUVβπ‘) / π’][(mExβπ‘) / π₯][(mVLβπ‘) / π£][(mEvalβπ‘) / π][(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦}))))) |
144 | | cmfs 34462 |
. . 3
class
mFS |
145 | 143, 4, 144 | crab 3432 |
. 2
class {π‘ β mFS β£
[(mUVβπ‘) /
π’][(mExβπ‘) / π₯][(mVLβπ‘) / π£][(mEvalβπ‘) / π][(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})))))} |
146 | 1, 145 | wceq 1541 |
1
wff mMdl =
{π‘ β mFS β£
[(mUVβπ‘) /
π’][(mExβπ‘) / π₯][(mVLβπ‘) / π£][(mEvalβπ‘) / π][(mFreshβπ‘) / π]((π’ β ((mTCβπ‘) Γ V) β§ π β (mFRelβπ‘) β§ π β (π’ βpm (π£ Γ (mExβπ‘)))) β§ βπ β π£ ((βπ β π₯ (π β {β¨π, πβ©}) β (π’ β {(1st βπ)}) β§ βπ¦ β (mVRβπ‘)β¨π, ((mVHβπ‘)βπ¦)β©π(πβπ¦) β§ βπβββπ(β¨π, β, πβ© β (mAxβπ‘) β ((βπ¦βπ§(π¦ππ§ β (πβπ¦)π(πβπ§)) β§ β β (dom π β {π})) β πdom π π))) β§ (βπ β ran (mSubstβπ‘)βπ β (mExβπ‘)βπ¦(β¨π , πβ©(mVSubstβπ‘)π¦ β (π β {β¨π, (π βπ)β©}) = (π β {β¨π¦, πβ©})) β§ βπ β π£ βπ β π₯ ((π βΎ ((mVarsβπ‘)βπ)) = (π βΎ ((mVarsβπ‘)βπ)) β (π β {β¨π, πβ©}) = (π β {β¨π, πβ©})) β§ βπ¦ β π’ βπ β π₯ ((π β ((mVarsβπ‘)βπ)) β (π β {π¦}) β (π β {β¨π, πβ©}) β (π β {π¦})))))} |