Definition df-mtree 31496

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

Assertion

Ref

Expression

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 ) ) ) } ) )

Distinct variable group:   e, d, h, m, o, p, r, s, t, x, y

Detailed syntax breakdown of Definition df-mtree

Step	Hyp	Ref	Expression
1		cmtree 31488	. 2 class mTree
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vd	. . . 4 setvar d
5		vh	. . . 4 setvar h
6	2	cv 1482	. . . . . 6 class t
7		cmdv 31365	. . . . . 6 class mDV
8	6, 7	cfv 5888	. . . . 5 class (mDV ` t )
9	8	cpw 4158	. . . 4 class ~P (mDV ` t )
10		cmex 31364	. . . . . 6 class mEx
11	6, 10	cfv 5888	. . . . 5 class (mEx ` t )
12	11	cpw 4158	. . . 4 class ~P (mEx ` t )
13		ve	. . . . . . . . . 10 setvar e
14	13	cv 1482	. . . . . . . . 9 class e
15		cm0s 31482	. . . . . . . . . . 11 class m0St
16	14, 15	cfv 5888	. . . . . . . . . 10 class (m0St ` e )
17		c0 3915	. . . . . . . . . 10 class (/)
18	16, 17	cop 4183	. . . . . . . . 9 class <. (m0St ` e ) , (/) >.
19		vr	. . . . . . . . . 10 setvar r
20	19	cv 1482	. . . . . . . . 9 class r
21	14, 18, 20	wbr 4653	. . . . . . . 8 wff e r <. (m0St ` e ) , (/) >.
22		cmvh 31369	. . . . . . . . . 10 class mVH
23	6, 22	cfv 5888	. . . . . . . . 9 class (mVH ` t )
24	23	crn 5115	. . . . . . . 8 class ran (mVH ` t )
25	21, 13, 24	wral 2912	. . . . . . 7 wff A. e e. ran (mVH ` t ) e r <. (m0St ` e ) , (/) >.
26	4	cv 1482	. . . . . . . . . . . 12 class d
27	5	cv 1482	. . . . . . . . . . . 12 class h
28	26, 27, 14	cotp 4185	. . . . . . . . . . 11 class <. d , h , e >.
29		cmsr 31371	. . . . . . . . . . . 12 class mStRed
30	6, 29	cfv 5888	. . . . . . . . . . 11 class (mStRed ` t )
31	28, 30	cfv 5888	. . . . . . . . . 10 class ( (mStRed ` t ) ` <. d , h , e >. )
32	31, 17	cop 4183	. . . . . . . . 9 class <. ( (mStRed ` t ) ` <. d , h , e >. ) , (/) >.
33	14, 32, 20	wbr 4653	. . . . . . . 8 wff e r <. ( (mStRed ` t ) ` <. d , h , e >. ) , (/) >.
34	33, 13, 27	wral 2912	. . . . . . 7 wff A. e e. h e r <. ( (mStRed ` t ) ` <. d , h , e >. ) , (/) >.
35		vm	. . . . . . . . . . . . . 14 setvar m
36	35	cv 1482	. . . . . . . . . . . . 13 class m
37		vo	. . . . . . . . . . . . . 14 setvar o
38	37	cv 1482	. . . . . . . . . . . . 13 class o
39		vp	. . . . . . . . . . . . . 14 setvar p
40	39	cv 1482	. . . . . . . . . . . . 13 class p
41	36, 38, 40	cotp 4185	. . . . . . . . . . . 12 class <. m , o , p >.
42		cmax 31362	. . . . . . . . . . . . 13 class mAx
43	6, 42	cfv 5888	. . . . . . . . . . . 12 class (mAx ` t )
44	41, 43	wcel 1990	. . . . . . . . . . 11 wff <. m , o , p >. e. (mAx ` t )
45		vx	. . . . . . . . . . . . . . . . . 18 setvar x
46	45	cv 1482	. . . . . . . . . . . . . . . . 17 class x
47		vy	. . . . . . . . . . . . . . . . . 18 setvar y
48	47	cv 1482	. . . . . . . . . . . . . . . . 17 class y
49	46, 48, 36	wbr 4653	. . . . . . . . . . . . . . . 16 wff x m y
50	46, 23	cfv 5888	. . . . . . . . . . . . . . . . . . . 20 class ( (mVH ` t ) ` x )
51		vs	. . . . . . . . . . . . . . . . . . . . 21 setvar s
52	51	cv 1482	. . . . . . . . . . . . . . . . . . . 20 class s
53	50, 52	cfv 5888	. . . . . . . . . . . . . . . . . . 19 class ( s ` ( (mVH ` t ) ` x ) )
54		cmvrs 31366	. . . . . . . . . . . . . . . . . . . 20 class mVars
55	6, 54	cfv 5888	. . . . . . . . . . . . . . . . . . 19 class (mVars ` t )
56	53, 55	cfv 5888	. . . . . . . . . . . . . . . . . 18 class ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` x ) ) )
57	48, 23	cfv 5888	. . . . . . . . . . . . . . . . . . . 20 class ( (mVH ` t ) ` y )
58	57, 52	cfv 5888	. . . . . . . . . . . . . . . . . . 19 class ( s ` ( (mVH ` t ) ` y ) )
59	58, 55	cfv 5888	. . . . . . . . . . . . . . . . . 18 class ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` y ) ) )
60	56, 59	cxp 5112	. . . . . . . . . . . . . . . . 17 class ( ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` x ) ) ) X. ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` y ) ) ) )
61	60, 26	wss 3574	. . . . . . . . . . . . . . . 16 wff ( ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` x ) ) ) X. ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` y ) ) ) ) C_ d
62	49, 61	wi 4	. . . . . . . . . . . . . . 15 wff ( x m y -> ( ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` x ) ) ) X. ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` y ) ) ) ) C_ d )
63	62, 47	wal 1481	. . . . . . . . . . . . . 14 wff A. y ( x m y -> ( ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` x ) ) ) X. ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` y ) ) ) ) C_ d )
64	63, 45	wal 1481	. . . . . . . . . . . . 13 wff A. x A. y ( x m y -> ( ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` x ) ) ) X. ( (mVars ` t ) ` ( s ` ( (mVH ` t ) ` y ) ) ) ) C_ d )
65	40, 52	cfv 5888	. . . . . . . . . . . . . . . 16 class ( s ` p )
66	65	csn 4177	. . . . . . . . . . . . . . 15 class { ( s ` p ) }
67	40	csn 4177	. . . . . . . . . . . . . . . . . . . . 21 class { p }
68	38, 67	cun 3572	. . . . . . . . . . . . . . . . . . . 20 class ( o u. { p } )
69	55, 68	cima 5117	. . . . . . . . . . . . . . . . . . 19 class ( (mVars ` t ) " ( o u. { p } ) )
70	69	cuni 4436	. . . . . . . . . . . . . . . . . 18 class U. ( (mVars ` t ) " ( o u. { p } ) )
71	23, 70	cima 5117	. . . . . . . . . . . . . . . . 17 class ( (mVH ` t ) " U. ( (mVars ` t ) " ( o u. { p } ) ) )
72	38, 71	cun 3572	. . . . . . . . . . . . . . . 16 class ( o u. ( (mVH ` t ) " U. ( (mVars ` t ) " ( o u. { p } ) ) ) )
73	14, 52	cfv 5888	. . . . . . . . . . . . . . . . . 18 class ( s ` e )
74	73	csn 4177	. . . . . . . . . . . . . . . . 17 class { ( s ` e ) }
75	20, 74	cima 5117	. . . . . . . . . . . . . . . 16 class ( r " { ( s ` e ) } )
76	13, 72, 75	cixp 7908	. . . . . . . . . . . . . . 15 class X_ e e. ( o u. ( (mVH ` t ) " U. ( (mVars ` t ) " ( o u. { p } ) ) ) ) ( r " { ( s ` e ) } )
77	66, 76	cxp 5112	. . . . . . . . . . . . . 14 class ( { ( s ` p ) } X. X_ e e. ( o u. ( (mVH ` t ) " U. ( (mVars ` t ) " ( o u. { p } ) ) ) ) ( r " { ( s ` e ) } ) )
78	77, 20	wss 3574	. . . . . . . . . . . . 13 wff ( { ( s ` p ) } X. X_ e e. ( o u. ( (mVH ` t ) " U. ( (mVars ` t ) " ( o u. { p } ) ) ) ) ( r " { ( s ` e ) } ) ) C_ r
79	64, 78	wi 4	. . . . . . . . . . . 12 wff ( 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 )
80		cmsub 31368	. . . . . . . . . . . . . 14 class mSubst
81	6, 80	cfv 5888	. . . . . . . . . . . . 13 class (mSubst ` t )
82	81	crn 5115	. . . . . . . . . . . 12 class ran (mSubst ` t )
83	79, 51, 82	wral 2912	. . . . . . . . . . 11 wff 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	44, 83	wi 4	. . . . . . . . . 10 wff ( <. 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, 39	wal 1481	. . . . . . . . 9 wff 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, 37	wal 1481	. . . . . . . 8 wff 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	86, 35	wal 1481	. . . . . . 7 wff 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	25, 34, 87	w3a 1037	. . . . . 6 wff ( 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, 19	cab 2608	. . . . 5 class { 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	89	cint 4475	. . . 4 class |^| { 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	4, 5, 9, 12, 90	cmpt2 6652	. . 3 class ( 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	2, 3, 91	cmpt 4729	. 2 class ( 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 ) ) ) } ) )
93	1, 92	wceq 1483	1 wff 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 ) ) ) } ) )

This definition is referenced by: (None)