Metamath Proof Explorer

Definition df-mst

Description: Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mst ⊢ mST = t ∈ V ⟼ ∅ mTree ⁡ t ∅ ↾ mEx ⁡ t ↾ mVT ⁡ t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmst class mST
1 vt setvar t
2 cvv class V
3 c0 class ∅
4 cmtree class mTree
5 1 cv setvar t
6 5 4 cfv class mTree ⁡ t
7 3 3 6 co class ∅ mTree ⁡ t ∅
8 cmex class mEx
9 5 8 cfv class mEx ⁡ t
10 cmvt class mVT
11 5 10 cfv class mVT ⁡ t
12 9 11 cres class mEx ⁡ t ↾ mVT ⁡ t
13 7 12 cres class ∅ mTree ⁡ t ∅ ↾ mEx ⁡ t ↾ mVT ⁡ t
14 1 2 13 cmpt class t ∈ V ⟼ ∅ mTree ⁡ t ∅ ↾ mEx ⁡ t ↾ mVT ⁡ t
15 0 14 wceq wff mST = t ∈ V ⟼ ∅ mTree ⁡ t ∅ ↾ mEx ⁡ t ↾ mVT ⁡ t