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	⊢ ( 𝐽 ∈ CovHasRef 𝐴 → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	iscref	⊢ ( 𝐽 ∈ CovHasRef 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) ) )
3	2	simplbi	⊢ ( 𝐽 ∈ CovHasRef 𝐴 → 𝐽 ∈ Top )