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 = U. J
Assertion	iscref	|- ( J e. CovHasRef A <-> ( J e. Top /\ A. y e. ~P J ( X = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscref.x	|- X = U. J
2		pweq	|- ( j = J -> ~P j = ~P J )
3		unieq	|- ( j = J -> U. j = U. J )
4	3 1	eqtr4di	|- ( j = J -> U. j = X )
5	4	eqeq1d	|- ( j = J -> ( U. j = U. y <-> X = U. y ) )
6	2	ineq1d	|- ( j = J -> ( ~P j i^i A ) = ( ~P J i^i A ) )
7	6	rexeqdv	|- ( j = J -> ( E. z e. ( ~P j i^i A ) z Ref y <-> E. z e. ( ~P J i^i A ) z Ref y ) )
8	5 7	imbi12d	|- ( j = J -> ( ( U. j = U. y -> E. z e. ( ~P j i^i A ) z Ref y ) <-> ( X = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) ) )
9	2 8	raleqbidv	|- ( j = J -> ( 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 ( X = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) ) )
10		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 ) }
11	9 10	elrab2	|- ( J e. CovHasRef A <-> ( J e. Top /\ A. y e. ~P J ( X = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) ) )