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 )