Metamath Proof Explorer


Theorem restnlly

Description: If the property A passes to open subspaces, then a space is n-locally A iff it is locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Hypothesis restlly.1 ( ( 𝜑 ∧ ( 𝑗𝐴𝑥𝑗 ) ) → ( 𝑗t 𝑥 ) ∈ 𝐴 )
Assertion restnlly ( 𝜑 → 𝑛-Locally 𝐴 = Locally 𝐴 )

Proof

Step Hyp Ref Expression
1 restlly.1 ( ( 𝜑 ∧ ( 𝑗𝐴𝑥𝑗 ) ) → ( 𝑗t 𝑥 ) ∈ 𝐴 )
2 nllytop ( 𝑘 ∈ 𝑛-Locally 𝐴𝑘 ∈ Top )
3 2 adantl ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) → 𝑘 ∈ Top )
4 nlly2i ( ( 𝑘 ∈ 𝑛-Locally 𝐴𝑦𝑘𝑢𝑦 ) → ∃ 𝑠 ∈ 𝒫 𝑦𝑥𝑘 ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) )
5 4 3adant1l ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) → ∃ 𝑠 ∈ 𝒫 𝑦𝑥𝑘 ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) )
6 simprl ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥𝑘 )
7 simprr2 ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥𝑠 )
8 simplr ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ 𝒫 𝑦 )
9 8 elpwid ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠𝑦 )
10 7 9 sstrd ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥𝑦 )
11 velpw ( 𝑥 ∈ 𝒫 𝑦𝑥𝑦 )
12 10 11 sylibr ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ∈ 𝒫 𝑦 )
13 6 12 elind ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) )
14 simprr1 ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑢𝑥 )
15 simpll1 ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) )
16 15 2 simpl2im ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑘 ∈ Top )
17 restabs ( ( 𝑘 ∈ Top ∧ 𝑥𝑠𝑠 ∈ 𝒫 𝑦 ) → ( ( 𝑘t 𝑠 ) ↾t 𝑥 ) = ( 𝑘t 𝑥 ) )
18 16 7 8 17 syl3anc ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( 𝑘t 𝑠 ) ↾t 𝑥 ) = ( 𝑘t 𝑥 ) )
19 df-ss ( 𝑥𝑠 ↔ ( 𝑥𝑠 ) = 𝑥 )
20 7 19 sylib ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑥𝑠 ) = 𝑥 )
21 elrestr ( ( 𝑘 ∈ Top ∧ 𝑠 ∈ 𝒫 𝑦𝑥𝑘 ) → ( 𝑥𝑠 ) ∈ ( 𝑘t 𝑠 ) )
22 16 8 6 21 syl3anc ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑥𝑠 ) ∈ ( 𝑘t 𝑠 ) )
23 20 22 eqeltrrd ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ∈ ( 𝑘t 𝑠 ) )
24 eleq2 ( 𝑗 = ( 𝑘t 𝑠 ) → ( 𝑥𝑗𝑥 ∈ ( 𝑘t 𝑠 ) ) )
25 oveq1 ( 𝑗 = ( 𝑘t 𝑠 ) → ( 𝑗t 𝑥 ) = ( ( 𝑘t 𝑠 ) ↾t 𝑥 ) )
26 25 eleq1d ( 𝑗 = ( 𝑘t 𝑠 ) → ( ( 𝑗t 𝑥 ) ∈ 𝐴 ↔ ( ( 𝑘t 𝑠 ) ↾t 𝑥 ) ∈ 𝐴 ) )
27 24 26 imbi12d ( 𝑗 = ( 𝑘t 𝑠 ) → ( ( 𝑥𝑗 → ( 𝑗t 𝑥 ) ∈ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝑘t 𝑠 ) → ( ( 𝑘t 𝑠 ) ↾t 𝑥 ) ∈ 𝐴 ) ) )
28 15 simpld ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → 𝜑 )
29 1 expr ( ( 𝜑𝑗𝐴 ) → ( 𝑥𝑗 → ( 𝑗t 𝑥 ) ∈ 𝐴 ) )
30 29 ralrimiva ( 𝜑 → ∀ 𝑗𝐴 ( 𝑥𝑗 → ( 𝑗t 𝑥 ) ∈ 𝐴 ) )
31 28 30 syl ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ∀ 𝑗𝐴 ( 𝑥𝑗 → ( 𝑗t 𝑥 ) ∈ 𝐴 ) )
32 simprr3 ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑘t 𝑠 ) ∈ 𝐴 )
33 27 31 32 rspcdva ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑥 ∈ ( 𝑘t 𝑠 ) → ( ( 𝑘t 𝑠 ) ↾t 𝑥 ) ∈ 𝐴 ) )
34 23 33 mpd ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( 𝑘t 𝑠 ) ↾t 𝑥 ) ∈ 𝐴 )
35 18 34 eqeltrrd ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑘t 𝑥 ) ∈ 𝐴 )
36 13 14 35 jca32 ( ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ∧ ( 𝑢𝑥 ∧ ( 𝑘t 𝑥 ) ∈ 𝐴 ) ) )
37 36 ex ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( 𝑥𝑘 ∧ ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) ) → ( 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ∧ ( 𝑢𝑥 ∧ ( 𝑘t 𝑥 ) ∈ 𝐴 ) ) ) )
38 37 reximdv2 ( ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ∃ 𝑥𝑘 ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢𝑥 ∧ ( 𝑘t 𝑥 ) ∈ 𝐴 ) ) )
39 38 rexlimdva ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) → ( ∃ 𝑠 ∈ 𝒫 𝑦𝑥𝑘 ( 𝑢𝑥𝑥𝑠 ∧ ( 𝑘t 𝑠 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢𝑥 ∧ ( 𝑘t 𝑥 ) ∈ 𝐴 ) ) )
40 5 39 mpd ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦𝑘𝑢𝑦 ) → ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢𝑥 ∧ ( 𝑘t 𝑥 ) ∈ 𝐴 ) )
41 40 3expb ( ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ ( 𝑦𝑘𝑢𝑦 ) ) → ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢𝑥 ∧ ( 𝑘t 𝑥 ) ∈ 𝐴 ) )
42 41 ralrimivva ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) → ∀ 𝑦𝑘𝑢𝑦𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢𝑥 ∧ ( 𝑘t 𝑥 ) ∈ 𝐴 ) )
43 islly ( 𝑘 ∈ Locally 𝐴 ↔ ( 𝑘 ∈ Top ∧ ∀ 𝑦𝑘𝑢𝑦𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢𝑥 ∧ ( 𝑘t 𝑥 ) ∈ 𝐴 ) ) )
44 3 42 43 sylanbrc ( ( 𝜑𝑘 ∈ 𝑛-Locally 𝐴 ) → 𝑘 ∈ Locally 𝐴 )
45 44 ex ( 𝜑 → ( 𝑘 ∈ 𝑛-Locally 𝐴𝑘 ∈ Locally 𝐴 ) )
46 45 ssrdv ( 𝜑 → 𝑛-Locally 𝐴 ⊆ Locally 𝐴 )
47 llyssnlly Locally 𝐴 ⊆ 𝑛-Locally 𝐴
48 47 a1i ( 𝜑 → Locally 𝐴 ⊆ 𝑛-Locally 𝐴 )
49 46 48 eqssd ( 𝜑 → 𝑛-Locally 𝐴 = Locally 𝐴 )