Metamath Proof Explorer

Theorem dislly

Description: The discrete space ~P X is locally A if and only if every singleton space has property A . (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion dislly 
|- ( X e. V -> ( ~P X e. Locally A <-> A. x e. X ~P { x } e. A ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> ~P X e. Locally A )
2 vex 
 |-  x e. _V
3 2 snelpw 
 |-  ( x e. X <-> { x } e. ~P X )
4 3 bilani 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> { x } e. ~P X )
5 vsnid 
 |-  x e. { x }
6 5 a1i 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> x e. { x } )
7 llyi 
 |-  ( ( ~P X e. Locally A /\ { x } e. ~P X /\ x e. { x } ) -> E. y e. ~P X ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) )
8 1 4 6 7 syl3anc 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> E. y e. ~P X ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) )
9 simpr1 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> y C_ { x } )
10 simpr2 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> x e. y )
11 10 snssd 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> { x } C_ y )
12 9 11 eqssd 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> y = { x } )
13 12 oveq2d 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> ( ~P X |`t y ) = ( ~P X |`t { x } ) )
14 simplll 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> X e. V )
15 simplr 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> x e. X )
16 15 snssd 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> { x } C_ X )
17 restdis 
 |-  ( ( X e. V /\ { x } C_ X ) -> ( ~P X |`t { x } ) = ~P { x } )
18 14 16 17 syl2anc 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> ( ~P X |`t { x } ) = ~P { x } )
19 13 18 eqtrd 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> ( ~P X |`t y ) = ~P { x } )
20 simpr3 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> ( ~P X |`t y ) e. A )
21 19 20 eqeltrrd 
 |-  ( ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) /\ ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) ) -> ~P { x } e. A )
22 21 ex 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> ( ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) -> ~P { x } e. A ) )
23 22 rexlimdvw 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> ( E. y e. ~P X ( y C_ { x } /\ x e. y /\ ( ~P X |`t y ) e. A ) -> ~P { x } e. A ) )
24 8 23 mpd 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> ~P { x } e. A )
25 24 ralrimiva 
 |-  ( ( X e. V /\ ~P X e. Locally A ) -> A. x e. X ~P { x } e. A )
26 distop 
 |-  ( X e. V -> ~P X e. Top )
27 26 adantr 
 |-  ( ( X e. V /\ A. x e. X ~P { x } e. A ) -> ~P X e. Top )
28 elpwi 
 |-  ( y e. ~P X -> y C_ X )
29 28 adantl 
 |-  ( ( X e. V /\ y e. ~P X ) -> y C_ X )
30 ssralv 
 |-  ( y C_ X -> ( A. x e. X ~P { x } e. A -> A. x e. y ~P { x } e. A ) )
31 29 30 syl 
 |-  ( ( X e. V /\ y e. ~P X ) -> ( A. x e. X ~P { x } e. A -> A. x e. y ~P { x } e. A ) )
32 simprl 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> x e. y )
33 32 snssd 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } C_ y )
34 29 adantr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> y C_ X )
35 33 34 sstrd 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } C_ X )
36 vsnex 
 |-  { x } e. _V
37 36 elpw 
 |-  ( { x } e. ~P X <-> { x } C_ X )
38 35 37 sylibr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } e. ~P X )
39 36 elpw 
 |-  ( { x } e. ~P y <-> { x } C_ y )
40 33 39 sylibr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } e. ~P y )
41 38 40 elind 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } e. ( ~P X i^i ~P y ) )
42 snidg 
 |-  ( x e. y -> x e. { x } )
43 42 ad2antrl 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> x e. { x } )
44 simpll 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> X e. V )
45 44 35 17 syl2anc 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> ( ~P X |`t { x } ) = ~P { x } )
46 simprr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> ~P { x } e. A )
47 45 46 eqeltrd 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> ( ~P X |`t { x } ) e. A )
48 eleq2 
 |-  ( u = { x } -> ( x e. u <-> x e. { x } ) )
49 oveq2 
 |-  ( u = { x } -> ( ~P X |`t u ) = ( ~P X |`t { x } ) )
50 49 eleq1d 
 |-  ( u = { x } -> ( ( ~P X |`t u ) e. A <-> ( ~P X |`t { x } ) e. A ) )
51 48 50 anbi12d 
 |-  ( u = { x } -> ( ( x e. u /\ ( ~P X |`t u ) e. A ) <-> ( x e. { x } /\ ( ~P X |`t { x } ) e. A ) ) )
52 51 rspcev 
 |-  ( ( { x } e. ( ~P X i^i ~P y ) /\ ( x e. { x } /\ ( ~P X |`t { x } ) e. A ) ) -> E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) )
53 41 43 47 52 syl12anc 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) )
54 53 expr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ x e. y ) -> ( ~P { x } e. A -> E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) ) )
55 54 ralimdva 
 |-  ( ( X e. V /\ y e. ~P X ) -> ( A. x e. y ~P { x } e. A -> A. x e. y E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) ) )
56 31 55 syld 
 |-  ( ( X e. V /\ y e. ~P X ) -> ( A. x e. X ~P { x } e. A -> A. x e. y E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) ) )
57 56 imp 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ A. x e. X ~P { x } e. A ) -> A. x e. y E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) )
58 57 an32s 
 |-  ( ( ( X e. V /\ A. x e. X ~P { x } e. A ) /\ y e. ~P X ) -> A. x e. y E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) )
59 58 ralrimiva 
 |-  ( ( X e. V /\ A. x e. X ~P { x } e. A ) -> A. y e. ~P X A. x e. y E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) )
60 islly 
 |-  ( ~P X e. Locally A <-> ( ~P X e. Top /\ A. y e. ~P X A. x e. y E. u e. ( ~P X i^i ~P y ) ( x e. u /\ ( ~P X |`t u ) e. A ) ) )
61 27 59 60 sylanbrc 
 |-  ( ( X e. V /\ A. x e. X ~P { x } e. A ) -> ~P X e. Locally A )
62 25 61 impbida 
 |-  ( X e. V -> ( ~P X e. Locally A <-> A. x e. X ~P { x } e. A ) )