Metamath Proof Explorer

Definition df-mtree

Description: Define the set of proof trees. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mtree mTree = ( 𝑡 ∈ V ↦ ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑟 ∣ ( ∀ 𝑒 ∈ ran ( mVH ‘ 𝑡 ) 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩ ∧ ∀ 𝑒 ∈ ℎ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩ ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmtree ⊢ mTree
1 vt ⊢ 𝑡
2 cvv ⊢ V
3 vd ⊢ 𝑑
4 cmdv ⊢ mDV
5 1 cv ⊢ 𝑡
6 5 4 cfv ⊢ ( mDV ‘ 𝑡 )
7 6 cpw ⊢ 𝒫 ( mDV ‘ 𝑡 )
8 vh ⊢ ℎ
9 cmex ⊢ mEx
10 5 9 cfv ⊢ ( mEx ‘ 𝑡 )
11 10 cpw ⊢ 𝒫 ( mEx ‘ 𝑡 )
12 vr ⊢ 𝑟
13 ve ⊢ 𝑒
14 cmvh ⊢ mVH
15 5 14 cfv ⊢ ( mVH ‘ 𝑡 )
16 15 crn ⊢ ran ( mVH ‘ 𝑡 )
17 13 cv ⊢ 𝑒
18 12 cv ⊢ 𝑟
19 cm0s ⊢ m0St
20 17 19 cfv ⊢ ( m0St ‘ 𝑒 )
21 c0 ⊢ ∅
22 20 21 cop ⊢ ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩
23 17 22 18 wbr ⊢ 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩
24 23 13 16 wral ⊢ ∀ 𝑒 ∈ ran ( mVH ‘ 𝑡 ) 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩
25 8 cv ⊢ ℎ
26 cmsr ⊢ mStRed
27 5 26 cfv ⊢ ( mStRed ‘ 𝑡 )
28 3 cv ⊢ 𝑑
29 28 25 17 cotp ⊢ ⟨ 𝑑 , ℎ , 𝑒 ⟩
30 29 27 cfv ⊢ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ )
31 30 21 cop ⊢ ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩
32 17 31 18 wbr ⊢ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩
33 32 13 25 wral ⊢ ∀ 𝑒 ∈ ℎ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩
34 vm ⊢ 𝑚
35 vo ⊢ 𝑜
36 vp ⊢ 𝑝
37 34 cv ⊢ 𝑚
38 35 cv ⊢ 𝑜
39 36 cv ⊢ 𝑝
40 37 38 39 cotp ⊢ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩
41 cmax ⊢ mAx
42 5 41 cfv ⊢ ( mAx ‘ 𝑡 )
43 40 42 wcel ⊢ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 )
44 vs ⊢ 𝑠
45 cmsub ⊢ mSubst
46 5 45 cfv ⊢ ( mSubst ‘ 𝑡 )
47 46 crn ⊢ ran ( mSubst ‘ 𝑡 )
48 vx ⊢ 𝑥
49 vy ⊢ 𝑦
50 48 cv ⊢ 𝑥
51 49 cv ⊢ 𝑦
52 50 51 37 wbr ⊢ 𝑥 𝑚 𝑦
53 cmvrs ⊢ mVars
54 5 53 cfv ⊢ ( mVars ‘ 𝑡 )
55 44 cv ⊢ 𝑠
56 50 15 cfv ⊢ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 )
57 56 55 cfv ⊢ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) )
58 57 54 cfv ⊢ ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) )
59 51 15 cfv ⊢ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 )
60 59 55 cfv ⊢ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) )
61 60 54 cfv ⊢ ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) )
62 58 61 cxp ⊢ ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) )
63 62 28 wss ⊢ ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑
64 52 63 wi ⊢ ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 )
65 64 49 wal ⊢ ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 )
66 65 48 wal ⊢ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 )
67 39 55 cfv ⊢ ( 𝑠 ‘ 𝑝 )
68 67 csn ⊢ { ( 𝑠 ‘ 𝑝 ) }
69 39 csn ⊢ { 𝑝 }
70 38 69 cun ⊢ ( 𝑜 ∪ { 𝑝 } )
71 54 70 cima ⊢ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) )
72 71 cuni ⊢ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) )
73 15 72 cima ⊢ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) )
74 38 73 cun ⊢ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) )
75 17 55 cfv ⊢ ( 𝑠 ‘ 𝑒 )
76 75 csn ⊢ { ( 𝑠 ‘ 𝑒 ) }
77 18 76 cima ⊢ ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } )
78 13 74 77 cixp ⊢ X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } )
79 68 78 cxp ⊢ ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) )
80 79 18 wss ⊢ ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟
81 66 80 wi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 )
82 81 44 47 wral ⊢ ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 )
83 43 82 wi ⊢ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) )
84 83 36 wal ⊢ ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) )
85 84 35 wal ⊢ ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) )
86 85 34 wal ⊢ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) )
87 24 33 86 w3a ⊢ ( ∀ 𝑒 ∈ ran ( mVH ‘ 𝑡 ) 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩ ∧ ∀ 𝑒 ∈ ℎ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩ ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) ) )
88 87 12 cab ⊢ { 𝑟 ∣ ( ∀ 𝑒 ∈ ran ( mVH ‘ 𝑡 ) 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩ ∧ ∀ 𝑒 ∈ ℎ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩ ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) ) ) }
89 88 cint ⊢ ∩ { 𝑟 ∣ ( ∀ 𝑒 ∈ ran ( mVH ‘ 𝑡 ) 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩ ∧ ∀ 𝑒 ∈ ℎ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩ ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) ) ) }
90 3 8 7 11 89 cmpo ⊢ ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑟 ∣ ( ∀ 𝑒 ∈ ran ( mVH ‘ 𝑡 ) 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩ ∧ ∀ 𝑒 ∈ ℎ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩ ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) ) ) } )
91 1 2 90 cmpt ⊢ ( 𝑡 ∈ V ↦ ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑟 ∣ ( ∀ 𝑒 ∈ ran ( mVH ‘ 𝑡 ) 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩ ∧ ∀ 𝑒 ∈ ℎ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩ ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) ) ) } ) )
92 0 91 wceq ⊢ mTree = ( 𝑡 ∈ V ↦ ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑟 ∣ ( ∀ 𝑒 ∈ ran ( mVH ‘ 𝑡 ) 𝑒 𝑟 ⟨ ( m0St ‘ 𝑒 ) , ∅ ⟩ ∧ ∀ 𝑒 ∈ ℎ 𝑒 𝑟 ⟨ ( ( mStRed ‘ 𝑡 ) ‘ ⟨ 𝑑 , ℎ , 𝑒 ⟩ ) , ∅ ⟩ ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) → ( { ( 𝑠 ‘ 𝑝 ) } × X 𝑒 ∈ ( 𝑜 ∪ ( ( mVH ‘ 𝑡 ) “ ∪ ( ( mVars ‘ 𝑡 ) “ ( 𝑜 ∪ { 𝑝 } ) ) ) ) ( 𝑟 “ { ( 𝑠 ‘ 𝑒 ) } ) ) ⊆ 𝑟 ) ) ) } ) )