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 = { 𝑡 ∈ mFS ∣ [ ( mUV ‘ 𝑡 ) / 𝑢 ] [ ( mEx ‘ 𝑡 ) / 𝑥 ] [ ( mVL ‘ 𝑡 ) / 𝑣 ] [ ( mEval ‘ 𝑡 ) / 𝑛 ] [ ( mFresh ‘ 𝑡 ) / 𝑓 ] ( ( 𝑢 ⊆ ( ( mTC ‘ 𝑡 ) × V ) ∧ 𝑓 ∈ ( mFRel ‘ 𝑡 ) ∧ 𝑛 ∈ ( 𝑢 ↑pm ( 𝑣 × ( mEx ‘ 𝑡 ) ) ) ) ∧ ∀ 𝑚 ∈ 𝑣 ( ( ∀ 𝑒 ∈ 𝑥 ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) ⊆ ( 𝑢 “ { ( 1st ‘ 𝑒 ) } ) ∧ ∀ 𝑦 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑦 ) ∧ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ( ( ∀ 𝑦 ∀ 𝑧 ( 𝑦 𝑑 𝑧 → ( 𝑚 ‘ 𝑦 ) 𝑓 ( 𝑚 ‘ 𝑧 ) ) ∧ ℎ ⊆ ( dom 𝑛 “ { 𝑚 } ) ) → 𝑚 dom 𝑛 𝑎 ) ) ) ∧ ( ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ∀ 𝑦 ( ⟨ 𝑠 , 𝑚 ⟩ ( mVSubst ‘ 𝑡 ) 𝑦 → ( 𝑛 “ { ⟨ 𝑚 , ( 𝑠 ‘ 𝑒 ) ⟩ } ) = ( 𝑛 “ { ⟨ 𝑦 , 𝑒 ⟩ } ) ) ∧ ∀ 𝑝 ∈ 𝑣 ∀ 𝑒 ∈ 𝑥 ( ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑒 ) ) = ( 𝑝 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑒 ) ) → ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( 𝑛 “ { ⟨ 𝑝 , 𝑒 ⟩ } ) ) ∧ ∀ 𝑦 ∈ 𝑢 ∀ 𝑒 ∈ 𝑥 ( ( 𝑚 “ ( ( mVars ‘ 𝑡 ) ‘ 𝑒 ) ) ⊆ ( 𝑓 “ { 𝑦 } ) → ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) ⊆ ( 𝑓 “ { 𝑦 } ) ) ) ) ) }

Detailed syntax breakdown

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