Metamath Proof Explorer

Definition df-mdl

Description: Define the set of models of a formal system. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mdl 
|- 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 } ) ) ) ) ) }

Detailed syntax breakdown

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 } ) ) ) ) ) }