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\in \mathrm{CovHasRef}A\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	iscref	$$⊢J\in \mathrm{CovHasRef}A\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall y\in 𝒫J\left(\bigcup J=\bigcup y\to \exists z\in \left(𝒫J\cap A\right)z\mathrm{Ref}y\right)\right)$$
3	2	simplbi	$$⊢J\in \mathrm{CovHasRef}A\to J\in \mathrm{Top}$$