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 )