Metamath Proof Explorer

Theorem crefss

Description: The "every open cover has an A refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020)

Ref Expression
Assertion crefss 
|- ( A C_ B -> CovHasRef A C_ CovHasRef B )

Proof

Step Hyp Ref Expression
1 sslin 
 |-  ( A C_ B -> ( ~P j i^i A ) C_ ( ~P j i^i B ) )
2 ssrexv 
 |-  ( ( ~P j i^i A ) C_ ( ~P j i^i B ) -> ( E. z e. ( ~P j i^i A ) z Ref y -> E. z e. ( ~P j i^i B ) z Ref y ) )
3 1 2 syl 
 |-  ( A C_ B -> ( E. z e. ( ~P j i^i A ) z Ref y -> E. z e. ( ~P j i^i B ) z Ref y ) )
4 3 imim2d 
 |-  ( A C_ 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 ) ) )
5 4 ralimdv 
 |-  ( A C_ 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 ) ) )
6 5 anim2d 
 |-  ( A C_ 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 ) ) ) )
7 eqid 
 |-  U. j = U. j
8 7 iscref 
 |-  ( j e. 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 ) ) )
9 7 iscref 
 |-  ( j e. 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 ) ) )
10 6 8 9 3imtr4g 
 |-  ( A C_ B -> ( j e. CovHasRef A -> j e. CovHasRef B ) )
11 10 ssrdv 
 |-  ( A C_ B -> CovHasRef A C_ CovHasRef B )