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

Definition df-mtree 34195
Description: Define the set of proof trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mtree mTree = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩ ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)))}))
Distinct variable group:   𝑒,𝑑,,𝑚,𝑜,𝑝,𝑟,𝑠,𝑡,𝑥,𝑦

Detailed syntax breakdown of Definition df-mtree
StepHypRef Expression
1 cmtree 34185 . 2 class mTree
2 vt . . 3 setvar 𝑡
3 cvv 3445 . . 3 class V
4 vd . . . 4 setvar 𝑑
5 vh . . . 4 setvar
62cv 1540 . . . . . 6 class 𝑡
7 cmdv 34062 . . . . . 6 class mDV
86, 7cfv 6496 . . . . 5 class (mDV‘𝑡)
98cpw 4560 . . . 4 class 𝒫 (mDV‘𝑡)
10 cmex 34061 . . . . . 6 class mEx
116, 10cfv 6496 . . . . 5 class (mEx‘𝑡)
1211cpw 4560 . . . 4 class 𝒫 (mEx‘𝑡)
13 ve . . . . . . . . . 10 setvar 𝑒
1413cv 1540 . . . . . . . . 9 class 𝑒
15 cm0s 34179 . . . . . . . . . . 11 class m0St
1614, 15cfv 6496 . . . . . . . . . 10 class (m0St‘𝑒)
17 c0 4282 . . . . . . . . . 10 class
1816, 17cop 4592 . . . . . . . . 9 class ⟨(m0St‘𝑒), ∅⟩
19 vr . . . . . . . . . 10 setvar 𝑟
2019cv 1540 . . . . . . . . 9 class 𝑟
2114, 18, 20wbr 5105 . . . . . . . 8 wff 𝑒𝑟⟨(m0St‘𝑒), ∅⟩
22 cmvh 34066 . . . . . . . . . 10 class mVH
236, 22cfv 6496 . . . . . . . . 9 class (mVH‘𝑡)
2423crn 5634 . . . . . . . 8 class ran (mVH‘𝑡)
2521, 13, 24wral 3064 . . . . . . 7 wff 𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩
264cv 1540 . . . . . . . . . . . 12 class 𝑑
275cv 1540 . . . . . . . . . . . 12 class
2826, 27, 14cotp 4594 . . . . . . . . . . 11 class 𝑑, , 𝑒
29 cmsr 34068 . . . . . . . . . . . 12 class mStRed
306, 29cfv 6496 . . . . . . . . . . 11 class (mStRed‘𝑡)
3128, 30cfv 6496 . . . . . . . . . 10 class ((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩)
3231, 17cop 4592 . . . . . . . . 9 class ⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩
3314, 32, 20wbr 5105 . . . . . . . 8 wff 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩
3433, 13, 27wral 3064 . . . . . . 7 wff 𝑒 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩
35 vm . . . . . . . . . . . . . 14 setvar 𝑚
3635cv 1540 . . . . . . . . . . . . 13 class 𝑚
37 vo . . . . . . . . . . . . . 14 setvar 𝑜
3837cv 1540 . . . . . . . . . . . . 13 class 𝑜
39 vp . . . . . . . . . . . . . 14 setvar 𝑝
4039cv 1540 . . . . . . . . . . . . 13 class 𝑝
4136, 38, 40cotp 4594 . . . . . . . . . . . 12 class 𝑚, 𝑜, 𝑝
42 cmax 34059 . . . . . . . . . . . . 13 class mAx
436, 42cfv 6496 . . . . . . . . . . . 12 class (mAx‘𝑡)
4441, 43wcel 2106 . . . . . . . . . . 11 wff 𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡)
45 vx . . . . . . . . . . . . . . . . . 18 setvar 𝑥
4645cv 1540 . . . . . . . . . . . . . . . . 17 class 𝑥
47 vy . . . . . . . . . . . . . . . . . 18 setvar 𝑦
4847cv 1540 . . . . . . . . . . . . . . . . 17 class 𝑦
4946, 48, 36wbr 5105 . . . . . . . . . . . . . . . 16 wff 𝑥𝑚𝑦
5046, 23cfv 6496 . . . . . . . . . . . . . . . . . . . 20 class ((mVH‘𝑡)‘𝑥)
51 vs . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑠
5251cv 1540 . . . . . . . . . . . . . . . . . . . 20 class 𝑠
5350, 52cfv 6496 . . . . . . . . . . . . . . . . . . 19 class (𝑠‘((mVH‘𝑡)‘𝑥))
54 cmvrs 34063 . . . . . . . . . . . . . . . . . . . 20 class mVars
556, 54cfv 6496 . . . . . . . . . . . . . . . . . . 19 class (mVars‘𝑡)
5653, 55cfv 6496 . . . . . . . . . . . . . . . . . 18 class ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥)))
5748, 23cfv 6496 . . . . . . . . . . . . . . . . . . . 20 class ((mVH‘𝑡)‘𝑦)
5857, 52cfv 6496 . . . . . . . . . . . . . . . . . . 19 class (𝑠‘((mVH‘𝑡)‘𝑦))
5958, 55cfv 6496 . . . . . . . . . . . . . . . . . 18 class ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))
6056, 59cxp 5631 . . . . . . . . . . . . . . . . 17 class (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦))))
6160, 26wss 3910 . . . . . . . . . . . . . . . 16 wff (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑
6249, 61wi 4 . . . . . . . . . . . . . . 15 wff (𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
6362, 47wal 1539 . . . . . . . . . . . . . 14 wff 𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
6463, 45wal 1539 . . . . . . . . . . . . 13 wff 𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
6540, 52cfv 6496 . . . . . . . . . . . . . . . 16 class (𝑠𝑝)
6665csn 4586 . . . . . . . . . . . . . . 15 class {(𝑠𝑝)}
6740csn 4586 . . . . . . . . . . . . . . . . . . . . 21 class {𝑝}
6838, 67cun 3908 . . . . . . . . . . . . . . . . . . . 20 class (𝑜 ∪ {𝑝})
6955, 68cima 5636 . . . . . . . . . . . . . . . . . . 19 class ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))
7069cuni 4865 . . . . . . . . . . . . . . . . . 18 class ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))
7123, 70cima 5636 . . . . . . . . . . . . . . . . 17 class ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝})))
7238, 71cun 3908 . . . . . . . . . . . . . . . 16 class (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))
7314, 52cfv 6496 . . . . . . . . . . . . . . . . . 18 class (𝑠𝑒)
7473csn 4586 . . . . . . . . . . . . . . . . 17 class {(𝑠𝑒)}
7520, 74cima 5636 . . . . . . . . . . . . . . . 16 class (𝑟 “ {(𝑠𝑒)})
7613, 72, 75cixp 8835 . . . . . . . . . . . . . . 15 class X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})
7766, 76cxp 5631 . . . . . . . . . . . . . 14 class ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)}))
7877, 20wss 3910 . . . . . . . . . . . . 13 wff ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟
7964, 78wi 4 . . . . . . . . . . . 12 wff (∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)
80 cmsub 34065 . . . . . . . . . . . . . 14 class mSubst
816, 80cfv 6496 . . . . . . . . . . . . 13 class (mSubst‘𝑡)
8281crn 5634 . . . . . . . . . . . 12 class ran (mSubst‘𝑡)
8379, 51, 82wral 3064 . . . . . . . . . . 11 wff 𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)
8444, 83wi 4 . . . . . . . . . 10 wff (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟))
8584, 39wal 1539 . . . . . . . . 9 wff 𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟))
8685, 37wal 1539 . . . . . . . 8 wff 𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟))
8786, 35wal 1539 . . . . . . 7 wff 𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟))
8825, 34, 87w3a 1087 . . . . . 6 wff (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩ ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)))
8988, 19cab 2713 . . . . 5 class {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩ ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)))}
9089cint 4907 . . . 4 class {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩ ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)))}
914, 5, 9, 12, 90cmpo 7359 . . 3 class (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩ ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)))})
922, 3, 91cmpt 5188 . 2 class (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩ ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)))}))
931, 92wceq 1541 1 wff mTree = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, , 𝑒⟩), ∅⟩ ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠𝑒)})) ⊆ 𝑟)))}))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator