Definition df-mdl 30771

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

Assertion

Ref

Expression

df-mdl

⊢ 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‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦})))))}

Distinct variable group:   𝑎,𝑑,𝑒,𝑓,ℎ,𝑚,𝑛,𝑝,𝑠,𝑡,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-mdl

Step	Hyp	Ref	Expression
1		cmdl 30760	. 2 class mMdl
2		vu	. . . . . . . . . . . 12 setvar 𝑢
3	2	cv 1474	. . . . . . . . . . 11 class 𝑢
4		vt	. . . . . . . . . . . . . 14 setvar 𝑡
5	4	cv 1474	. . . . . . . . . . . . 13 class 𝑡
6		cmtc 30615	. . . . . . . . . . . . 13 class mTC
7	5, 6	cfv 5804	. . . . . . . . . . . 12 class (mTC‘𝑡)
8		cvv 3173	. . . . . . . . . . . 12 class V
9	7, 8	cxp 5036	. . . . . . . . . . 11 class ((mTC‘𝑡) × V)
10	3, 9	wss 3540	. . . . . . . . . 10 wff 𝑢 ⊆ ((mTC‘𝑡) × V)
11		vf	. . . . . . . . . . . 12 setvar 𝑓
12	11	cv 1474	. . . . . . . . . . 11 class 𝑓
13		cmfr 30758	. . . . . . . . . . . 12 class mFRel
14	5, 13	cfv 5804	. . . . . . . . . . 11 class (mFRel‘𝑡)
15	12, 14	wcel 1977	. . . . . . . . . 10 wff 𝑓 ∈ (mFRel‘𝑡)
16		vn	. . . . . . . . . . . 12 setvar 𝑛
17	16	cv 1474	. . . . . . . . . . 11 class 𝑛
18		vv	. . . . . . . . . . . . . 14 setvar 𝑣
19	18	cv 1474	. . . . . . . . . . . . 13 class 𝑣
20		cmex 30618	. . . . . . . . . . . . . 14 class mEx
21	5, 20	cfv 5804	. . . . . . . . . . . . 13 class (mEx‘𝑡)
22	19, 21	cxp 5036	. . . . . . . . . . . 12 class (𝑣 × (mEx‘𝑡))
23		cpm 7745	. . . . . . . . . . . 12 class ↑pm
24	3, 22, 23	co 6549	. . . . . . . . . . 11 class (𝑢 ↑pm (𝑣 × (mEx‘𝑡)))
25	17, 24	wcel 1977	. . . . . . . . . 10 wff 𝑛 ∈ (𝑢 ↑pm (𝑣 × (mEx‘𝑡)))
26	10, 15, 25	w3a 1031	. . . . . . . . 9 wff (𝑢 ⊆ ((mTC‘𝑡) × V) ∧ 𝑓 ∈ (mFRel‘𝑡) ∧ 𝑛 ∈ (𝑢 ↑pm (𝑣 × (mEx‘𝑡))))
27		vm	. . . . . . . . . . . . . . . . . 18 setvar 𝑚
28	27	cv 1474	. . . . . . . . . . . . . . . . 17 class 𝑚
29		ve	. . . . . . . . . . . . . . . . . 18 setvar 𝑒
30	29	cv 1474	. . . . . . . . . . . . . . . . 17 class 𝑒
31	28, 30	cop 4131	. . . . . . . . . . . . . . . 16 class ⟨𝑚, 𝑒⟩
32	31	csn 4125	. . . . . . . . . . . . . . 15 class {⟨𝑚, 𝑒⟩}
33	17, 32	cima 5041	. . . . . . . . . . . . . 14 class (𝑛 “ {⟨𝑚, 𝑒⟩})
34		c1st 7057	. . . . . . . . . . . . . . . . 17 class 1st
35	30, 34	cfv 5804	. . . . . . . . . . . . . . . 16 class (1st ‘𝑒)
36	35	csn 4125	. . . . . . . . . . . . . . 15 class {(1st ‘𝑒)}
37	3, 36	cima 5041	. . . . . . . . . . . . . 14 class (𝑢 “ {(1st ‘𝑒)})
38	33, 37	wss 3540	. . . . . . . . . . . . 13 wff (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)})
39		vx	. . . . . . . . . . . . . 14 setvar 𝑥
40	39	cv 1474	. . . . . . . . . . . . 13 class 𝑥
41	38, 29, 40	wral 2896	. . . . . . . . . . . 12 wff ∀𝑒 ∈ 𝑥 (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)})
42		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
43	42	cv 1474	. . . . . . . . . . . . . . . 16 class 𝑦
44		cmvh 30623	. . . . . . . . . . . . . . . . 17 class mVH
45	5, 44	cfv 5804	. . . . . . . . . . . . . . . 16 class (mVH‘𝑡)
46	43, 45	cfv 5804	. . . . . . . . . . . . . . 15 class ((mVH‘𝑡)‘𝑦)
47	28, 46	cop 4131	. . . . . . . . . . . . . 14 class ⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩
48	43, 28	cfv 5804	. . . . . . . . . . . . . 14 class (𝑚‘𝑦)
49	47, 48, 17	wbr 4583	. . . . . . . . . . . . 13 wff ⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦)
50		cmvar 30612	. . . . . . . . . . . . . 14 class mVR
51	5, 50	cfv 5804	. . . . . . . . . . . . 13 class (mVR‘𝑡)
52	49, 42, 51	wral 2896	. . . . . . . . . . . 12 wff ∀𝑦 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦)
53		vd	. . . . . . . . . . . . . . . . . . 19 setvar 𝑑
54	53	cv 1474	. . . . . . . . . . . . . . . . . 18 class 𝑑
55		vh	. . . . . . . . . . . . . . . . . . 19 setvar ℎ
56	55	cv 1474	. . . . . . . . . . . . . . . . . 18 class ℎ
57		va	. . . . . . . . . . . . . . . . . . 19 setvar 𝑎
58	57	cv 1474	. . . . . . . . . . . . . . . . . 18 class 𝑎
59	54, 56, 58	cotp 4133	. . . . . . . . . . . . . . . . 17 class ⟨𝑑, ℎ, 𝑎⟩
60		cmax 30616	. . . . . . . . . . . . . . . . . 18 class mAx
61	5, 60	cfv 5804	. . . . . . . . . . . . . . . . 17 class (mAx‘𝑡)
62	59, 61	wcel 1977	. . . . . . . . . . . . . . . 16 wff ⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡)
63		vz	. . . . . . . . . . . . . . . . . . . . . . 23 setvar 𝑧
64	63	cv 1474	. . . . . . . . . . . . . . . . . . . . . 22 class 𝑧
65	43, 64, 54	wbr 4583	. . . . . . . . . . . . . . . . . . . . 21 wff 𝑦𝑑𝑧
66	64, 28	cfv 5804	. . . . . . . . . . . . . . . . . . . . . 22 class (𝑚‘𝑧)
67	48, 66, 12	wbr 4583	. . . . . . . . . . . . . . . . . . . . 21 wff (𝑚‘𝑦)𝑓(𝑚‘𝑧)
68	65, 67	wi 4	. . . . . . . . . . . . . . . . . . . 20 wff (𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧))
69	68, 63	wal 1473	. . . . . . . . . . . . . . . . . . 19 wff ∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧))
70	69, 42	wal 1473	. . . . . . . . . . . . . . . . . 18 wff ∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧))
71	17	cdm 5038	. . . . . . . . . . . . . . . . . . . 20 class dom 𝑛
72	28	csn 4125	. . . . . . . . . . . . . . . . . . . 20 class {𝑚}
73	71, 72	cima 5041	. . . . . . . . . . . . . . . . . . 19 class (dom 𝑛 “ {𝑚})
74	56, 73	wss 3540	. . . . . . . . . . . . . . . . . 18 wff ℎ ⊆ (dom 𝑛 “ {𝑚})
75	70, 74	wa 383	. . . . . . . . . . . . . . . . 17 wff (∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚}))
76	28, 58, 71	wbr 4583	. . . . . . . . . . . . . . . . 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 1473	. . . . . . . . . . . . . 14 wff ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))
80	79, 55	wal 1473	. . . . . . . . . . . . 13 wff ∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))
81	80, 53	wal 1473	. . . . . . . . . . . 12 wff ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))
82	41, 52, 81	w3a 1031	. . . . . . . . . . 11 wff (∀𝑒 ∈ 𝑥 (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)}) ∧ ∀𝑦 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦) ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎)))
83		vs	. . . . . . . . . . . . . . . . . . 19 setvar 𝑠
84	83	cv 1474	. . . . . . . . . . . . . . . . . 18 class 𝑠
85	84, 28	cop 4131	. . . . . . . . . . . . . . . . 17 class ⟨𝑠, 𝑚⟩
86		cmvsb 30756	. . . . . . . . . . . . . . . . . 18 class mVSubst
87	5, 86	cfv 5804	. . . . . . . . . . . . . . . . 17 class (mVSubst‘𝑡)
88	85, 43, 87	wbr 4583	. . . . . . . . . . . . . . . 16 wff ⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦
89	30, 84	cfv 5804	. . . . . . . . . . . . . . . . . . . 20 class (𝑠‘𝑒)
90	28, 89	cop 4131	. . . . . . . . . . . . . . . . . . 19 class ⟨𝑚, (𝑠‘𝑒)⟩
91	90	csn 4125	. . . . . . . . . . . . . . . . . 18 class {⟨𝑚, (𝑠‘𝑒)⟩}
92	17, 91	cima 5041	. . . . . . . . . . . . . . . . 17 class (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩})
93	43, 30	cop 4131	. . . . . . . . . . . . . . . . . . 19 class ⟨𝑦, 𝑒⟩
94	93	csn 4125	. . . . . . . . . . . . . . . . . 18 class {⟨𝑦, 𝑒⟩}
95	17, 94	cima 5041	. . . . . . . . . . . . . . . . 17 class (𝑛 “ {⟨𝑦, 𝑒⟩})
96	92, 95	wceq 1475	. . . . . . . . . . . . . . . 16 wff (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩})
97	88, 96	wi 4	. . . . . . . . . . . . . . 15 wff (⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩}))
98	97, 42	wal 1473	. . . . . . . . . . . . . 14 wff ∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩}))
99	98, 29, 21	wral 2896	. . . . . . . . . . . . 13 wff ∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩}))
100		cmsub 30622	. . . . . . . . . . . . . . 15 class mSubst
101	5, 100	cfv 5804	. . . . . . . . . . . . . 14 class (mSubst‘𝑡)
102	101	crn 5039	. . . . . . . . . . . . 13 class ran (mSubst‘𝑡)
103	99, 83, 102	wral 2896	. . . . . . . . . . . 12 wff ∀𝑠 ∈ ran (mSubst‘𝑡)∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩}))
104		cmvrs 30620	. . . . . . . . . . . . . . . . . . 19 class mVars
105	5, 104	cfv 5804	. . . . . . . . . . . . . . . . . 18 class (mVars‘𝑡)
106	30, 105	cfv 5804	. . . . . . . . . . . . . . . . 17 class ((mVars‘𝑡)‘𝑒)
107	28, 106	cres 5040	. . . . . . . . . . . . . . . 16 class (𝑚 ↾ ((mVars‘𝑡)‘𝑒))
108		vp	. . . . . . . . . . . . . . . . . 18 setvar 𝑝
109	108	cv 1474	. . . . . . . . . . . . . . . . 17 class 𝑝
110	109, 106	cres 5040	. . . . . . . . . . . . . . . 16 class (𝑝 ↾ ((mVars‘𝑡)‘𝑒))
111	107, 110	wceq 1475	. . . . . . . . . . . . . . 15 wff (𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒))
112	109, 30	cop 4131	. . . . . . . . . . . . . . . . . 18 class ⟨𝑝, 𝑒⟩
113	112	csn 4125	. . . . . . . . . . . . . . . . 17 class {⟨𝑝, 𝑒⟩}
114	17, 113	cima 5041	. . . . . . . . . . . . . . . 16 class (𝑛 “ {⟨𝑝, 𝑒⟩})
115	33, 114	wceq 1475	. . . . . . . . . . . . . . 15 wff (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩})
116	111, 115	wi 4	. . . . . . . . . . . . . 14 wff ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩}))
117	116, 29, 40	wral 2896	. . . . . . . . . . . . 13 wff ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩}))
118	117, 108, 19	wral 2896	. . . . . . . . . . . 12 wff ∀𝑝 ∈ 𝑣 ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩}))
119	28, 106	cima 5041	. . . . . . . . . . . . . . . 16 class (𝑚 “ ((mVars‘𝑡)‘𝑒))
120	43	csn 4125	. . . . . . . . . . . . . . . . 17 class {𝑦}
121	12, 120	cima 5041	. . . . . . . . . . . . . . . 16 class (𝑓 “ {𝑦})
122	119, 121	wss 3540	. . . . . . . . . . . . . . 15 wff (𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦})
123	33, 121	wss 3540	. . . . . . . . . . . . . . 15 wff (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦})
124	122, 123	wi 4	. . . . . . . . . . . . . 14 wff ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦}))
125	124, 29, 40	wral 2896	. . . . . . . . . . . . 13 wff ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦}))
126	125, 42, 3	wral 2896	. . . . . . . . . . . 12 wff ∀𝑦 ∈ 𝑢 ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦}))
127	103, 118, 126	w3a 1031	. . . . . . . . . . 11 wff (∀𝑠 ∈ ran (mSubst‘𝑡)∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩})) ∧ ∀𝑝 ∈ 𝑣 ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩})) ∧ ∀𝑦 ∈ 𝑢 ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦})))
128	82, 127	wa 383	. . . . . . . . . 10 wff ((∀𝑒 ∈ 𝑥 (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)}) ∧ ∀𝑦 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦) ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))) ∧ (∀𝑠 ∈ ran (mSubst‘𝑡)∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩})) ∧ ∀𝑝 ∈ 𝑣 ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩})) ∧ ∀𝑦 ∈ 𝑢 ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦}))))
129	128, 27, 19	wral 2896	. . . . . . . . 9 wff ∀𝑚 ∈ 𝑣 ((∀𝑒 ∈ 𝑥 (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)}) ∧ ∀𝑦 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦) ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))) ∧ (∀𝑠 ∈ ran (mSubst‘𝑡)∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩})) ∧ ∀𝑝 ∈ 𝑣 ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩})) ∧ ∀𝑦 ∈ 𝑢 ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦}))))
130	26, 129	wa 383	. . . . . . . 8 wff ((𝑢 ⊆ ((mTC‘𝑡) × V) ∧ 𝑓 ∈ (mFRel‘𝑡) ∧ 𝑛 ∈ (𝑢 ↑pm (𝑣 × (mEx‘𝑡)))) ∧ ∀𝑚 ∈ 𝑣 ((∀𝑒 ∈ 𝑥 (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)}) ∧ ∀𝑦 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦) ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))) ∧ (∀𝑠 ∈ ran (mSubst‘𝑡)∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩})) ∧ ∀𝑝 ∈ 𝑣 ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩})) ∧ ∀𝑦 ∈ 𝑢 ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦})))))
131		cmfsh 30757	. . . . . . . . 9 class mFresh
132	5, 131	cfv 5804	. . . . . . . 8 class (mFresh‘𝑡)
133	130, 11, 132	wsbc 3402	. . . . . . 7 wff [(mFresh‘𝑡) / 𝑓]((𝑢 ⊆ ((mTC‘𝑡) × V) ∧ 𝑓 ∈ (mFRel‘𝑡) ∧ 𝑛 ∈ (𝑢 ↑pm (𝑣 × (mEx‘𝑡)))) ∧ ∀𝑚 ∈ 𝑣 ((∀𝑒 ∈ 𝑥 (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)}) ∧ ∀𝑦 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦) ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))) ∧ (∀𝑠 ∈ ran (mSubst‘𝑡)∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩})) ∧ ∀𝑝 ∈ 𝑣 ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩})) ∧ ∀𝑦 ∈ 𝑢 ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦})))))
134		cmevl 30759	. . . . . . . 8 class mEval
135	5, 134	cfv 5804	. . . . . . 7 class (mEval‘𝑡)
136	133, 16, 135	wsbc 3402	. . . . . 6 wff [(mEval‘𝑡) / 𝑛][(mFresh‘𝑡) / 𝑓]((𝑢 ⊆ ((mTC‘𝑡) × V) ∧ 𝑓 ∈ (mFRel‘𝑡) ∧ 𝑛 ∈ (𝑢 ↑pm (𝑣 × (mEx‘𝑡)))) ∧ ∀𝑚 ∈ 𝑣 ((∀𝑒 ∈ 𝑥 (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)}) ∧ ∀𝑦 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦) ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))) ∧ (∀𝑠 ∈ ran (mSubst‘𝑡)∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩})) ∧ ∀𝑝 ∈ 𝑣 ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩})) ∧ ∀𝑦 ∈ 𝑢 ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦})))))
137		cmvl 30755	. . . . . . 7 class mVL
138	5, 137	cfv 5804	. . . . . 6 class (mVL‘𝑡)
139	136, 18, 138	wsbc 3402	. . . . 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 3402	. . . 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 30754	. . . . 5 class mUV
142	5, 141	cfv 5804	. . . 4 class (mUV‘𝑡)
143	140, 2, 142	wsbc 3402	. . 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 30627	. . 3 class mFS
145	143, 4, 144	crab 2900	. 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 1475	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‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦})))))}

This definition is referenced by: (None)