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 simpr 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> x e. X )
3 vex 
 |-  x e. _V
4 3 snelpw 
 |-  ( x e. X <-> { x } e. ~P X )
5 2 4 sylib 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> { x } e. ~P X )
6 vsnid 
 |-  x e. { x }
7 6 a1i 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> x e. { x } )
8 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 ) )
9 1 5 7 8 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 ) )
10 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 } )
11 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 )
12 11 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 )
13 10 12 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 } )
14 13 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 } ) )
15 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 )
16 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 )
17 16 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 )
18 restdis 
 |-  ( ( X e. V /\ { x } C_ X ) -> ( ~P X |`t { x } ) = ~P { x } )
19 15 17 18 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 } )
20 14 19 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 } )
21 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 )
22 20 21 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 )
23 22 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 ) )
24 23 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 ) )
25 9 24 mpd 
 |-  ( ( ( X e. V /\ ~P X e. Locally A ) /\ x e. X ) -> ~P { x } e. A )
26 25 ralrimiva 
 |-  ( ( X e. V /\ ~P X e. Locally A ) -> A. x e. X ~P { x } e. A )
27 distop 
 |-  ( X e. V -> ~P X e. Top )
28 27 adantr 
 |-  ( ( X e. V /\ A. x e. X ~P { x } e. A ) -> ~P X e. Top )
29 elpwi 
 |-  ( y e. ~P X -> y C_ X )
30 29 adantl 
 |-  ( ( X e. V /\ y e. ~P X ) -> y C_ X )
31 ssralv 
 |-  ( y C_ X -> ( A. x e. X ~P { x } e. A -> A. x e. y ~P { x } e. A ) )
32 30 31 syl 
 |-  ( ( X e. V /\ y e. ~P X ) -> ( A. x e. X ~P { x } e. A -> A. x e. y ~P { x } e. A ) )
33 simprl 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> x e. y )
34 33 snssd 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } C_ y )
35 30 adantr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> y C_ X )
36 34 35 sstrd 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } C_ X )
37 snex 
 |-  { x } e. _V
38 37 elpw 
 |-  ( { x } e. ~P X <-> { x } C_ X )
39 36 38 sylibr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } e. ~P X )
40 37 elpw 
 |-  ( { x } e. ~P y <-> { x } C_ y )
41 34 40 sylibr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } e. ~P y )
42 39 41 elind 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> { x } e. ( ~P X i^i ~P y ) )
43 snidg 
 |-  ( x e. y -> x e. { x } )
44 43 ad2antrl 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> x e. { x } )
45 simpll 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> X e. V )
46 45 36 18 syl2anc 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> ( ~P X |`t { x } ) = ~P { x } )
47 simprr 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> ~P { x } e. A )
48 46 47 eqeltrd 
 |-  ( ( ( X e. V /\ y e. ~P X ) /\ ( x e. y /\ ~P { x } e. A ) ) -> ( ~P X |`t { x } ) e. A )
49 eleq2 
 |-  ( u = { x } -> ( x e. u <-> x e. { x } ) )
50 oveq2 
 |-  ( u = { x } -> ( ~P X |`t u ) = ( ~P X |`t { x } ) )
51 50 eleq1d 
 |-  ( u = { x } -> ( ( ~P X |`t u ) e. A <-> ( ~P X |`t { x } ) e. A ) )
52 49 51 anbi12d 
 |-  ( u = { x } -> ( ( x e. u /\ ( ~P X |`t u ) e. A ) <-> ( x e. { x } /\ ( ~P X |`t { x } ) e. A ) ) )
53 52 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 ) )
54 42 44 48 53 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 ) )
55 54 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 ) ) )
56 55 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 ) ) )
57 32 56 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 ) ) )
58 57 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 ) )
59 58 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 ) )
60 59 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 ) )
61 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 ) ) )
62 28 60 61 sylanbrc 
 |-  ( ( X e. V /\ A. x e. X ~P { x } e. A ) -> ~P X e. Locally A )
63 26 62 impbida 
 |-  ( X e. V -> ( ~P X e. Locally A <-> A. x e. X ~P { x } e. A ) )