Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Topology
Open cover refinement property
df-cref
Metamath Proof Explorer
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