Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cref Structured version   Visualization version   GIF version

Definition df-cref 30244
 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
StepHypRef Expression
1 cA . . 3 class 𝐴
21ccref 30243 . 2 class CovHasRef𝐴
3 vj . . . . . . . 8 setvar 𝑗
43cv 1629 . . . . . . 7 class 𝑗
54cuni 4572 . . . . . 6 class 𝑗
6 vy . . . . . . . 8 setvar 𝑦
76cv 1629 . . . . . . 7 class 𝑦
87cuni 4572 . . . . . 6 class 𝑦
95, 8wceq 1630 . . . . 5 wff 𝑗 = 𝑦
10 vz . . . . . . . 8 setvar 𝑧
1110cv 1629 . . . . . . 7 class 𝑧
12 cref 21525 . . . . . . 7 class Ref
1311, 7, 12wbr 4784 . . . . . 6 wff 𝑧Ref𝑦
144cpw 4295 . . . . . . 7 class 𝒫 𝑗
1514, 1cin 3720 . . . . . 6 class (𝒫 𝑗𝐴)
1613, 10, 15wrex 3061 . . . . 5 wff 𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦
179, 16wi 4 . . . 4 wff ( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦)
1817, 6, 14wral 3060 . . 3 wff 𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦)
19 ctop 20917 . . 3 class Top
2018, 3, 19crab 3064 . 2 class {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦)}
212, 20wceq 1630 1 wff CovHasRef𝐴 = {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦)}
 Colors of variables: wff setvar class This definition is referenced by:  iscref  30245  crefeq  30246
 Copyright terms: Public domain W3C validator