Step |
Hyp |
Ref |
Expression |
0 |
|
cmdl |
|- mMdl |
1 |
|
vt |
|- t |
2 |
|
cmfs |
|- mFS |
3 |
|
cmuv |
|- mUV |
4 |
1
|
cv |
|- t |
5 |
4 3
|
cfv |
|- ( mUV ` t ) |
6 |
|
vu |
|- u |
7 |
|
cmex |
|- mEx |
8 |
4 7
|
cfv |
|- ( mEx ` t ) |
9 |
|
vx |
|- x |
10 |
|
cmvl |
|- mVL |
11 |
4 10
|
cfv |
|- ( mVL ` t ) |
12 |
|
vv |
|- v |
13 |
|
cmevl |
|- mEval |
14 |
4 13
|
cfv |
|- ( mEval ` t ) |
15 |
|
vn |
|- n |
16 |
|
cmfsh |
|- mFresh |
17 |
4 16
|
cfv |
|- ( mFresh ` t ) |
18 |
|
vf |
|- f |
19 |
6
|
cv |
|- u |
20 |
|
cmtc |
|- mTC |
21 |
4 20
|
cfv |
|- ( mTC ` t ) |
22 |
|
cvv |
|- _V |
23 |
21 22
|
cxp |
|- ( ( mTC ` t ) X. _V ) |
24 |
19 23
|
wss |
|- u C_ ( ( mTC ` t ) X. _V ) |
25 |
18
|
cv |
|- f |
26 |
|
cmfr |
|- mFRel |
27 |
4 26
|
cfv |
|- ( mFRel ` t ) |
28 |
25 27
|
wcel |
|- f e. ( mFRel ` t ) |
29 |
15
|
cv |
|- n |
30 |
|
cpm |
|- ^pm |
31 |
12
|
cv |
|- v |
32 |
31 8
|
cxp |
|- ( v X. ( mEx ` t ) ) |
33 |
19 32 30
|
co |
|- ( u ^pm ( v X. ( mEx ` t ) ) ) |
34 |
29 33
|
wcel |
|- n e. ( u ^pm ( v X. ( mEx ` t ) ) ) |
35 |
24 28 34
|
w3a |
|- ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) |
36 |
|
vm |
|- m |
37 |
|
ve |
|- e |
38 |
9
|
cv |
|- x |
39 |
36
|
cv |
|- m |
40 |
37
|
cv |
|- e |
41 |
39 40
|
cop |
|- <. m , e >. |
42 |
41
|
csn |
|- { <. m , e >. } |
43 |
29 42
|
cima |
|- ( n " { <. m , e >. } ) |
44 |
|
c1st |
|- 1st |
45 |
40 44
|
cfv |
|- ( 1st ` e ) |
46 |
45
|
csn |
|- { ( 1st ` e ) } |
47 |
19 46
|
cima |
|- ( u " { ( 1st ` e ) } ) |
48 |
43 47
|
wss |
|- ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) |
49 |
48 37 38
|
wral |
|- A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) |
50 |
|
vy |
|- y |
51 |
|
cmvar |
|- mVR |
52 |
4 51
|
cfv |
|- ( mVR ` t ) |
53 |
|
cmvh |
|- mVH |
54 |
4 53
|
cfv |
|- ( mVH ` t ) |
55 |
50
|
cv |
|- y |
56 |
55 54
|
cfv |
|- ( ( mVH ` t ) ` y ) |
57 |
39 56
|
cop |
|- <. m , ( ( mVH ` t ) ` y ) >. |
58 |
55 39
|
cfv |
|- ( m ` y ) |
59 |
57 58 29
|
wbr |
|- <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) |
60 |
59 50 52
|
wral |
|- A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) |
61 |
|
vd |
|- d |
62 |
|
vh |
|- h |
63 |
|
va |
|- a |
64 |
61
|
cv |
|- d |
65 |
62
|
cv |
|- h |
66 |
63
|
cv |
|- a |
67 |
64 65 66
|
cotp |
|- <. d , h , a >. |
68 |
|
cmax |
|- mAx |
69 |
4 68
|
cfv |
|- ( mAx ` t ) |
70 |
67 69
|
wcel |
|- <. d , h , a >. e. ( mAx ` t ) |
71 |
|
vz |
|- z |
72 |
71
|
cv |
|- z |
73 |
55 72 64
|
wbr |
|- y d z |
74 |
72 39
|
cfv |
|- ( m ` z ) |
75 |
58 74 25
|
wbr |
|- ( m ` y ) f ( m ` z ) |
76 |
73 75
|
wi |
|- ( y d z -> ( m ` y ) f ( m ` z ) ) |
77 |
76 71
|
wal |
|- A. z ( y d z -> ( m ` y ) f ( m ` z ) ) |
78 |
77 50
|
wal |
|- A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) |
79 |
29
|
cdm |
|- dom n |
80 |
39
|
csn |
|- { m } |
81 |
79 80
|
cima |
|- ( dom n " { m } ) |
82 |
65 81
|
wss |
|- h C_ ( dom n " { m } ) |
83 |
78 82
|
wa |
|- ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) |
84 |
39 66 79
|
wbr |
|- m dom n a |
85 |
83 84
|
wi |
|- ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) |
86 |
70 85
|
wi |
|- ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) |
87 |
86 63
|
wal |
|- A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) |
88 |
87 62
|
wal |
|- A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) |
89 |
88 61
|
wal |
|- A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) |
90 |
49 60 89
|
w3a |
|- ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) |
91 |
|
vs |
|- s |
92 |
|
cmsub |
|- mSubst |
93 |
4 92
|
cfv |
|- ( mSubst ` t ) |
94 |
93
|
crn |
|- ran ( mSubst ` t ) |
95 |
91
|
cv |
|- s |
96 |
95 39
|
cop |
|- <. s , m >. |
97 |
|
cmvsb |
|- mVSubst |
98 |
4 97
|
cfv |
|- ( mVSubst ` t ) |
99 |
96 55 98
|
wbr |
|- <. s , m >. ( mVSubst ` t ) y |
100 |
40 95
|
cfv |
|- ( s ` e ) |
101 |
39 100
|
cop |
|- <. m , ( s ` e ) >. |
102 |
101
|
csn |
|- { <. m , ( s ` e ) >. } |
103 |
29 102
|
cima |
|- ( n " { <. m , ( s ` e ) >. } ) |
104 |
55 40
|
cop |
|- <. y , e >. |
105 |
104
|
csn |
|- { <. y , e >. } |
106 |
29 105
|
cima |
|- ( n " { <. y , e >. } ) |
107 |
103 106
|
wceq |
|- ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) |
108 |
99 107
|
wi |
|- ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) |
109 |
108 50
|
wal |
|- A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) |
110 |
109 37 8
|
wral |
|- A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) |
111 |
110 91 94
|
wral |
|- A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) |
112 |
|
vp |
|- p |
113 |
|
cmvrs |
|- mVars |
114 |
4 113
|
cfv |
|- ( mVars ` t ) |
115 |
40 114
|
cfv |
|- ( ( mVars ` t ) ` e ) |
116 |
39 115
|
cres |
|- ( m |` ( ( mVars ` t ) ` e ) ) |
117 |
112
|
cv |
|- p |
118 |
117 115
|
cres |
|- ( p |` ( ( mVars ` t ) ` e ) ) |
119 |
116 118
|
wceq |
|- ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) |
120 |
117 40
|
cop |
|- <. p , e >. |
121 |
120
|
csn |
|- { <. p , e >. } |
122 |
29 121
|
cima |
|- ( n " { <. p , e >. } ) |
123 |
43 122
|
wceq |
|- ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) |
124 |
119 123
|
wi |
|- ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) |
125 |
124 37 38
|
wral |
|- A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) |
126 |
125 112 31
|
wral |
|- A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) |
127 |
39 115
|
cima |
|- ( m " ( ( mVars ` t ) ` e ) ) |
128 |
55
|
csn |
|- { y } |
129 |
25 128
|
cima |
|- ( f " { y } ) |
130 |
127 129
|
wss |
|- ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) |
131 |
43 129
|
wss |
|- ( n " { <. m , e >. } ) C_ ( f " { y } ) |
132 |
130 131
|
wi |
|- ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) |
133 |
132 37 38
|
wral |
|- A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) |
134 |
133 50 19
|
wral |
|- A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) |
135 |
111 126 134
|
w3a |
|- ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) |
136 |
90 135
|
wa |
|- ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) |
137 |
136 36 31
|
wral |
|- A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) |
138 |
35 137
|
wa |
|- ( ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) |
139 |
138 18 17
|
wsbc |
|- [. ( mFresh ` t ) / f ]. ( ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) |
140 |
139 15 14
|
wsbc |
|- [. ( mEval ` t ) / n ]. [. ( mFresh ` t ) / f ]. ( ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) |
141 |
140 12 11
|
wsbc |
|- [. ( mVL ` t ) / v ]. [. ( mEval ` t ) / n ]. [. ( mFresh ` t ) / f ]. ( ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) |
142 |
141 9 8
|
wsbc |
|- [. ( mEx ` t ) / x ]. [. ( mVL ` t ) / v ]. [. ( mEval ` t ) / n ]. [. ( mFresh ` t ) / f ]. ( ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) |
143 |
142 6 5
|
wsbc |
|- [. ( mUV ` t ) / u ]. [. ( mEx ` t ) / x ]. [. ( mVL ` t ) / v ]. [. ( mEval ` t ) / n ]. [. ( mFresh ` t ) / f ]. ( ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) |
144 |
143 1 2
|
crab |
|- { t e. mFS | [. ( mUV ` t ) / u ]. [. ( mEx ` t ) / x ]. [. ( mVL ` t ) / v ]. [. ( mEval ` t ) / n ]. [. ( mFresh ` t ) / f ]. ( ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) } |
145 |
0 144
|
wceq |
|- mMdl = { t e. mFS | [. ( mUV ` t ) / u ]. [. ( mEx ` t ) / x ]. [. ( mVL ` t ) / v ]. [. ( mEval ` t ) / n ]. [. ( mFresh ` t ) / f ]. ( ( u C_ ( ( mTC ` t ) X. _V ) /\ f e. ( mFRel ` t ) /\ n e. ( u ^pm ( v X. ( mEx ` t ) ) ) ) /\ A. m e. v ( ( A. e e. x ( n " { <. m , e >. } ) C_ ( u " { ( 1st ` e ) } ) /\ A. y e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` y ) >. n ( m ` y ) /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> ( ( A. y A. z ( y d z -> ( m ` y ) f ( m ` z ) ) /\ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\ ( A. s e. ran ( mSubst ` t ) A. e e. ( mEx ` t ) A. y ( <. s , m >. ( mVSubst ` t ) y -> ( n " { <. m , ( s ` e ) >. } ) = ( n " { <. y , e >. } ) ) /\ A. p e. v A. e e. x ( ( m |` ( ( mVars ` t ) ` e ) ) = ( p |` ( ( mVars ` t ) ` e ) ) -> ( n " { <. m , e >. } ) = ( n " { <. p , e >. } ) ) /\ A. y e. u A. e e. x ( ( m " ( ( mVars ` t ) ` e ) ) C_ ( f " { y } ) -> ( n " { <. m , e >. } ) C_ ( f " { y } ) ) ) ) ) } |