Definition df-mtree

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

	Ref	Expression
Assertion	df-mtree	$$⊢\mathrm{mTree}=\left(t\in \mathrm{V}⟼\left(d\in 𝒫\mathrm{mDV}\left(t\right),h\in 𝒫\mathrm{mEx}\left(t\right)⟼\bigcap \left\{r|\left(\forall e\in \mathrm{ran}\mathrm{mVH}\left(t\right)er⟨\mathrm{m0St}\left(e\right),\varnothing ⟩\wedge \forall e\in her⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩\wedge \forall m\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)\right)\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmtree	$$class\mathrm{mTree}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		vd	$$setvard$$
4		cmdv	$$class\mathrm{mDV}$$
5	1	cv	$$setvart$$
6	5 4	cfv	$$class\mathrm{mDV}\left(t\right)$$
7	6	cpw	$$class𝒫\mathrm{mDV}\left(t\right)$$
8		vh	$$setvarh$$
9		cmex	$$class\mathrm{mEx}$$
10	5 9	cfv	$$class\mathrm{mEx}\left(t\right)$$
11	10	cpw	$$class𝒫\mathrm{mEx}\left(t\right)$$
12		vr	$$setvarr$$
13		ve	$$setvare$$
14		cmvh	$$class\mathrm{mVH}$$
15	5 14	cfv	$$class\mathrm{mVH}\left(t\right)$$
16	15	crn	$$class\mathrm{ran}\mathrm{mVH}\left(t\right)$$
17	13	cv	$$setvare$$
18	12	cv	$$setvarr$$
19		cm0s	$$class\mathrm{m0St}$$
20	17 19	cfv	$$class\mathrm{m0St}\left(e\right)$$
21		c0	$$class\varnothing$$
22	20 21	cop	$$class⟨\mathrm{m0St}\left(e\right),\varnothing ⟩$$
23	17 22 18	wbr	$$wffer⟨\mathrm{m0St}\left(e\right),\varnothing ⟩$$
24	23 13 16	wral	$$wff\forall e\in \mathrm{ran}\mathrm{mVH}\left(t\right)er⟨\mathrm{m0St}\left(e\right),\varnothing ⟩$$
25	8	cv	$$setvarh$$
26		cmsr	$$class\mathrm{mStRed}$$
27	5 26	cfv	$$class\mathrm{mStRed}\left(t\right)$$
28	3	cv	$$setvard$$
29	28 25 17	cotp	$$class⟨d,h,e⟩$$
30	29 27	cfv	$$class\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right)$$
31	30 21	cop	$$class⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩$$
32	17 31 18	wbr	$$wffer⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩$$
33	32 13 25	wral	$$wff\forall e\in her⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩$$
34		vm	$$setvarm$$
35		vo	$$setvaro$$
36		vp	$$setvarp$$
37	34	cv	$$setvarm$$
38	35	cv	$$setvaro$$
39	36	cv	$$setvarp$$
40	37 38 39	cotp	$$class⟨m,o,p⟩$$
41		cmax	$$class\mathrm{mAx}$$
42	5 41	cfv	$$class\mathrm{mAx}\left(t\right)$$
43	40 42	wcel	$$wff⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)$$
44		vs	$$setvars$$
45		cmsub	$$class\mathrm{mSubst}$$
46	5 45	cfv	$$class\mathrm{mSubst}\left(t\right)$$
47	46	crn	$$class\mathrm{ran}\mathrm{mSubst}\left(t\right)$$
48		vx	$$setvarx$$
49		vy	$$setvary$$
50	48	cv	$$setvarx$$
51	49	cv	$$setvary$$
52	50 51 37	wbr	$$wffxmy$$
53		cmvrs	$$class\mathrm{mVars}$$
54	5 53	cfv	$$class\mathrm{mVars}\left(t\right)$$
55	44	cv	$$setvars$$
56	50 15	cfv	$$class\mathrm{mVH}\left(t\right)\left(x\right)$$
57	56 55	cfv	$$classs\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)$$
58	57 54	cfv	$$class\mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)$$
59	51 15	cfv	$$class\mathrm{mVH}\left(t\right)\left(y\right)$$
60	59 55	cfv	$$classs\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)$$
61	60 54	cfv	$$class\mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)$$
62	58 61	cxp	$$class\left(\mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\right)$$
63	62 28	wss	$$wff\mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d$$
64	52 63	wi	$$wff\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)$$
65	64 49	wal	$$wff\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)$$
66	65 48	wal	$$wff\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)$$
67	39 55	cfv	$$classs\left(p\right)$$
68	67	csn	$$class\left\{s\left(p\right)\right\}$$
69	39	csn	$$class\left\{p\right\}$$
70	38 69	cun	$$class\left(o\cup \left\{p\right\}\right)$$
71	54 70	cima	$$class\mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]$$
72	71	cuni	$$class\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]$$
73	15 72	cima	$$class\mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]$$
74	38 73	cun	$$class\left(o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]\right)$$
75	17 55	cfv	$$classs\left(e\right)$$
76	75	csn	$$class\left\{s\left(e\right)\right\}$$
77	18 76	cima	$$classr\left[\left\{s\left(e\right)\right\}\right]$$
78	13 74 77	cixp	$$class\underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]$$
79	68 78	cxp	$$class\left(\left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\right)$$
80	79 18	wss	$$wff\left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r$$
81	66 80	wi	$$wff\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)$$
82	81 44 47	wral	$$wff\forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)$$
83	43 82	wi	$$wff\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)$$
84	83 36	wal	$$wff\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)$$
85	84 35	wal	$$wff\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)$$
86	85 34	wal	$$wff\forall m\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)$$
87	24 33 86	w3a	$$wff\left(\forall e\in \mathrm{ran}\mathrm{mVH}\left(t\right)er⟨\mathrm{m0St}\left(e\right),\varnothing ⟩\wedge \forall e\in her⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩\wedge \forall m\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)\right)$$
88	87 12	cab	$$class\left\{r|\left(\forall e\in \mathrm{ran}\mathrm{mVH}\left(t\right)er⟨\mathrm{m0St}\left(e\right),\varnothing ⟩\wedge \forall e\in her⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩\wedge \forall m\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)\right)\right\}$$
89	88	cint	$$class\bigcap \left\{r|\left(\forall e\in \mathrm{ran}\mathrm{mVH}\left(t\right)er⟨\mathrm{m0St}\left(e\right),\varnothing ⟩\wedge \forall e\in her⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩\wedge \forall m\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)\right)\right\}$$
90	3 8 7 11 89	cmpo	$$class\left(d\in 𝒫\mathrm{mDV}\left(t\right),h\in 𝒫\mathrm{mEx}\left(t\right)⟼\bigcap \left\{r|\left(\forall e\in \mathrm{ran}\mathrm{mVH}\left(t\right)er⟨\mathrm{m0St}\left(e\right),\varnothing ⟩\wedge \forall e\in her⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩\wedge \forall m\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)\right)\right\}\right)$$
91	1 2 90	cmpt	$$class\left(t\in \mathrm{V}⟼\left(d\in 𝒫\mathrm{mDV}\left(t\right),h\in 𝒫\mathrm{mEx}\left(t\right)⟼\bigcap \left\{r|\left(\forall e\in \mathrm{ran}\mathrm{mVH}\left(t\right)er⟨\mathrm{m0St}\left(e\right),\varnothing ⟩\wedge \forall e\in her⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩\wedge \forall m\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)\right)\right\}\right)\right)$$
92	0 91	wceq	$$wff\mathrm{mTree}=\left(t\in \mathrm{V}⟼\left(d\in 𝒫\mathrm{mDV}\left(t\right),h\in 𝒫\mathrm{mEx}\left(t\right)⟼\bigcap \left\{r|\left(\forall e\in \mathrm{ran}\mathrm{mVH}\left(t\right)er⟨\mathrm{m0St}\left(e\right),\varnothing ⟩\wedge \forall e\in her⟨\mathrm{mStRed}\left(t\right)\left(⟨d,h,e⟩\right),\varnothing ⟩\wedge \forall m\forall o\forall p\left(⟨m,o,p⟩\in \mathrm{mAx}\left(t\right)\to \forall s\in \mathrm{ran}\mathrm{mSubst}\left(t\right)\left(\forall x\forall y\left(xmy\to \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(x\right)\right)\right)\times \mathrm{mVars}\left(t\right)\left(s\left(\mathrm{mVH}\left(t\right)\left(y\right)\right)\right)\subseteq d\right)\to \left\{s\left(p\right)\right\}\times \underset{e\in o\cup \mathrm{mVH}\left(t\right)\left[\bigcup \mathrm{mVars}\left(t\right)\left[o\cup \left\{p\right\}\right]\right]}{⨉}r\left[\left\{s\left(e\right)\right\}\right]\subseteq r\right)\right)\right)\right\}\right)\right)$$