Definition df-mdl 31517

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

Assertion

Ref

Expression

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

Distinct variable group:   a, d, e, f, h, m, n, p, s, t, u, v, x, y, z

Detailed syntax breakdown of Definition df-mdl

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

This definition is referenced by: (None)