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	|- CovHasRef A = { j e. Top | A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	ccref	|- CovHasRef A
2		vj	|- j
3		ctop	|- Top
4		vy	|- y
5	2	cv	|- j
6	5	cpw	|- ~P j
7	5	cuni	|- U. j
8	4	cv	|- y
9	8	cuni	|- U. y
10	7 9	wceq	|- U. j = U. y
11		vz	|- z
12	6 0	cin	|- ( ~P j i^i A )
13	11	cv	|- z
14		cref	|- Ref
15	13 8 14	wbr	|- z Ref y
16	15 11 12	wrex	|- E. z e. ( ~P j i^i A ) z Ref y
17	10 16	wi	|- ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y )
18	17 4 6	wral	|- A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y )
19	18 2 3	crab	|- { j e. Top | A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) }
20	1 19	wceq	|- CovHasRef A = { j e. Top | A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) }