Definition df-cref

Description: Define a statement "every open cover has an A refinement" , where A is a property for refinements like "finite", "countable", "point finite" or "locally finite". (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Assertion	df-cref	$$⊢\mathrm{CovHasRef}A=\left\{j\in \mathrm{Top}|\forall y\in 𝒫j\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	ccref	$$class\mathrm{CovHasRef}A$$
2		vj	$$setvarj$$
3		ctop	$$class\mathrm{Top}$$
4		vy	$$setvary$$
5	2	cv	$$setvarj$$
6	5	cpw	$$class𝒫j$$
7	5	cuni	$$class\bigcup j$$
8	4	cv	$$setvary$$
9	8	cuni	$$class\bigcup y$$
10	7 9	wceq	$$wff\bigcup j=\bigcup y$$
11		vz	$$setvarz$$
12	6 0	cin	$$class\left(𝒫j\cap A\right)$$
13	11	cv	$$setvarz$$
14		cref	$$class\mathrm{Ref}$$
15	13 8 14	wbr	$$wffz\mathrm{Ref}y$$
16	15 11 12	wrex	$$wff\exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y$$
17	10 16	wi	$$wff\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)$$
18	17 4 6	wral	$$wff\forall y\in 𝒫j\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)$$
19	18 2 3	crab	$$class\left\{j\in \mathrm{Top}|\forall y\in 𝒫j\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)\right\}$$
20	1 19	wceq	$$wff\mathrm{CovHasRef}A=\left\{j\in \mathrm{Top}|\forall y\in 𝒫j\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)\right\}$$