Definition df-mtree 34587

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

Assertion

Ref	Expression
df-mtree	⊢ mTree = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩ ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)))}))

Distinct variable group:   𝑒,𝑑,ℎ,𝑚,𝑜,𝑝,𝑟,𝑠,𝑡,𝑥,𝑦

Detailed syntax breakdown of Definition df-mtree

Step	Hyp	Ref	Expression
1		cmtree 34577	. 2 class mTree
2		vt	. . 3 setvar 𝑡
3		cvv 3474	. . 3 class V
4		vd	. . . 4 setvar 𝑑
5		vh	. . . 4 setvar ℎ
6	2	cv 1540	. . . . . 6 class 𝑡
7		cmdv 34454	. . . . . 6 class mDV
8	6, 7	cfv 6543	. . . . 5 class (mDV‘𝑡)
9	8	cpw 4602	. . . 4 class 𝒫 (mDV‘𝑡)
10		cmex 34453	. . . . . 6 class mEx
11	6, 10	cfv 6543	. . . . 5 class (mEx‘𝑡)
12	11	cpw 4602	. . . 4 class 𝒫 (mEx‘𝑡)
13		ve	. . . . . . . . . 10 setvar 𝑒
14	13	cv 1540	. . . . . . . . 9 class 𝑒
15		cm0s 34571	. . . . . . . . . . 11 class m0St
16	14, 15	cfv 6543	. . . . . . . . . 10 class (m0St‘𝑒)
17		c0 4322	. . . . . . . . . 10 class ∅
18	16, 17	cop 4634	. . . . . . . . 9 class ⟨(m0St‘𝑒), ∅⟩
19		vr	. . . . . . . . . 10 setvar 𝑟
20	19	cv 1540	. . . . . . . . 9 class 𝑟
21	14, 18, 20	wbr 5148	. . . . . . . 8 wff 𝑒𝑟⟨(m0St‘𝑒), ∅⟩
22		cmvh 34458	. . . . . . . . . 10 class mVH
23	6, 22	cfv 6543	. . . . . . . . 9 class (mVH‘𝑡)
24	23	crn 5677	. . . . . . . 8 class ran (mVH‘𝑡)
25	21, 13, 24	wral 3061	. . . . . . 7 wff ∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩
26	4	cv 1540	. . . . . . . . . . . 12 class 𝑑
27	5	cv 1540	. . . . . . . . . . . 12 class ℎ
28	26, 27, 14	cotp 4636	. . . . . . . . . . 11 class ⟨𝑑, ℎ, 𝑒⟩
29		cmsr 34460	. . . . . . . . . . . 12 class mStRed
30	6, 29	cfv 6543	. . . . . . . . . . 11 class (mStRed‘𝑡)
31	28, 30	cfv 6543	. . . . . . . . . 10 class ((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩)
32	31, 17	cop 4634	. . . . . . . . 9 class ⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩
33	14, 32, 20	wbr 5148	. . . . . . . 8 wff 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩
34	33, 13, 27	wral 3061	. . . . . . 7 wff ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩
35		vm	. . . . . . . . . . . . . 14 setvar 𝑚
36	35	cv 1540	. . . . . . . . . . . . 13 class 𝑚
37		vo	. . . . . . . . . . . . . 14 setvar 𝑜
38	37	cv 1540	. . . . . . . . . . . . 13 class 𝑜
39		vp	. . . . . . . . . . . . . 14 setvar 𝑝
40	39	cv 1540	. . . . . . . . . . . . 13 class 𝑝
41	36, 38, 40	cotp 4636	. . . . . . . . . . . 12 class ⟨𝑚, 𝑜, 𝑝⟩
42		cmax 34451	. . . . . . . . . . . . 13 class mAx
43	6, 42	cfv 6543	. . . . . . . . . . . 12 class (mAx‘𝑡)
44	41, 43	wcel 2106	. . . . . . . . . . 11 wff ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡)
45		vx	. . . . . . . . . . . . . . . . . 18 setvar 𝑥
46	45	cv 1540	. . . . . . . . . . . . . . . . 17 class 𝑥
47		vy	. . . . . . . . . . . . . . . . . 18 setvar 𝑦
48	47	cv 1540	. . . . . . . . . . . . . . . . 17 class 𝑦
49	46, 48, 36	wbr 5148	. . . . . . . . . . . . . . . 16 wff 𝑥𝑚𝑦
50	46, 23	cfv 6543	. . . . . . . . . . . . . . . . . . . 20 class ((mVH‘𝑡)‘𝑥)
51		vs	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑠
52	51	cv 1540	. . . . . . . . . . . . . . . . . . . 20 class 𝑠
53	50, 52	cfv 6543	. . . . . . . . . . . . . . . . . . 19 class (𝑠‘((mVH‘𝑡)‘𝑥))
54		cmvrs 34455	. . . . . . . . . . . . . . . . . . . 20 class mVars
55	6, 54	cfv 6543	. . . . . . . . . . . . . . . . . . 19 class (mVars‘𝑡)
56	53, 55	cfv 6543	. . . . . . . . . . . . . . . . . 18 class ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥)))
57	48, 23	cfv 6543	. . . . . . . . . . . . . . . . . . . 20 class ((mVH‘𝑡)‘𝑦)
58	57, 52	cfv 6543	. . . . . . . . . . . . . . . . . . 19 class (𝑠‘((mVH‘𝑡)‘𝑦))
59	58, 55	cfv 6543	. . . . . . . . . . . . . . . . . 18 class ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))
60	56, 59	cxp 5674	. . . . . . . . . . . . . . . . 17 class (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦))))
61	60, 26	wss 3948	. . . . . . . . . . . . . . . 16 wff (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑
62	49, 61	wi 4	. . . . . . . . . . . . . . 15 wff (𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
63	62, 47	wal 1539	. . . . . . . . . . . . . 14 wff ∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
64	63, 45	wal 1539	. . . . . . . . . . . . 13 wff ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
65	40, 52	cfv 6543	. . . . . . . . . . . . . . . 16 class (𝑠‘𝑝)
66	65	csn 4628	. . . . . . . . . . . . . . 15 class {(𝑠‘𝑝)}
67	40	csn 4628	. . . . . . . . . . . . . . . . . . . . 21 class {𝑝}
68	38, 67	cun 3946	. . . . . . . . . . . . . . . . . . . 20 class (𝑜 ∪ {𝑝})
69	55, 68	cima 5679	. . . . . . . . . . . . . . . . . . 19 class ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))
70	69	cuni 4908	. . . . . . . . . . . . . . . . . 18 class ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))
71	23, 70	cima 5679	. . . . . . . . . . . . . . . . 17 class ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝})))
72	38, 71	cun 3946	. . . . . . . . . . . . . . . 16 class (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))
73	14, 52	cfv 6543	. . . . . . . . . . . . . . . . . 18 class (𝑠‘𝑒)
74	73	csn 4628	. . . . . . . . . . . . . . . . 17 class {(𝑠‘𝑒)}
75	20, 74	cima 5679	. . . . . . . . . . . . . . . 16 class (𝑟 “ {(𝑠‘𝑒)})
76	13, 72, 75	cixp 8890	. . . . . . . . . . . . . . 15 class X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})
77	66, 76	cxp 5674	. . . . . . . . . . . . . 14 class ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)}))
78	77, 20	wss 3948	. . . . . . . . . . . . 13 wff ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟
79	64, 78	wi 4	. . . . . . . . . . . 12 wff (∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)
80		cmsub 34457	. . . . . . . . . . . . . 14 class mSubst
81	6, 80	cfv 6543	. . . . . . . . . . . . 13 class (mSubst‘𝑡)
82	81	crn 5677	. . . . . . . . . . . 12 class ran (mSubst‘𝑡)
83	79, 51, 82	wral 3061	. . . . . . . . . . 11 wff ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)
84	44, 83	wi 4	. . . . . . . . . 10 wff (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟))
85	84, 39	wal 1539	. . . . . . . . 9 wff ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟))
86	85, 37	wal 1539	. . . . . . . 8 wff ∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟))
87	86, 35	wal 1539	. . . . . . 7 wff ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟))
88	25, 34, 87	w3a 1087	. . . . . 6 wff (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩ ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)))
89	88, 19	cab 2709	. . . . 5 class {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩ ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)))}
90	89	cint 4950	. . . 4 class ∩ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩ ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)))}
91	4, 5, 9, 12, 90	cmpo 7410	. . 3 class (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩ ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)))})
92	2, 3, 91	cmpt 5231	. 2 class (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩ ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)))}))
93	1, 92	wceq 1541	1 wff mTree = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩ ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)))}))

This definition is referenced by: (None)