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 -> CovHasRef A = CovHasRef B )

Proof

Step	Hyp	Ref	Expression
1		ineq2	|- ( A = B -> ( ~P j i^i A ) = ( ~P j i^i B ) )
2	1	rexeqdv	|- ( A = B -> ( E. z e. ( ~P j i^i A ) z Ref y <-> E. z e. ( ~P j i^i B ) z Ref y ) )
3	2	imbi2d	|- ( A = B -> ( ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) <-> ( U. j = U. y -> E. z e. ( ~P j i^i B ) z Ref y ) ) )
4	3	ralbidv	|- ( A = B -> ( A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) <-> A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i B ) z Ref y ) ) )
5	4	rabbidv	|- ( A = B -> { j e. Top | A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) } = { j e. Top | A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i B ) z Ref y ) } )
6		df-cref	|- CovHasRef A = { j e. Top | A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) }
7		df-cref	|- CovHasRef B = { j e. Top | A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i B ) z Ref y ) }
8	5 6 7	3eqtr4g	|- ( A = B -> CovHasRef A = CovHasRef B )