Definition df-cref 29910

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

Assertion

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

Distinct variable group:   A, j, y, z

Detailed syntax breakdown of Definition df-cref

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	ccref 29909	. 2 class CovHasRef A
3		vj	. . . . . . . 8 setvar j
4	3	cv 1482	. . . . . . 7 class j
5	4	cuni 4436	. . . . . 6 class U. j
6		vy	. . . . . . . 8 setvar y
7	6	cv 1482	. . . . . . 7 class y
8	7	cuni 4436	. . . . . 6 class U. y
9	5, 8	wceq 1483	. . . . 5 wff U. j = U. y
10		vz	. . . . . . . 8 setvar z
11	10	cv 1482	. . . . . . 7 class z
12		cref 21305	. . . . . . 7 class Ref
13	11, 7, 12	wbr 4653	. . . . . 6 wff z Ref y
14	4	cpw 4158	. . . . . . 7 class ~P j
15	14, 1	cin 3573	. . . . . 6 class ( ~P j i^i A )
16	13, 10, 15	wrex 2913	. . . . 5 wff E. z e. ( ~P j i^i A ) z Ref y
17	9, 16	wi 4	. . . 4 wff ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y )
18	17, 6, 14	wral 2912	. . 3 wff A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y )
19		ctop 20698	. . 3 class Top
20	18, 3, 19	crab 2916	. 2 class { j e. Top | A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) }
21	2, 20	wceq 1483	1 wff 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 ) }

This definition is referenced by:  iscref  29911  crefeq  29912