Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mdl Structured version   Visualization version   GIF version

Definition df-mdl 34608
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
StepHypRef Expression
1 cmdl 34597 . 2 class mMdl
2 vu . . . . . . . . . . . 12 setvar 𝑒
32cv 1540 . . . . . . . . . . 11 class 𝑒
4 vt . . . . . . . . . . . . . 14 setvar 𝑑
54cv 1540 . . . . . . . . . . . . 13 class 𝑑
6 cmtc 34450 . . . . . . . . . . . . 13 class mTC
75, 6cfv 6543 . . . . . . . . . . . 12 class (mTCβ€˜π‘‘)
8 cvv 3474 . . . . . . . . . . . 12 class V
97, 8cxp 5674 . . . . . . . . . . 11 class ((mTCβ€˜π‘‘) Γ— V)
103, 9wss 3948 . . . . . . . . . 10 wff 𝑒 βŠ† ((mTCβ€˜π‘‘) Γ— V)
11 vf . . . . . . . . . . . 12 setvar 𝑓
1211cv 1540 . . . . . . . . . . 11 class 𝑓
13 cmfr 34595 . . . . . . . . . . . 12 class mFRel
145, 13cfv 6543 . . . . . . . . . . 11 class (mFRelβ€˜π‘‘)
1512, 14wcel 2106 . . . . . . . . . 10 wff 𝑓 ∈ (mFRelβ€˜π‘‘)
16 vn . . . . . . . . . . . 12 setvar 𝑛
1716cv 1540 . . . . . . . . . . 11 class 𝑛
18 vv . . . . . . . . . . . . . 14 setvar 𝑣
1918cv 1540 . . . . . . . . . . . . 13 class 𝑣
20 cmex 34453 . . . . . . . . . . . . . 14 class mEx
215, 20cfv 6543 . . . . . . . . . . . . 13 class (mExβ€˜π‘‘)
2219, 21cxp 5674 . . . . . . . . . . . 12 class (𝑣 Γ— (mExβ€˜π‘‘))
23 cpm 8820 . . . . . . . . . . . 12 class ↑pm
243, 22, 23co 7408 . . . . . . . . . . 11 class (𝑒 ↑pm (𝑣 Γ— (mExβ€˜π‘‘)))
2517, 24wcel 2106 . . . . . . . . . 10 wff 𝑛 ∈ (𝑒 ↑pm (𝑣 Γ— (mExβ€˜π‘‘)))
2610, 15, 25w3a 1087 . . . . . . . . 9 wff (𝑒 βŠ† ((mTCβ€˜π‘‘) Γ— V) ∧ 𝑓 ∈ (mFRelβ€˜π‘‘) ∧ 𝑛 ∈ (𝑒 ↑pm (𝑣 Γ— (mExβ€˜π‘‘))))
27 vm . . . . . . . . . . . . . . . . . 18 setvar π‘š
2827cv 1540 . . . . . . . . . . . . . . . . 17 class π‘š
29 ve . . . . . . . . . . . . . . . . . 18 setvar 𝑒
3029cv 1540 . . . . . . . . . . . . . . . . 17 class 𝑒
3128, 30cop 4634 . . . . . . . . . . . . . . . 16 class βŸ¨π‘š, π‘’βŸ©
3231csn 4628 . . . . . . . . . . . . . . 15 class {βŸ¨π‘š, π‘’βŸ©}
3317, 32cima 5679 . . . . . . . . . . . . . 14 class (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©})
34 c1st 7972 . . . . . . . . . . . . . . . . 17 class 1st
3530, 34cfv 6543 . . . . . . . . . . . . . . . 16 class (1st β€˜π‘’)
3635csn 4628 . . . . . . . . . . . . . . 15 class {(1st β€˜π‘’)}
373, 36cima 5679 . . . . . . . . . . . . . 14 class (𝑒 β€œ {(1st β€˜π‘’)})
3833, 37wss 3948 . . . . . . . . . . . . 13 wff (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)})
39 vx . . . . . . . . . . . . . 14 setvar π‘₯
4039cv 1540 . . . . . . . . . . . . 13 class π‘₯
4138, 29, 40wral 3061 . . . . . . . . . . . 12 wff βˆ€π‘’ ∈ π‘₯ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)})
42 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
4342cv 1540 . . . . . . . . . . . . . . . 16 class 𝑦
44 cmvh 34458 . . . . . . . . . . . . . . . . 17 class mVH
455, 44cfv 6543 . . . . . . . . . . . . . . . 16 class (mVHβ€˜π‘‘)
4643, 45cfv 6543 . . . . . . . . . . . . . . 15 class ((mVHβ€˜π‘‘)β€˜π‘¦)
4728, 46cop 4634 . . . . . . . . . . . . . 14 class βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)⟩
4843, 28cfv 6543 . . . . . . . . . . . . . 14 class (π‘šβ€˜π‘¦)
4947, 48, 17wbr 5148 . . . . . . . . . . . . 13 wff βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦)
50 cmvar 34447 . . . . . . . . . . . . . 14 class mVR
515, 50cfv 6543 . . . . . . . . . . . . 13 class (mVRβ€˜π‘‘)
5249, 42, 51wral 3061 . . . . . . . . . . . 12 wff βˆ€π‘¦ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦)
53 vd . . . . . . . . . . . . . . . . . . 19 setvar 𝑑
5453cv 1540 . . . . . . . . . . . . . . . . . 18 class 𝑑
55 vh . . . . . . . . . . . . . . . . . . 19 setvar β„Ž
5655cv 1540 . . . . . . . . . . . . . . . . . 18 class β„Ž
57 va . . . . . . . . . . . . . . . . . . 19 setvar π‘Ž
5857cv 1540 . . . . . . . . . . . . . . . . . 18 class π‘Ž
5954, 56, 58cotp 4636 . . . . . . . . . . . . . . . . 17 class βŸ¨π‘‘, β„Ž, π‘ŽβŸ©
60 cmax 34451 . . . . . . . . . . . . . . . . . 18 class mAx
615, 60cfv 6543 . . . . . . . . . . . . . . . . 17 class (mAxβ€˜π‘‘)
6259, 61wcel 2106 . . . . . . . . . . . . . . . 16 wff βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘)
63 vz . . . . . . . . . . . . . . . . . . . . . . 23 setvar 𝑧
6463cv 1540 . . . . . . . . . . . . . . . . . . . . . 22 class 𝑧
6543, 64, 54wbr 5148 . . . . . . . . . . . . . . . . . . . . 21 wff 𝑦𝑑𝑧
6664, 28cfv 6543 . . . . . . . . . . . . . . . . . . . . . 22 class (π‘šβ€˜π‘§)
6748, 66, 12wbr 5148 . . . . . . . . . . . . . . . . . . . . 21 wff (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)
6865, 67wi 4 . . . . . . . . . . . . . . . . . . . 20 wff (𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§))
6968, 63wal 1539 . . . . . . . . . . . . . . . . . . 19 wff βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§))
7069, 42wal 1539 . . . . . . . . . . . . . . . . . 18 wff βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§))
7117cdm 5676 . . . . . . . . . . . . . . . . . . . 20 class dom 𝑛
7228csn 4628 . . . . . . . . . . . . . . . . . . . 20 class {π‘š}
7371, 72cima 5679 . . . . . . . . . . . . . . . . . . 19 class (dom 𝑛 β€œ {π‘š})
7456, 73wss 3948 . . . . . . . . . . . . . . . . . 18 wff β„Ž βŠ† (dom 𝑛 β€œ {π‘š})
7570, 74wa 396 . . . . . . . . . . . . . . . . 17 wff (βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š}))
7628, 58, 71wbr 5148 . . . . . . . . . . . . . . . . 17 wff π‘šdom 𝑛 π‘Ž
7775, 76wi 4 . . . . . . . . . . . . . . . 16 wff ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž)
7862, 77wi 4 . . . . . . . . . . . . . . 15 wff (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))
7978, 57wal 1539 . . . . . . . . . . . . . 14 wff βˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))
8079, 55wal 1539 . . . . . . . . . . . . 13 wff βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))
8180, 53wal 1539 . . . . . . . . . . . 12 wff βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))
8241, 52, 81w3a 1087 . . . . . . . . . . 11 wff (βˆ€π‘’ ∈ π‘₯ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)}) ∧ βˆ€π‘¦ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦) ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž)))
83 vs . . . . . . . . . . . . . . . . . . 19 setvar 𝑠
8483cv 1540 . . . . . . . . . . . . . . . . . 18 class 𝑠
8584, 28cop 4634 . . . . . . . . . . . . . . . . 17 class βŸ¨π‘ , π‘šβŸ©
86 cmvsb 34593 . . . . . . . . . . . . . . . . . 18 class mVSubst
875, 86cfv 6543 . . . . . . . . . . . . . . . . 17 class (mVSubstβ€˜π‘‘)
8885, 43, 87wbr 5148 . . . . . . . . . . . . . . . 16 wff βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦
8930, 84cfv 6543 . . . . . . . . . . . . . . . . . . . 20 class (π‘ β€˜π‘’)
9028, 89cop 4634 . . . . . . . . . . . . . . . . . . 19 class βŸ¨π‘š, (π‘ β€˜π‘’)⟩
9190csn 4628 . . . . . . . . . . . . . . . . . 18 class {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}
9217, 91cima 5679 . . . . . . . . . . . . . . . . 17 class (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩})
9343, 30cop 4634 . . . . . . . . . . . . . . . . . . 19 class βŸ¨π‘¦, π‘’βŸ©
9493csn 4628 . . . . . . . . . . . . . . . . . 18 class {βŸ¨π‘¦, π‘’βŸ©}
9517, 94cima 5679 . . . . . . . . . . . . . . . . 17 class (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})
9692, 95wceq 1541 . . . . . . . . . . . . . . . 16 wff (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})
9788, 96wi 4 . . . . . . . . . . . . . . 15 wff (βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©}))
9897, 42wal 1539 . . . . . . . . . . . . . 14 wff βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©}))
9998, 29, 21wral 3061 . . . . . . . . . . . . 13 wff βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©}))
100 cmsub 34457 . . . . . . . . . . . . . . 15 class mSubst
1015, 100cfv 6543 . . . . . . . . . . . . . 14 class (mSubstβ€˜π‘‘)
102101crn 5677 . . . . . . . . . . . . 13 class ran (mSubstβ€˜π‘‘)
10399, 83, 102wral 3061 . . . . . . . . . . . 12 wff βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©}))
104 cmvrs 34455 . . . . . . . . . . . . . . . . . . 19 class mVars
1055, 104cfv 6543 . . . . . . . . . . . . . . . . . 18 class (mVarsβ€˜π‘‘)
10630, 105cfv 6543 . . . . . . . . . . . . . . . . 17 class ((mVarsβ€˜π‘‘)β€˜π‘’)
10728, 106cres 5678 . . . . . . . . . . . . . . . 16 class (π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’))
108 vp . . . . . . . . . . . . . . . . . 18 setvar 𝑝
109108cv 1540 . . . . . . . . . . . . . . . . 17 class 𝑝
110109, 106cres 5678 . . . . . . . . . . . . . . . 16 class (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’))
111107, 110wceq 1541 . . . . . . . . . . . . . . 15 wff (π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’))
112109, 30cop 4634 . . . . . . . . . . . . . . . . . 18 class βŸ¨π‘, π‘’βŸ©
113112csn 4628 . . . . . . . . . . . . . . . . 17 class {βŸ¨π‘, π‘’βŸ©}
11417, 113cima 5679 . . . . . . . . . . . . . . . 16 class (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})
11533, 114wceq 1541 . . . . . . . . . . . . . . 15 wff (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})
116111, 115wi 4 . . . . . . . . . . . . . 14 wff ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©}))
117116, 29, 40wral 3061 . . . . . . . . . . . . 13 wff βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©}))
118117, 108, 19wral 3061 . . . . . . . . . . . 12 wff βˆ€π‘ ∈ 𝑣 βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©}))
11928, 106cima 5679 . . . . . . . . . . . . . . . 16 class (π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’))
12043csn 4628 . . . . . . . . . . . . . . . . 17 class {𝑦}
12112, 120cima 5679 . . . . . . . . . . . . . . . 16 class (𝑓 β€œ {𝑦})
122119, 121wss 3948 . . . . . . . . . . . . . . 15 wff (π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦})
12333, 121wss 3948 . . . . . . . . . . . . . . 15 wff (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦})
124122, 123wi 4 . . . . . . . . . . . . . 14 wff ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦}))
125124, 29, 40wral 3061 . . . . . . . . . . . . 13 wff βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦}))
126125, 42, 3wral 3061 . . . . . . . . . . . 12 wff βˆ€π‘¦ ∈ 𝑒 βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦}))
127103, 118, 126w3a 1087 . . . . . . . . . . 11 wff (βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})) ∧ βˆ€π‘ ∈ 𝑣 βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})) ∧ βˆ€π‘¦ ∈ 𝑒 βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦})))
12882, 127wa 396 . . . . . . . . . 10 wff ((βˆ€π‘’ ∈ π‘₯ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)}) ∧ βˆ€π‘¦ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦) ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))) ∧ (βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})) ∧ βˆ€π‘ ∈ 𝑣 βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})) ∧ βˆ€π‘¦ ∈ 𝑒 βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦}))))
129128, 27, 19wral 3061 . . . . . . . . 9 wff βˆ€π‘š ∈ 𝑣 ((βˆ€π‘’ ∈ π‘₯ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)}) ∧ βˆ€π‘¦ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦) ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))) ∧ (βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})) ∧ βˆ€π‘ ∈ 𝑣 βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})) ∧ βˆ€π‘¦ ∈ 𝑒 βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦}))))
13026, 129wa 396 . . . . . . . 8 wff ((𝑒 βŠ† ((mTCβ€˜π‘‘) Γ— V) ∧ 𝑓 ∈ (mFRelβ€˜π‘‘) ∧ 𝑛 ∈ (𝑒 ↑pm (𝑣 Γ— (mExβ€˜π‘‘)))) ∧ βˆ€π‘š ∈ 𝑣 ((βˆ€π‘’ ∈ π‘₯ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)}) ∧ βˆ€π‘¦ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦) ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))) ∧ (βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})) ∧ βˆ€π‘ ∈ 𝑣 βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})) ∧ βˆ€π‘¦ ∈ 𝑒 βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦})))))
131 cmfsh 34594 . . . . . . . . 9 class mFresh
1325, 131cfv 6543 . . . . . . . 8 class (mFreshβ€˜π‘‘)
133130, 11, 132wsbc 3777 . . . . . . 7 wff [(mFreshβ€˜π‘‘) / 𝑓]((𝑒 βŠ† ((mTCβ€˜π‘‘) Γ— V) ∧ 𝑓 ∈ (mFRelβ€˜π‘‘) ∧ 𝑛 ∈ (𝑒 ↑pm (𝑣 Γ— (mExβ€˜π‘‘)))) ∧ βˆ€π‘š ∈ 𝑣 ((βˆ€π‘’ ∈ π‘₯ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)}) ∧ βˆ€π‘¦ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦) ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))) ∧ (βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})) ∧ βˆ€π‘ ∈ 𝑣 βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})) ∧ βˆ€π‘¦ ∈ 𝑒 βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦})))))
134 cmevl 34596 . . . . . . . 8 class mEval
1355, 134cfv 6543 . . . . . . 7 class (mEvalβ€˜π‘‘)
136133, 16, 135wsbc 3777 . . . . . 6 wff [(mEvalβ€˜π‘‘) / 𝑛][(mFreshβ€˜π‘‘) / 𝑓]((𝑒 βŠ† ((mTCβ€˜π‘‘) Γ— V) ∧ 𝑓 ∈ (mFRelβ€˜π‘‘) ∧ 𝑛 ∈ (𝑒 ↑pm (𝑣 Γ— (mExβ€˜π‘‘)))) ∧ βˆ€π‘š ∈ 𝑣 ((βˆ€π‘’ ∈ π‘₯ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)}) ∧ βˆ€π‘¦ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦) ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))) ∧ (βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})) ∧ βˆ€π‘ ∈ 𝑣 βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})) ∧ βˆ€π‘¦ ∈ 𝑒 βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦})))))
137 cmvl 34592 . . . . . . 7 class mVL
1385, 137cfv 6543 . . . . . 6 class (mVLβ€˜π‘‘)
139136, 18, 138wsbc 3777 . . . . 5 wff [(mVLβ€˜π‘‘) / 𝑣][(mEvalβ€˜π‘‘) / 𝑛][(mFreshβ€˜π‘‘) / 𝑓]((𝑒 βŠ† ((mTCβ€˜π‘‘) Γ— V) ∧ 𝑓 ∈ (mFRelβ€˜π‘‘) ∧ 𝑛 ∈ (𝑒 ↑pm (𝑣 Γ— (mExβ€˜π‘‘)))) ∧ βˆ€π‘š ∈ 𝑣 ((βˆ€π‘’ ∈ π‘₯ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑒 β€œ {(1st β€˜π‘’)}) ∧ βˆ€π‘¦ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘¦)βŸ©π‘›(π‘šβ€˜π‘¦) ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ ((βˆ€π‘¦βˆ€π‘§(𝑦𝑑𝑧 β†’ (π‘šβ€˜π‘¦)𝑓(π‘šβ€˜π‘§)) ∧ β„Ž βŠ† (dom 𝑛 β€œ {π‘š})) β†’ π‘šdom 𝑛 π‘Ž))) ∧ (βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)βˆ€π‘¦(βŸ¨π‘ , π‘šβŸ©(mVSubstβ€˜π‘‘)𝑦 β†’ (𝑛 β€œ {βŸ¨π‘š, (π‘ β€˜π‘’)⟩}) = (𝑛 β€œ {βŸ¨π‘¦, π‘’βŸ©})) ∧ βˆ€π‘ ∈ 𝑣 βˆ€π‘’ ∈ π‘₯ ((π‘š β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) = (𝑝 β†Ύ ((mVarsβ€˜π‘‘)β€˜π‘’)) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = (𝑛 β€œ {βŸ¨π‘, π‘’βŸ©})) ∧ βˆ€π‘¦ ∈ 𝑒 βˆ€π‘’ ∈ π‘₯ ((π‘š β€œ ((mVarsβ€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦})))))
140139, 39, 21wsbc 3777 . . . 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 34591 . . . . 5 class mUV
1425, 141cfv 6543 . . . 4 class (mUVβ€˜π‘‘)
143140, 2, 142wsbc 3777 . . 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 34462 . . 3 class mFS
145143, 4, 144crab 3432 . 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β€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦})))))}
1461, 145wceq 1541 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β€˜π‘‘)β€˜π‘’)) βŠ† (𝑓 β€œ {𝑦}) β†’ (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) βŠ† (𝑓 β€œ {𝑦})))))}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator