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 ( 𝑋 ∈ 𝑉 → ( 𝒫 𝑋 ∈ Locally 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → 𝒫 𝑋 ∈ Locally 𝐴 )
2 simpr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
3 vex ⊢ 𝑥 ∈ V
4 3 snelpw ⊢ ( 𝑥 ∈ 𝑋 ↔ { 𝑥 } ∈ 𝒫 𝑋 )
5 2 4 sylib ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ 𝒫 𝑋 )
6 vsnid ⊢ 𝑥 ∈ { 𝑥 }
7 6 a1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ { 𝑥 } )
8 llyi ⊢ ( ( 𝒫 𝑋 ∈ Locally 𝐴 ∧ { 𝑥 } ∈ 𝒫 𝑋 ∧ 𝑥 ∈ { 𝑥 } ) → ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) )
9 1 5 7 8 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) )
10 simpr1 ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → 𝑦 ⊆ { 𝑥 } )
11 simpr2 ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → 𝑥 ∈ 𝑦 )
12 11 snssd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → { 𝑥 } ⊆ 𝑦 )
13 10 12 eqssd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → 𝑦 = { 𝑥 } )
14 13 oveq2d ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → ( 𝒫 𝑋 ↾t 𝑦 ) = ( 𝒫 𝑋 ↾t { 𝑥 } ) )
15 simplll ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → 𝑋 ∈ 𝑉 )
16 simplr ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → 𝑥 ∈ 𝑋 )
17 16 snssd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → { 𝑥 } ⊆ 𝑋 )
18 restdis ⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑥 } ⊆ 𝑋 ) → ( 𝒫 𝑋 ↾t { 𝑥 } ) = 𝒫 { 𝑥 } )
19 15 17 18 syl2anc ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → ( 𝒫 𝑋 ↾t { 𝑥 } ) = 𝒫 { 𝑥 } )
20 14 19 eqtrd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → ( 𝒫 𝑋 ↾t 𝑦 ) = 𝒫 { 𝑥 } )
21 simpr3 ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 )
22 20 21 eqeltrrd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) ) → 𝒫 { 𝑥 } ∈ 𝐴 )
23 22 ex ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) → 𝒫 { 𝑥 } ∈ 𝐴 ) )
24 23 rexlimdvw ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ⊆ { 𝑥 } ∧ 𝑥 ∈ 𝑦 ∧ ( 𝒫 𝑋 ↾t 𝑦 ) ∈ 𝐴 ) → 𝒫 { 𝑥 } ∈ 𝐴 ) )
25 9 24 mpd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → 𝒫 { 𝑥 } ∈ 𝐴 )
26 25 ralrimiva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝒫 𝑋 ∈ Locally 𝐴 ) → ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 )
27 distop ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Top )
28 27 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 ) → 𝒫 𝑋 ∈ Top )
29 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
30 29 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) → 𝑦 ⊆ 𝑋 )
31 ssralv ⊢ ( 𝑦 ⊆ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 → ∀ 𝑥 ∈ 𝑦 𝒫 { 𝑥 } ∈ 𝐴 ) )
32 30 31 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 → ∀ 𝑥 ∈ 𝑦 𝒫 { 𝑥 } ∈ 𝐴 ) )
33 simprl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → 𝑥 ∈ 𝑦 )
34 33 snssd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → { 𝑥 } ⊆ 𝑦 )
35 30 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → 𝑦 ⊆ 𝑋 )
36 34 35 sstrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → { 𝑥 } ⊆ 𝑋 )
37 snex ⊢ { 𝑥 } ∈ V
38 37 elpw ⊢ ( { 𝑥 } ∈ 𝒫 𝑋 ↔ { 𝑥 } ⊆ 𝑋 )
39 36 38 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → { 𝑥 } ∈ 𝒫 𝑋 )
40 37 elpw ⊢ ( { 𝑥 } ∈ 𝒫 𝑦 ↔ { 𝑥 } ⊆ 𝑦 )
41 34 40 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → { 𝑥 } ∈ 𝒫 𝑦 )
42 39 41 elind ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → { 𝑥 } ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) )
43 snidg ⊢ ( 𝑥 ∈ 𝑦 → 𝑥 ∈ { 𝑥 } )
44 43 ad2antrl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → 𝑥 ∈ { 𝑥 } )
45 simpll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → 𝑋 ∈ 𝑉 )
46 45 36 18 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → ( 𝒫 𝑋 ↾t { 𝑥 } ) = 𝒫 { 𝑥 } )
47 simprr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → 𝒫 { 𝑥 } ∈ 𝐴 )
48 46 47 eqeltrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → ( 𝒫 𝑋 ↾t { 𝑥 } ) ∈ 𝐴 )
49 eleq2 ⊢ ( 𝑢 = { 𝑥 } → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ { 𝑥 } ) )
50 oveq2 ⊢ ( 𝑢 = { 𝑥 } → ( 𝒫 𝑋 ↾t 𝑢 ) = ( 𝒫 𝑋 ↾t { 𝑥 } ) )
51 50 eleq1d ⊢ ( 𝑢 = { 𝑥 } → ( ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ↔ ( 𝒫 𝑋 ↾t { 𝑥 } ) ∈ 𝐴 ) )
52 49 51 anbi12d ⊢ ( 𝑢 = { 𝑥 } → ( ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ( 𝑥 ∈ { 𝑥 } ∧ ( 𝒫 𝑋 ↾t { 𝑥 } ) ∈ 𝐴 ) ) )
53 52 rspcev ⊢ ( ( { 𝑥 } ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ { 𝑥 } ∧ ( 𝒫 𝑋 ↾t { 𝑥 } ) ∈ 𝐴 ) ) → ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) )
54 42 44 48 53 syl12anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝒫 { 𝑥 } ∈ 𝐴 ) ) → ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) )
55 54 expr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝒫 { 𝑥 } ∈ 𝐴 → ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) ) )
56 55 ralimdva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ∀ 𝑥 ∈ 𝑦 𝒫 { 𝑥 } ∈ 𝐴 → ∀ 𝑥 ∈ 𝑦 ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) ) )
57 32 56 syld ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 → ∀ 𝑥 ∈ 𝑦 ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) ) )
58 57 imp ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑦 ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) )
59 58 an32s ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ∀ 𝑥 ∈ 𝑦 ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) )
60 59 ralrimiva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝒫 𝑋 ∀ 𝑥 ∈ 𝑦 ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) )
61 islly ⊢ ( 𝒫 𝑋 ∈ Locally 𝐴 ↔ ( 𝒫 𝑋 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑋 ∀ 𝑥 ∈ 𝑦 ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ 𝒫 𝑦 ) ( 𝑥 ∈ 𝑢 ∧ ( 𝒫 𝑋 ↾t 𝑢 ) ∈ 𝐴 ) ) )
62 28 60 61 sylanbrc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 ) → 𝒫 𝑋 ∈ Locally 𝐴 )
63 26 62 impbida ⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 𝑋 ∈ Locally 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 𝐴 ) )