Metamath Proof Explorer

Theorem llyidm

Description: Idempotence of the "locally" predicate, i.e. being "locally A " is a local property. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion llyidm 
|- Locally Locally A = Locally A

Proof

Step Hyp Ref Expression
1 llytop 
 |-  ( j e. Locally Locally A -> j e. Top )
2 llyi 
 |-  ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) -> E. u e. j ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) )
3 simprr3 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> ( j |`t u ) e. Locally A )
4 simprl 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> u e. j )
5 ssidd 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> u C_ u )
6 1 3ad2ant1 
 |-  ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) -> j e. Top )
7 6 adantr 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. 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 Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> ( u e. ( j |`t u ) <-> ( u e. j /\ u C_ u ) ) )
10 4 5 9 mpbir2and 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> u e. ( j |`t u ) )
11 simprr2 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> y e. u )
12 llyi 
 |-  ( ( ( j |`t u ) e. Locally A /\ u e. ( j |`t u ) /\ y e. u ) -> E. v e. ( j |`t u ) ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) )
13 3 10 11 12 syl3anc 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> E. v e. ( j |`t u ) ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) )
14 restopn2 
 |-  ( ( j e. Top /\ u e. j ) -> ( v e. ( j |`t u ) <-> ( v e. j /\ v C_ u ) ) )
15 7 4 14 syl2anc 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> ( v e. ( j |`t u ) <-> ( v e. j /\ v C_ u ) ) )
16 simpl 
 |-  ( ( v e. j /\ v C_ u ) -> v e. j )
17 15 16 biimtrdi 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> ( v e. ( j |`t u ) -> v e. j ) )
18 simprl 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v e. j )
19 simprr1 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v C_ u )
20 simprr1 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> u C_ x )
21 20 adantr 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> u C_ x )
22 19 21 sstrd 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v C_ x )
23 velpw 
 |-  ( v e. ~P x <-> v C_ x )
24 22 23 sylibr 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v e. ~P x )
25 18 24 elind 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> v e. ( j i^i ~P x ) )
26 simprr2 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> y e. v )
27 7 adantr 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> j e. Top )
28 simplrl 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> u e. j )
29 restabs 
 |-  ( ( j e. Top /\ v C_ u /\ u e. j ) -> ( ( j |`t u ) |`t v ) = ( j |`t v ) )
30 27 19 28 29 syl3anc 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> ( ( j |`t u ) |`t v ) = ( j |`t v ) )
31 simprr3 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> ( ( j |`t u ) |`t v ) e. A )
32 30 31 eqeltrrd 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> ( j |`t v ) e. A )
33 25 26 32 jca32 
 |-  ( ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) /\ ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) ) -> ( v e. ( j i^i ~P x ) /\ ( y e. v /\ ( j |`t v ) e. A ) ) )
34 33 ex 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> ( ( v e. j /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) -> ( v e. ( j i^i ~P x ) /\ ( y e. v /\ ( j |`t v ) e. A ) ) ) )
35 17 34 syland 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> ( ( v e. ( j |`t u ) /\ ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) ) -> ( v e. ( j i^i ~P x ) /\ ( y e. v /\ ( j |`t v ) e. A ) ) ) )
36 35 reximdv2 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> ( E. v e. ( j |`t u ) ( v C_ u /\ y e. v /\ ( ( j |`t u ) |`t v ) e. A ) -> E. v e. ( j i^i ~P x ) ( y e. v /\ ( j |`t v ) e. A ) ) )
37 13 36 mpd 
 |-  ( ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) /\ ( u e. j /\ ( u C_ x /\ y e. u /\ ( j |`t u ) e. Locally A ) ) ) -> E. v e. ( j i^i ~P x ) ( y e. v /\ ( j |`t v ) e. A ) )
38 2 37 rexlimddv 
 |-  ( ( j e. Locally Locally A /\ x e. j /\ y e. x ) -> E. v e. ( j i^i ~P x ) ( y e. v /\ ( j |`t v ) e. A ) )
39 38 3expb 
 |-  ( ( j e. Locally Locally A /\ ( x e. j /\ y e. x ) ) -> E. v e. ( j i^i ~P x ) ( y e. v /\ ( j |`t v ) e. A ) )
40 39 ralrimivva 
 |-  ( j e. Locally Locally A -> A. x e. j A. y e. x E. v e. ( j i^i ~P x ) ( y e. v /\ ( j |`t v ) e. A ) )
41 islly 
 |-  ( j e. Locally A <-> ( j e. Top /\ A. x e. j A. y e. x E. v e. ( j i^i ~P x ) ( y e. v /\ ( j |`t v ) e. A ) ) )
42 1 40 41 sylanbrc 
 |-  ( j e. Locally Locally A -> j e. Locally A )
43 42 ssriv 
 |-  Locally Locally A C_ Locally A
44 llyrest 
 |-  ( ( j e. Locally A /\ x e. j ) -> ( j |`t x ) e. Locally A )
45 44 adantl 
 |-  ( ( T. /\ ( j e. Locally A /\ x e. j ) ) -> ( j |`t x ) e. Locally A )
46 llytop 
 |-  ( j e. Locally A -> j e. Top )
47 46 ssriv 
 |-  Locally A C_ Top
48 47 a1i 
 |-  ( T. -> Locally A C_ Top )
49 45 48 restlly 
 |-  ( T. -> Locally A C_ Locally Locally A )
50 49 mptru 
 |-  Locally A C_ Locally Locally A
51 43 50 eqssi 
 |-  Locally Locally A = Locally A