Users' Mathboxes 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 29040
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 29039 . 2 class CovHasRef𝐴
3 vj . . . . . . . 8 setvar 𝑗
43cv 1473 . . . . . . 7 class 𝑗
54cuni 4362 . . . . . 6 class 𝑗
6 vy . . . . . . . 8 setvar 𝑦
76cv 1473 . . . . . . 7 class 𝑦
87cuni 4362 . . . . . 6 class 𝑦
95, 8wceq 1474 . . . . 5 wff 𝑗 = 𝑦
10 vz . . . . . . . 8 setvar 𝑧
1110cv 1473 . . . . . . 7 class 𝑧
12 cref 21053 . . . . . . 7 class Ref
1311, 7, 12wbr 4573 . . . . . 6 wff 𝑧Ref𝑦
144cpw 4103 . . . . . . 7 class 𝒫 𝑗
1514, 1cin 3534 . . . . . 6 class (𝒫 𝑗𝐴)
1613, 10, 15wrex 2892 . . . . 5 wff 𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦
179, 16wi 4 . . . 4 wff ( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦)
1817, 6, 14wral 2891 . . 3 wff 𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦)
19 ctop 20455 . . 3 class Top
2018, 3, 19crab 2895 . 2 class {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦)}
212, 20wceq 1474 1 wff CovHasRef𝐴 = {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗𝐴)𝑧Ref𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  iscref  29041  crefeq  29042
  Copyright terms: Public domain W3C validator