This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem llyss

Description: The "locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion llyss 
|- ( A C_ B -> Locally A C_ Locally B )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( ( j |`t u ) e. A -> ( j |`t u ) e. B ) )
2 1 anim2d 
 |-  ( A C_ B -> ( ( y e. u /\ ( j |`t u ) e. A ) -> ( y e. u /\ ( j |`t u ) e. B ) ) )
3 2 reximdv 
 |-  ( A C_ B -> ( E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) -> E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) ) )
4 3 ralimdv 
 |-  ( A C_ B -> ( A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) -> A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) ) )
5 4 ralimdv 
 |-  ( A C_ B -> ( A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) -> A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) ) )
6 5 anim2d 
 |-  ( A C_ B -> ( ( j e. Top /\ A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) ) -> ( j e. Top /\ A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) ) ) )
7 islly 
 |-  ( j e. Locally A <-> ( j e. Top /\ A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) ) )
8 islly 
 |-  ( j e. Locally B <-> ( j e. Top /\ A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) ) )
9 6 7 8 3imtr4g 
 |-  ( A C_ B -> ( j e. Locally A -> j e. Locally B ) )
10 9 ssrdv 
 |-  ( A C_ B -> Locally A C_ Locally B )