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

Metamath Proof Explorer

Theorem nllyss

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

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

Proof

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