Metamath Proof Explorer

Theorem crefi

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

Proof

Step Hyp Ref Expression
1 crefi.x 
 |-  X = U. J
2 simp1 
 |-  ( ( J e. CovHasRef A /\ C C_ J /\ X = U. C ) -> J e. CovHasRef A )
3 simp2 
 |-  ( ( J e. CovHasRef A /\ C C_ J /\ X = U. C ) -> C C_ J )
4 2 3 sselpwd 
 |-  ( ( J e. CovHasRef A /\ C C_ J /\ X = U. C ) -> C e. ~P J )
5 1 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 ) ) )
6 5 simprbi 
 |-  ( J e. CovHasRef A -> A. y e. ~P J ( X = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) )
7 6 3ad2ant1 
 |-  ( ( J e. CovHasRef A /\ C C_ J /\ X = U. C ) -> A. y e. ~P J ( X = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) )
8 simp3 
 |-  ( ( J e. CovHasRef A /\ C C_ J /\ X = U. C ) -> X = U. C )
9 unieq 
 |-  ( y = C -> U. y = U. C )
10 9 eqeq2d 
 |-  ( y = C -> ( X = U. y <-> X = U. C ) )
11 breq2 
 |-  ( y = C -> ( z Ref y <-> z Ref C ) )
12 11 rexbidv 
 |-  ( y = C -> ( E. z e. ( ~P J i^i A ) z Ref y <-> E. z e. ( ~P J i^i A ) z Ref C ) )
13 10 12 imbi12d 
 |-  ( y = C -> ( ( X = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) <-> ( X = U. C -> E. z e. ( ~P J i^i A ) z Ref C ) ) )
14 13 rspcv 
 |-  ( C e. ~P J -> ( A. y e. ~P J ( X = U. y -> E. z e. ( ~P J i^i A ) z Ref y ) -> ( X = U. C -> E. z e. ( ~P J i^i A ) z Ref C ) ) )
15 4 7 8 14 syl3c 
 |-  ( ( J e. CovHasRef A /\ C C_ J /\ X = U. C ) -> E. z e. ( ~P J i^i A ) z Ref C )