Detailed syntax breakdown of Definition df-mcls
Step | Hyp | Ref
| Expression |
1 | | cmcls 33175 |
. 2
class
mCls |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3421 |
. . 3
class
V |
4 | | vd |
. . . 4
setvar 𝑑 |
5 | | vh |
. . . 4
setvar ℎ |
6 | 2 | cv 1542 |
. . . . . 6
class 𝑡 |
7 | | cmdv 33166 |
. . . . . 6
class
mDV |
8 | 6, 7 | cfv 6398 |
. . . . 5
class
(mDV‘𝑡) |
9 | 8 | cpw 4528 |
. . . 4
class 𝒫
(mDV‘𝑡) |
10 | | cmex 33165 |
. . . . . 6
class
mEx |
11 | 6, 10 | cfv 6398 |
. . . . 5
class
(mEx‘𝑡) |
12 | 11 | cpw 4528 |
. . . 4
class 𝒫
(mEx‘𝑡) |
13 | 5 | cv 1542 |
. . . . . . . . 9
class ℎ |
14 | | cmvh 33170 |
. . . . . . . . . . 11
class
mVH |
15 | 6, 14 | cfv 6398 |
. . . . . . . . . 10
class
(mVH‘𝑡) |
16 | 15 | crn 5567 |
. . . . . . . . 9
class ran
(mVH‘𝑡) |
17 | 13, 16 | cun 3879 |
. . . . . . . 8
class (ℎ ∪ ran (mVH‘𝑡)) |
18 | | vc |
. . . . . . . . 9
setvar 𝑐 |
19 | 18 | cv 1542 |
. . . . . . . 8
class 𝑐 |
20 | 17, 19 | wss 3881 |
. . . . . . 7
wff (ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 |
21 | | vm |
. . . . . . . . . . . . . 14
setvar 𝑚 |
22 | 21 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑚 |
23 | | vo |
. . . . . . . . . . . . . 14
setvar 𝑜 |
24 | 23 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑜 |
25 | | vp |
. . . . . . . . . . . . . 14
setvar 𝑝 |
26 | 25 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑝 |
27 | 22, 24, 26 | cotp 4564 |
. . . . . . . . . . . 12
class
〈𝑚, 𝑜, 𝑝〉 |
28 | | cmax 33163 |
. . . . . . . . . . . . 13
class
mAx |
29 | 6, 28 | cfv 6398 |
. . . . . . . . . . . 12
class
(mAx‘𝑡) |
30 | 27, 29 | wcel 2111 |
. . . . . . . . . . 11
wff 〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) |
31 | | vs |
. . . . . . . . . . . . . . . . 17
setvar 𝑠 |
32 | 31 | cv 1542 |
. . . . . . . . . . . . . . . 16
class 𝑠 |
33 | 24, 16 | cun 3879 |
. . . . . . . . . . . . . . . 16
class (𝑜 ∪ ran (mVH‘𝑡)) |
34 | 32, 33 | cima 5569 |
. . . . . . . . . . . . . . 15
class (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) |
35 | 34, 19 | wss 3881 |
. . . . . . . . . . . . . 14
wff (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 |
36 | | vx |
. . . . . . . . . . . . . . . . . . 19
setvar 𝑥 |
37 | 36 | cv 1542 |
. . . . . . . . . . . . . . . . . 18
class 𝑥 |
38 | | vy |
. . . . . . . . . . . . . . . . . . 19
setvar 𝑦 |
39 | 38 | cv 1542 |
. . . . . . . . . . . . . . . . . 18
class 𝑦 |
40 | 37, 39, 22 | wbr 5068 |
. . . . . . . . . . . . . . . . 17
wff 𝑥𝑚𝑦 |
41 | 37, 15 | cfv 6398 |
. . . . . . . . . . . . . . . . . . . . 21
class
((mVH‘𝑡)‘𝑥) |
42 | 41, 32 | cfv 6398 |
. . . . . . . . . . . . . . . . . . . 20
class (𝑠‘((mVH‘𝑡)‘𝑥)) |
43 | | cmvrs 33167 |
. . . . . . . . . . . . . . . . . . . . 21
class
mVars |
44 | 6, 43 | cfv 6398 |
. . . . . . . . . . . . . . . . . . . 20
class
(mVars‘𝑡) |
45 | 42, 44 | cfv 6398 |
. . . . . . . . . . . . . . . . . . 19
class
((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) |
46 | 39, 15 | cfv 6398 |
. . . . . . . . . . . . . . . . . . . . 21
class
((mVH‘𝑡)‘𝑦) |
47 | 46, 32 | cfv 6398 |
. . . . . . . . . . . . . . . . . . . 20
class (𝑠‘((mVH‘𝑡)‘𝑦)) |
48 | 47, 44 | cfv 6398 |
. . . . . . . . . . . . . . . . . . 19
class
((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦))) |
49 | 45, 48 | cxp 5564 |
. . . . . . . . . . . . . . . . . 18
class
(((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) |
50 | 4 | cv 1542 |
. . . . . . . . . . . . . . . . . 18
class 𝑑 |
51 | 49, 50 | wss 3881 |
. . . . . . . . . . . . . . . . 17
wff
(((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑 |
52 | 40, 51 | wi 4 |
. . . . . . . . . . . . . . . 16
wff (𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) |
53 | 52, 38 | wal 1541 |
. . . . . . . . . . . . . . 15
wff
∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) |
54 | 53, 36 | wal 1541 |
. . . . . . . . . . . . . 14
wff
∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) |
55 | 35, 54 | wa 399 |
. . . . . . . . . . . . 13
wff ((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) |
56 | 26, 32 | cfv 6398 |
. . . . . . . . . . . . . 14
class (𝑠‘𝑝) |
57 | 56, 19 | wcel 2111 |
. . . . . . . . . . . . 13
wff (𝑠‘𝑝) ∈ 𝑐 |
58 | 55, 57 | wi 4 |
. . . . . . . . . . . 12
wff (((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐) |
59 | | cmsub 33169 |
. . . . . . . . . . . . . 14
class
mSubst |
60 | 6, 59 | cfv 6398 |
. . . . . . . . . . . . 13
class
(mSubst‘𝑡) |
61 | 60 | crn 5567 |
. . . . . . . . . . . 12
class ran
(mSubst‘𝑡) |
62 | 58, 31, 61 | wral 3062 |
. . . . . . . . . . 11
wff
∀𝑠 ∈ ran
(mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐) |
63 | 30, 62 | wi 4 |
. . . . . . . . . 10
wff
(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) |
64 | 63, 25 | wal 1541 |
. . . . . . . . 9
wff
∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) |
65 | 64, 23 | wal 1541 |
. . . . . . . 8
wff
∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) |
66 | 65, 21 | wal 1541 |
. . . . . . 7
wff
∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) |
67 | 20, 66 | wa 399 |
. . . . . 6
wff ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))) |
68 | 67, 18 | cab 2715 |
. . . . 5
class {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))} |
69 | 68 | cint 4874 |
. . . 4
class ∩ {𝑐
∣ ((ℎ ∪ ran
(mVH‘𝑡)) ⊆
𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))} |
70 | 4, 5, 9, 12, 69 | cmpo 7234 |
. . 3
class (𝑑 ∈ 𝒫
(mDV‘𝑡), ℎ ∈ 𝒫
(mEx‘𝑡) ↦ ∩ {𝑐
∣ ((ℎ ∪ ran
(mVH‘𝑡)) ⊆
𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}) |
71 | 2, 3, 70 | cmpt 5150 |
. 2
class (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫
(mDV‘𝑡), ℎ ∈ 𝒫
(mEx‘𝑡) ↦ ∩ {𝑐
∣ ((ℎ ∪ ran
(mVH‘𝑡)) ⊆
𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))})) |
72 | 1, 71 | wceq 1543 |
1
wff mCls =
(𝑡 ∈ V ↦ (𝑑 ∈ 𝒫
(mDV‘𝑡), ℎ ∈ 𝒫
(mEx‘𝑡) ↦ ∩ {𝑐
∣ ((ℎ ∪ ran
(mVH‘𝑡)) ⊆
𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))})) |