Definition df-cref 31695

Description: Define a statement "every open cover has an 𝐴 refinement" , where 𝐴 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𝐴 = {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗(∪ 𝑗 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦)}

Distinct variable group:   𝐴,𝑗,𝑦,𝑧

Detailed syntax breakdown of Definition df-cref

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	ccref 31694	. 2 class CovHasRef𝐴
3		vj	. . . . . . . 8 setvar 𝑗
4	3	cv 1538	. . . . . . 7 class 𝑗
5	4	cuni 4836	. . . . . 6 class ∪ 𝑗
6		vy	. . . . . . . 8 setvar 𝑦
7	6	cv 1538	. . . . . . 7 class 𝑦
8	7	cuni 4836	. . . . . 6 class ∪ 𝑦
9	5, 8	wceq 1539	. . . . 5 wff ∪ 𝑗 = ∪ 𝑦
10		vz	. . . . . . . 8 setvar 𝑧
11	10	cv 1538	. . . . . . 7 class 𝑧
12		cref 22561	. . . . . . 7 class Ref
13	11, 7, 12	wbr 5070	. . . . . 6 wff 𝑧Ref𝑦
14	4	cpw 4530	. . . . . . 7 class 𝒫 𝑗
15	14, 1	cin 3882	. . . . . 6 class (𝒫 𝑗 ∩ 𝐴)
16	13, 10, 15	wrex 3064	. . . . 5 wff ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦
17	9, 16	wi 4	. . . 4 wff (∪ 𝑗 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦)
18	17, 6, 14	wral 3063	. . 3 wff ∀𝑦 ∈ 𝒫 𝑗(∪ 𝑗 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦)
19		ctop 21950	. . 3 class Top
20	18, 3, 19	crab 3067	. 2 class {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗(∪ 𝑗 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦)}
21	2, 20	wceq 1539	1 wff CovHasRef𝐴 = {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗(∪ 𝑗 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦)}

This definition is referenced by:  iscref  31696  crefeq  31697