# Metamath Proof Explorer

## 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)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}↔\exists {z}\in \left(𝒫{j}\cap {B}\right)\phantom{\rule{.4em}{0ex}}{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)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)↔\left(\bigcup {j}=\bigcup {y}\to \exists {z}\in \left(𝒫{j}\cap {B}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
4 3 ralbidv ${⊢}{A}={B}\to \left(\forall {y}\in 𝒫{j}\phantom{\rule{.4em}{0ex}}\left(\bigcup {j}=\bigcup {y}\to \exists {z}\in \left(𝒫{j}\cap {A}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)↔\forall {y}\in 𝒫{j}\phantom{\rule{.4em}{0ex}}\left(\bigcup {j}=\bigcup {y}\to \exists {z}\in \left(𝒫{j}\cap {B}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
5 4 rabbidv ${⊢}{A}={B}\to \left\{{j}\in \mathrm{Top}|\forall {y}\in 𝒫{j}\phantom{\rule{.4em}{0ex}}\left(\bigcup {j}=\bigcup {y}\to \exists {z}\in \left(𝒫{j}\cap {A}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right\}=\left\{{j}\in \mathrm{Top}|\forall {y}\in 𝒫{j}\phantom{\rule{.4em}{0ex}}\left(\bigcup {j}=\bigcup {y}\to \exists {z}\in \left(𝒫{j}\cap {B}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right\}$
6 df-cref ${⊢}\mathrm{CovHasRef}{A}=\left\{{j}\in \mathrm{Top}|\forall {y}\in 𝒫{j}\phantom{\rule{.4em}{0ex}}\left(\bigcup {j}=\bigcup {y}\to \exists {z}\in \left(𝒫{j}\cap {A}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right\}$
7 df-cref ${⊢}\mathrm{CovHasRef}{B}=\left\{{j}\in \mathrm{Top}|\forall {y}\in 𝒫{j}\phantom{\rule{.4em}{0ex}}\left(\bigcup {j}=\bigcup {y}\to \exists {z}\in \left(𝒫{j}\cap {B}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right\}$
8 5 6 7 3eqtr4g ${⊢}{A}={B}\to \mathrm{CovHasRef}{A}=\mathrm{CovHasRef}{B}$