Theorem iscref

Description: The property that every open cover has an A refinement for the topological space J . (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Hypothesis	iscref.x	$$⊢X=\bigcup J$$
Assertion	iscref	$$⊢J\in \mathrm{CovHasRef}A\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall y\in 𝒫J\left(X=\bigcup y\to \exists z\in \left(𝒫J\cap A\right)z\mathrm{Ref}y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscref.x	$$⊢X=\bigcup J$$
2		pweq	$$⊢j=J\to 𝒫j=𝒫J$$
3		unieq	$$⊢j=J\to \bigcup j=\bigcup J$$
4	3 1	eqtr4di	$$⊢j=J\to \bigcup j=X$$
5	4	eqeq1d	$$⊢j=J\to \left(\bigcup j=\bigcup y\leftrightarrow X=\bigcup y\right)$$
6	2	ineq1d	$$⊢j=J\to 𝒫j\cap A=𝒫J\cap A$$
7	6	rexeqdv	$$⊢j=J\to \left(\exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\leftrightarrow \exists z\in \left(𝒫J\cap A\right)z\mathrm{Ref}y\right)$$
8	5 7	imbi12d	$$⊢j=J\to \left(\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)\leftrightarrow \left(X=\bigcup y\to \exists z\in \left(𝒫J\cap A\right)z\mathrm{Ref}y\right)\right)$$
9	2 8	raleqbidv	$$⊢j=J\to \left(\forall y\in 𝒫j\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)\leftrightarrow \forall y\in 𝒫J\left(X=\bigcup y\to \exists z\in \left(𝒫J\cap A\right)z\mathrm{Ref}y\right)\right)$$
10		df-cref	$$⊢\mathrm{CovHasRef}A=\left\{j\in \mathrm{Top}|\forall y\in 𝒫j\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)\right\}$$
11	9 10	elrab2	$$⊢J\in \mathrm{CovHasRef}A\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall y\in 𝒫J\left(X=\bigcup y\to \exists z\in \left(𝒫J\cap A\right)z\mathrm{Ref}y\right)\right)$$