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 e. _V |-> ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { r | ( A. e e. ran ( mVH ` t ) e r <. ( m0St ` e ) , (/) >. /\ A. e e. h e r <. ( ( mStRed ` t ) ` <. d , h , e >. ) , (/) >. /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) -> ( { ( s ` p ) } X. X_ e e. ( o u. ( ( mVH ` t ) " U. ( ( mVars ` t ) " ( o u. { p } ) ) ) ) ( r " { ( s ` e ) } ) ) C_ r ) ) ) } ) )

Detailed syntax breakdown

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