Theorem crefeq

Description: Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Assertion	crefeq	$$⊢A=B\to \mathrm{CovHasRef}A=\mathrm{CovHasRef}B$$

Proof

Step	Hyp	Ref	Expression
1		ineq2	$$⊢A=B\to 𝒫j\cap A=𝒫j\cap B$$
2	1	rexeqdv	$$⊢A=B\to \left(\exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\leftrightarrow \exists z\in \left(𝒫j\cap B\right)z\mathrm{Ref}y\right)$$
3	2	imbi2d	$$⊢A=B\to \left(\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap A\right)z\mathrm{Ref}y\right)\leftrightarrow \left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap B\right)z\mathrm{Ref}y\right)\right)$$
4	3	ralbidv	$$⊢A=B\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(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap B\right)z\mathrm{Ref}y\right)\right)$$
5	4	rabbidv	$$⊢A=B\to \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\}=\left\{j\in \mathrm{Top}|\forall y\in 𝒫j\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap B\right)z\mathrm{Ref}y\right)\right\}$$
6		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\}$$
7		df-cref	$$⊢\mathrm{CovHasRef}B=\left\{j\in \mathrm{Top}|\forall y\in 𝒫j\left(\bigcup j=\bigcup y\to \exists z\in \left(𝒫j\cap B\right)z\mathrm{Ref}y\right)\right\}$$
8	5 6 7	3eqtr4g	$$⊢A=B\to \mathrm{CovHasRef}A=\mathrm{CovHasRef}B$$