Metamath Proof Explorer

Theorem nllyidm

Description: Idempotence of the "n-locally" predicate, i.e. being "n-locally A " is a local property. (Use loclly to show N-Locally N-Locally A = N-Locally A .) (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion nllyidm 
|- Locally N-Locally A = N-Locally A

Proof

Step Hyp Ref Expression
1 llytop 
 |-  ( j e. Locally N-Locally A -> j e. Top )
2 llyi 
 |-  ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) -> E. u e. j ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) )
3 simprr3 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> ( j |`t u ) e. N-Locally A )
4 simprl 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> u e. j )
5 ssidd 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> u C_ u )
6 simpl1 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> j e. Locally N-Locally A )
7 6 1 syl 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> j e. Top )
8 restopn2 
 |-  ( ( j e. Top /\ u e. j ) -> ( u e. ( j |`t u ) <-> ( u e. j /\ u C_ u ) ) )
9 7 4 8 syl2anc 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> ( u e. ( j |`t u ) <-> ( u e. j /\ u C_ u ) ) )
10 4 5 9 mpbir2and 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> u e. ( j |`t u ) )
11 simprr2 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> y e. u )
12 nlly2i 
 |-  ( ( ( j |`t u ) e. N-Locally A /\ u e. ( j |`t u ) /\ y e. u ) -> E. v e. ~P u E. z e. ( j |`t u ) ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) )
13 3 10 11 12 syl3anc 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> E. v e. ~P u E. z e. ( j |`t u ) ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) )
14 restopn2 
 |-  ( ( j e. Top /\ u e. j ) -> ( z e. ( j |`t u ) <-> ( z e. j /\ z C_ u ) ) )
15 7 4 14 syl2anc 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> ( z e. ( j |`t u ) <-> ( z e. j /\ z C_ u ) ) )
16 15 adantr 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ v e. ~P u ) -> ( z e. ( j |`t u ) <-> ( z e. j /\ z C_ u ) ) )
17 7 adantr 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> j e. Top )
18 simpr2l 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> z e. j )
19 simpr31 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> y e. z )
20 opnneip 
 |-  ( ( j e. Top /\ z e. j /\ y e. z ) -> z e. ( ( nei ` j ) ` { y } ) )
21 17 18 19 20 syl3anc 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> z e. ( ( nei ` j ) ` { y } ) )
22 simpr32 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> z C_ v )
23 simpr1 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v e. ~P u )
24 23 elpwid 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v C_ u )
25 4 adantr 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> u e. j )
26 elssuni 
 |-  ( u e. j -> u C_ U. j )
27 25 26 syl 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> u C_ U. j )
28 24 27 sstrd 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v C_ U. j )
29 eqid 
 |-  U. j = U. j
30 29 ssnei2 
 |-  ( ( ( j e. Top /\ z e. ( ( nei ` j ) ` { y } ) ) /\ ( z C_ v /\ v C_ U. j ) ) -> v e. ( ( nei ` j ) ` { y } ) )
31 17 21 22 28 30 syl22anc 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v e. ( ( nei ` j ) ` { y } ) )
32 simprr1 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> u C_ x )
33 32 adantr 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> u C_ x )
34 24 33 sstrd 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v C_ x )
35 velpw 
 |-  ( v e. ~P x <-> v C_ x )
36 34 35 sylibr 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v e. ~P x )
37 31 36 elind 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) )
38 restabs 
 |-  ( ( j e. Top /\ v C_ u /\ u e. j ) -> ( ( j |`t u ) |`t v ) = ( j |`t v ) )
39 17 24 25 38 syl3anc 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> ( ( j |`t u ) |`t v ) = ( j |`t v ) )
40 simpr33 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> ( ( j |`t u ) |`t v ) e. A )
41 39 40 eqeltrrd 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> ( j |`t v ) e. A )
42 37 41 jca 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ ( v e. ~P u /\ ( z e. j /\ z C_ u ) /\ ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> ( v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) /\ ( j |`t v ) e. A ) )
43 42 3exp2 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> ( v e. ~P u -> ( ( z e. j /\ z C_ u ) -> ( ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) -> ( v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) /\ ( j |`t v ) e. A ) ) ) ) )
44 43 imp 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ v e. ~P u ) -> ( ( z e. j /\ z C_ u ) -> ( ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) -> ( v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) /\ ( j |`t v ) e. A ) ) ) )
45 16 44 sylbid 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ v e. ~P u ) -> ( z e. ( j |`t u ) -> ( ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) -> ( v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) /\ ( j |`t v ) e. A ) ) ) )
46 45 rexlimdv 
 |-  ( ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) /\ v e. ~P u ) -> ( E. z e. ( j |`t u ) ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) -> ( v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) /\ ( j |`t v ) e. A ) ) )
47 46 expimpd 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> ( ( v e. ~P u /\ E. z e. ( j |`t u ) ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) ) -> ( v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) /\ ( j |`t v ) e. A ) ) )
48 47 reximdv2 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> ( E. v e. ~P u E. z e. ( j |`t u ) ( y e. z /\ z C_ v /\ ( ( j |`t u ) |`t v ) e. A ) -> E. v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t v ) e. A ) )
49 13 48 mpd 
 |-  ( ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. N-Locally A ) ) ) -> E. v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t v ) e. A )
50 2 49 rexlimddv 
 |-  ( ( j e. Locally N-Locally A /\ x e. j /\ y e. x ) -> E. v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t v ) e. A )
51 50 3expb 
 |-  ( ( j e. Locally N-Locally A /\ ( x e. j /\ y e. x ) ) -> E. v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t v ) e. A )
52 51 ralrimivva 
 |-  ( j e. Locally N-Locally A -> A. x e. j A. y e. x E. v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t v ) e. A )
53 isnlly 
 |-  ( j e. N-Locally A <-> ( j e. Top /\ A. x e. j A. y e. x E. v e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t v ) e. A ) )
54 1 52 53 sylanbrc 
 |-  ( j e. Locally N-Locally A -> j e. N-Locally A )
55 54 ssriv 
 |-  Locally N-Locally A C_ N-Locally A
56 nllyrest 
 |-  ( ( j e. N-Locally A /\ x e. j ) -> ( j |`t x ) e. N-Locally A )
57 56 adantl 
 |-  ( ( T. /\ ( j e. N-Locally A /\ x e. j ) ) -> ( j |`t x ) e. N-Locally A )
58 nllytop 
 |-  ( j e. N-Locally A -> j e. Top )
59 58 ssriv 
 |-  N-Locally A C_ Top
60 59 a1i 
 |-  ( T. -> N-Locally A C_ Top )
61 57 60 restlly 
 |-  ( T. -> N-Locally A C_ Locally N-Locally A )
62 61 mptru 
 |-  N-Locally A C_ Locally N-Locally A
63 55 62 eqssi 
 |-  Locally N-Locally A = N-Locally A