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	$$⊢\mathrm{mMdl}=\left\{t\in \mathrm{mFS}|\underset{\dot{}}{[}\mathrm{mUV}\left(t\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEx}\left(t\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mVL}\left(t\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEval}\left(t\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mFresh}\left(t\right)/f\underset{\dot{}}{]}\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmdl	$$class\mathrm{mMdl}$$
1		vt	$$setvart$$
2		cmfs	$$class\mathrm{mFS}$$
3		cmuv	$$class\mathrm{mUV}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class\mathrm{mUV}\left(t\right)$$
6		vu	$$setvaru$$
7		cmex	$$class\mathrm{mEx}$$
8	4 7	cfv	$$class\mathrm{mEx}\left(t\right)$$
9		vx	$$setvarx$$
10		cmvl	$$class\mathrm{mVL}$$
11	4 10	cfv	$$class\mathrm{mVL}\left(t\right)$$
12		vv	$$setvarv$$
13		cmevl	$$class\mathrm{mEval}$$
14	4 13	cfv	$$class\mathrm{mEval}\left(t\right)$$
15		vn	$$setvarn$$
16		cmfsh	$$class\mathrm{mFresh}$$
17	4 16	cfv	$$class\mathrm{mFresh}\left(t\right)$$
18		vf	$$setvarf$$
19	6	cv	$$setvaru$$
20		cmtc	$$class\mathrm{mTC}$$
21	4 20	cfv	$$class\mathrm{mTC}\left(t\right)$$
22		cvv	$$class\mathrm{V}$$
23	21 22	cxp	$$class\left(\mathrm{mTC}\left(t\right)\times \mathrm{V}\right)$$
24	19 23	wss	$$wffu\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}$$
25	18	cv	$$setvarf$$
26		cmfr	$$class\mathrm{mFRel}$$
27	4 26	cfv	$$class\mathrm{mFRel}\left(t\right)$$
28	25 27	wcel	$$wfff\in \mathrm{mFRel}\left(t\right)$$
29	15	cv	$$setvarn$$
30		cpm	$$class{\uparrow }_{𝑝𝑚}$$
31	12	cv	$$setvarv$$
32	31 8	cxp	$$class\left(v\times \mathrm{mEx}\left(t\right)\right)$$
33	19 32 30	co	$$class\left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)$$
34	29 33	wcel	$$wffn\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)$$
35	24 28 34	w3a	$$wff\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)$$
36		vm	$$setvarm$$
37		ve	$$setvare$$
38	9	cv	$$setvarx$$
39	36	cv	$$setvarm$$
40	37	cv	$$setvare$$
41	39 40	cop	$$class⟨m,e⟩$$
42	41	csn	$$class\left\{⟨m,e⟩\right\}$$
43	29 42	cima	$$classn\left[\left\{⟨m,e⟩\right\}\right]$$
44		c1st	$$class{1}^{st}$$
45	40 44	cfv	$$class{1}^{st}\left(e\right)$$
46	45	csn	$$class\left\{1^{st}\left(e\right)\right\}$$
47	19 46	cima	$$classu\left[\left\{1^{st}\left(e\right)\right\}\right]$$
48	43 47	wss	$$wffn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]$$
49	48 37 38	wral	$$wff\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]$$
50		vy	$$setvary$$
51		cmvar	$$class\mathrm{mVR}$$
52	4 51	cfv	$$class\mathrm{mVR}\left(t\right)$$
53		cmvh	$$class\mathrm{mVH}$$
54	4 53	cfv	$$class\mathrm{mVH}\left(t\right)$$
55	50	cv	$$setvary$$
56	55 54	cfv	$$class\mathrm{mVH}\left(t\right)\left(y\right)$$
57	39 56	cop	$$class⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩$$
58	55 39	cfv	$$classm\left(y\right)$$
59	57 58 29	wbr	$$wff⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)$$
60	59 50 52	wral	$$wff\forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)$$
61		vd	$$setvard$$
62		vh	$$setvarh$$
63		va	$$setvara$$
64	61	cv	$$setvard$$
65	62	cv	$$setvarh$$
66	63	cv	$$setvara$$
67	64 65 66	cotp	$$class⟨d,h,a⟩$$
68		cmax	$$class\mathrm{mAx}$$
69	4 68	cfv	$$class\mathrm{mAx}\left(t\right)$$
70	67 69	wcel	$$wff⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)$$
71		vz	$$setvarz$$
72	71	cv	$$setvarz$$
73	55 72 64	wbr	$$wffydz$$
74	72 39	cfv	$$classm\left(z\right)$$
75	58 74 25	wbr	$$wffm\left(y\right)fm\left(z\right)$$
76	73 75	wi	$$wff\left(ydz\to m\left(y\right)fm\left(z\right)\right)$$
77	76 71	wal	$$wff\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)$$
78	77 50	wal	$$wff\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)$$
79	29	cdm	$$class\mathrm{dom}n$$
80	39	csn	$$class\left\{m\right\}$$
81	79 80	cima	$$class\mathrm{dom}n\left[\left\{m\right\}\right]$$
82	65 81	wss	$$wffh\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]$$
83	78 82	wa	$$wff\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)$$
84	39 66 79	wbr	$$wffm\mathrm{dom}na$$
85	83 84	wi	$$wff\left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)$$
86	70 85	wi	$$wff\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)$$
87	86 63	wal	$$wff\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)$$
88	87 62	wal	$$wff\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)$$
89	88 61	wal	$$wff\forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)$$
90	49 60 89	w3a	$$wff\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)$$
91		vs	$$setvars$$
92		cmsub	$$class\mathrm{mSubst}$$
93	4 92	cfv	$$class\mathrm{mSubst}\left(t\right)$$
94	93	crn	$$class\mathrm{ran}\mathrm{mSubst}\left(t\right)$$
95	91	cv	$$setvars$$
96	95 39	cop	$$class⟨s,m⟩$$
97		cmvsb	$$class\mathrm{mVSubst}$$
98	4 97	cfv	$$class\mathrm{mVSubst}\left(t\right)$$
99	96 55 98	wbr	$$wff⟨s,m⟩\mathrm{mVSubst}\left(t\right)y$$
100	40 95	cfv	$$classs\left(e\right)$$
101	39 100	cop	$$class⟨m,s\left(e\right)⟩$$
102	101	csn	$$class\left\{⟨m,s\left(e\right)⟩\right\}$$
103	29 102	cima	$$classn\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]$$
104	55 40	cop	$$class⟨y,e⟩$$
105	104	csn	$$class\left\{⟨y,e⟩\right\}$$
106	29 105	cima	$$classn\left[\left\{⟨y,e⟩\right\}\right]$$
107	103 106	wceq	$$wffn\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]$$
108	99 107	wi	$$wff\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)$$
109	108 50	wal	$$wff\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)$$
110	109 37 8	wral	$$wff\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)$$
111	110 91 94	wral	$$wff\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)$$
112		vp	$$setvarp$$
113		cmvrs	$$class\mathrm{mVars}$$
114	4 113	cfv	$$class\mathrm{mVars}\left(t\right)$$
115	40 114	cfv	$$class\mathrm{mVars}\left(t\right)\left(e\right)$$
116	39 115	cres	$$class\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\right)$$
117	112	cv	$$setvarp$$
118	117 115	cres	$$class\left({p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\right)$$
119	116 118	wceq	$$wff{m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}$$
120	117 40	cop	$$class⟨p,e⟩$$
121	120	csn	$$class\left\{⟨p,e⟩\right\}$$
122	29 121	cima	$$classn\left[\left\{⟨p,e⟩\right\}\right]$$
123	43 122	wceq	$$wffn\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]$$
124	119 123	wi	$$wff\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)$$
125	124 37 38	wral	$$wff\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)$$
126	125 112 31	wral	$$wff\forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)$$
127	39 115	cima	$$classm\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]$$
128	55	csn	$$class\left\{y\right\}$$
129	25 128	cima	$$classf\left[\left\{y\right\}\right]$$
130	127 129	wss	$$wffm\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]$$
131	43 129	wss	$$wffn\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]$$
132	130 131	wi	$$wff\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)$$
133	132 37 38	wral	$$wff\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)$$
134	133 50 19	wral	$$wff\forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)$$
135	111 126 134	w3a	$$wff\left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)$$
136	90 135	wa	$$wff\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)$$
137	136 36 31	wral	$$wff\forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)$$
138	35 137	wa	$$wff\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)$$
139	138 18 17	wsbc	$$wff\underset{\dot{}}{[}\mathrm{mFresh}\left(t\right)/f\underset{\dot{}}{]}\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)$$
140	139 15 14	wsbc	$$wff\underset{\dot{}}{[}\mathrm{mEval}\left(t\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mFresh}\left(t\right)/f\underset{\dot{}}{]}\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)$$
141	140 12 11	wsbc	$$wff\underset{\dot{}}{[}\mathrm{mVL}\left(t\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEval}\left(t\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mFresh}\left(t\right)/f\underset{\dot{}}{]}\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)$$
142	141 9 8	wsbc	$$wff\underset{\dot{}}{[}\mathrm{mEx}\left(t\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mVL}\left(t\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEval}\left(t\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mFresh}\left(t\right)/f\underset{\dot{}}{]}\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)$$
143	142 6 5	wsbc	$$wff\underset{\dot{}}{[}\mathrm{mUV}\left(t\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEx}\left(t\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mVL}\left(t\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEval}\left(t\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mFresh}\left(t\right)/f\underset{\dot{}}{]}\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)$$
144	143 1 2	crab	$$class\left\{t\in \mathrm{mFS}|\underset{\dot{}}{[}\mathrm{mUV}\left(t\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEx}\left(t\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mVL}\left(t\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEval}\left(t\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mFresh}\left(t\right)/f\underset{\dot{}}{]}\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)\right\}$$
145	0 144	wceq	$$wff\mathrm{mMdl}=\left\{t\in \mathrm{mFS}|\underset{\dot{}}{[}\mathrm{mUV}\left(t\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEx}\left(t\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mVL}\left(t\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mEval}\left(t\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{mFresh}\left(t\right)/f\underset{\dot{}}{]}\left(\left(u\subseteq \mathrm{mTC}\left(t\right)\times \mathrm{V}\wedge f\in \mathrm{mFRel}\left(t\right)\wedge n\in \left(u{\uparrow }_{𝑝𝑚}\left(v\times \mathrm{mEx}\left(t\right)\right)\right)\right)\wedge \forall m\in v\left(\left(\forall e\in xn\left[\left\{⟨m,e⟩\right\}\right]\subseteq u\left[\left\{1^{st}\left(e\right)\right\}\right]\wedge \forall y\in \mathrm{mVR}\left(t\right)⟨m,\mathrm{mVH}\left(t\right)\left(y\right)⟩nm\left(y\right)\wedge \forall d\forall h\forall a\left(⟨d,h,a⟩\in \mathrm{mAx}\left(t\right)\to \left(\left(\forall y\forall z\left(ydz\to m\left(y\right)fm\left(z\right)\right)\wedge h\subseteq \mathrm{dom}n\left[\left\{m\right\}\right]\right)\to m\mathrm{dom}na\right)\right)\right)\wedge \left(\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\forall e\in \mathrm{mEx}\left(t\right)\forall y\left(⟨s,m⟩\mathrm{mVSubst}\left(t\right)y\to n\left[\left\{⟨m,s\left(e\right)⟩\right\}\right]=n\left[\left\{⟨y,e⟩\right\}\right]\right)\wedge \forall p\in v\forall e\in x\left({m\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}={p\upharpoonright }_{\mathrm{mVars}\left(t\right)\left(e\right)}\to n\left[\left\{⟨m,e⟩\right\}\right]=n\left[\left\{⟨p,e⟩\right\}\right]\right)\wedge \forall y\in u\forall e\in x\left(m\left[\mathrm{mVars}\left(t\right)\left(e\right)\right]\subseteq f\left[\left\{y\right\}\right]\to n\left[\left\{⟨m,e⟩\right\}\right]\subseteq f\left[\left\{y\right\}\right]\right)\right)\right)\right)\right\}$$