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 𝐴 )