Metamath Proof Explorer


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 Top | y 𝒫 j j = y z 𝒫 j A z Ref y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 ccref class CovHasRef A
2 vj setvar j
3 ctop class Top
4 vy setvar y
5 2 cv setvar j
6 5 cpw class 𝒫 j
7 5 cuni class j
8 4 cv setvar y
9 8 cuni class y
10 7 9 wceq wff j = y
11 vz setvar z
12 6 0 cin class 𝒫 j A
13 11 cv setvar z
14 cref class Ref
15 13 8 14 wbr wff z Ref y
16 15 11 12 wrex wff z 𝒫 j A z Ref y
17 10 16 wi wff j = y z 𝒫 j A z Ref y
18 17 4 6 wral wff y 𝒫 j j = y z 𝒫 j A z Ref y
19 18 2 3 crab class j Top | y 𝒫 j j = y z 𝒫 j A z Ref y
20 1 19 wceq wff CovHasRef A = j Top | y 𝒫 j j = y z 𝒫 j A z Ref y