Metamath Proof Explorer

Theorem creftop

Description: A space where every open cover has an A refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020)

Ref Expression
Assertion creftop 
|- ( J e. CovHasRef A -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 iscref 
 |-  ( J e. CovHasRef A <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) ) )
3 2 simplbi 
 |-  ( J e. CovHasRef A -> J e. Top )