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 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	ccref	⊢ CovHasRef 𝐴
2		vj	⊢ 𝑗
3		ctop	⊢ Top
4		vy	⊢ 𝑦
5	2	cv	⊢ 𝑗
6	5	cpw	⊢ 𝒫 𝑗
7	5	cuni	⊢ ∪ 𝑗
8	4	cv	⊢ 𝑦
9	8	cuni	⊢ ∪ 𝑦
10	7 9	wceq	⊢ ∪ 𝑗 = ∪ 𝑦
11		vz	⊢ 𝑧
12	6 0	cin	⊢ ( 𝒫 𝑗 ∩ 𝐴 )
13	11	cv	⊢ 𝑧
14		cref	⊢ Ref
15	13 8 14	wbr	⊢ 𝑧 Ref 𝑦
16	15 11 12	wrex	⊢ ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦
17	10 16	wi	⊢ ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 )
18	17 4 6	wral	⊢ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 )
19	18 2 3	crab	⊢ { 𝑗 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) }
20	1 19	wceq	⊢ CovHasRef 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) }