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 = t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ r | ∀ e ∈ ran ⁡ mVH ⁡ t e r m0St ⁡ e ∅ ∧ ∀ e ∈ h e r mStRed ⁡ t ⁡ d h e ∅ ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmtree class mTree
1 vt setvar t
2 cvv class V
3 vd setvar d
4 cmdv class mDV
5 1 cv setvar t
6 5 4 cfv class mDV ⁡ t
7 6 cpw class 𝒫 mDV ⁡ t
8 vh setvar h
9 cmex class mEx
10 5 9 cfv class mEx ⁡ t
11 10 cpw class 𝒫 mEx ⁡ t
12 vr setvar r
13 ve setvar e
14 cmvh class mVH
15 5 14 cfv class mVH ⁡ t
16 15 crn class ran ⁡ mVH ⁡ t
17 13 cv setvar e
18 12 cv setvar r
19 cm0s class m0St
20 17 19 cfv class m0St ⁡ e
21 c0 class ∅
22 20 21 cop class m0St ⁡ e ∅
23 17 22 18 wbr wff e r m0St ⁡ e ∅
24 23 13 16 wral wff ∀ e ∈ ran ⁡ mVH ⁡ t e r m0St ⁡ e ∅
25 8 cv setvar h
26 cmsr class mStRed
27 5 26 cfv class mStRed ⁡ t
28 3 cv setvar d
29 28 25 17 cotp class d h e
30 29 27 cfv class mStRed ⁡ t ⁡ d h e
31 30 21 cop class mStRed ⁡ t ⁡ d h e ∅
32 17 31 18 wbr wff e r mStRed ⁡ t ⁡ d h e ∅
33 32 13 25 wral wff ∀ e ∈ h e r mStRed ⁡ t ⁡ d h e ∅
34 vm setvar m
35 vo setvar o
36 vp setvar p
37 34 cv setvar m
38 35 cv setvar o
39 36 cv setvar p
40 37 38 39 cotp class m o p
41 cmax class mAx
42 5 41 cfv class mAx ⁡ t
43 40 42 wcel wff m o p ∈ mAx ⁡ t
44 vs setvar s
45 cmsub class mSubst
46 5 45 cfv class mSubst ⁡ t
47 46 crn class ran ⁡ mSubst ⁡ t
48 vx setvar x
49 vy setvar y
50 48 cv setvar x
51 49 cv setvar y
52 50 51 37 wbr wff x m y
53 cmvrs class mVars
54 5 53 cfv class mVars ⁡ t
55 44 cv setvar s
56 50 15 cfv class mVH ⁡ t ⁡ x
57 56 55 cfv class s ⁡ mVH ⁡ t ⁡ x
58 57 54 cfv class mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x
59 51 15 cfv class mVH ⁡ t ⁡ y
60 59 55 cfv class s ⁡ mVH ⁡ t ⁡ y
61 60 54 cfv class mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y
62 58 61 cxp class mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y
63 62 28 wss wff mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
64 52 63 wi wff x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
65 64 49 wal wff ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
66 65 48 wal wff ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
67 39 55 cfv class s ⁡ p
68 67 csn class s ⁡ p
69 39 csn class p
70 38 69 cun class o ∪ p
71 54 70 cima class mVars ⁡ t o ∪ p
72 71 cuni class ⋃ mVars ⁡ t o ∪ p
73 15 72 cima class mVH ⁡ t ⋃ mVars ⁡ t o ∪ p
74 38 73 cun class o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p
75 17 55 cfv class s ⁡ e
76 75 csn class s ⁡ e
77 18 76 cima class r s ⁡ e
78 13 74 77 cixp class ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e
79 68 78 cxp class s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e
80 79 18 wss wff s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
81 66 80 wi wff ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
82 81 44 47 wral wff ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
83 43 82 wi wff m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
84 83 36 wal wff ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
85 84 35 wal wff ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
86 85 34 wal wff ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
87 24 33 86 w3a wff ∀ e ∈ ran ⁡ mVH ⁡ t e r m0St ⁡ e ∅ ∧ ∀ e ∈ h e r mStRed ⁡ t ⁡ d h e ∅ ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
88 87 12 cab class r | ∀ e ∈ ran ⁡ mVH ⁡ t e r m0St ⁡ e ∅ ∧ ∀ e ∈ h e r mStRed ⁡ t ⁡ d h e ∅ ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
89 88 cint class ⋂ r | ∀ e ∈ ran ⁡ mVH ⁡ t e r m0St ⁡ e ∅ ∧ ∀ e ∈ h e r mStRed ⁡ t ⁡ d h e ∅ ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
90 3 8 7 11 89 cmpo class d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ r | ∀ e ∈ ran ⁡ mVH ⁡ t e r m0St ⁡ e ∅ ∧ ∀ e ∈ h e r mStRed ⁡ t ⁡ d h e ∅ ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
91 1 2 90 cmpt class t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ r | ∀ e ∈ ran ⁡ mVH ⁡ t e r m0St ⁡ e ∅ ∧ ∀ e ∈ h e r mStRed ⁡ t ⁡ d h e ∅ ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r
92 0 91 wceq wff mTree = t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ r | ∀ e ∈ ran ⁡ mVH ⁡ t e r m0St ⁡ e ∅ ∧ ∀ e ∈ h e r mStRed ⁡ t ⁡ d h e ∅ ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p × ⨉ e ∈ o ∪ mVH ⁡ t ⋃ mVars ⁡ t o ∪ p r s ⁡ e ⊆ r