Metamath Proof Explorer

Theorem llyrest

Description: An open subspace of a locally A space is also locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion llyrest ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐵 ) ∈ Locally 𝐴 )

Proof

Step Hyp Ref Expression
1 llytop ⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top )
2 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐵 ) ∈ Top )
3 1 2 sylan ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐵 ) ∈ Top )
4 restopn2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ) )
5 1 4 sylan ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ) )
6 simp1l ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝐽 ∈ Locally 𝐴 )
7 simp2l ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ 𝐽 )
8 simp3 ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
9 llyi ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) )
11 simprl ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ 𝐽 )
12 simprr1 ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ⊆ 𝑥 )
13 simpl2r ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑥 ⊆ 𝐵 )
14 12 13 sstrd ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ⊆ 𝐵 )
15 6 1 syl ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → 𝐽 ∈ Top )
16 15 adantr ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top )
17 simpl1r ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝐵 ∈ 𝐽 )
18 restopn2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝐽 ) → ( 𝑣 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝐵 ) ) )
19 16 17 18 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( 𝑣 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝐵 ) ) )
20 11 14 19 mpbir2and ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ ( 𝐽 ↾t 𝐵 ) )
21 velpw ⊢ ( 𝑣 ∈ 𝒫 𝑥 ↔ 𝑣 ⊆ 𝑥 )
22 12 21 sylibr ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ 𝒫 𝑥 )
23 20 22 elind ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) )
24 simprr2 ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ 𝑣 )
25 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽 ) → ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) = ( 𝐽 ↾t 𝑣 ) )
26 16 14 17 25 syl3anc ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) = ( 𝐽 ↾t 𝑣 ) )
27 simprr3 ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 )
28 26 27 eqeltrd ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 )
29 23 24 28 jca32 ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) ) )
30 29 ex ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑣 ∈ 𝐽 ∧ ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) → ( 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) )
31 30 reximdv2 ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑣 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) → ∃ 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) ) )
32 10 31 mpd ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) )
33 32 3expa ⊢ ( ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) )
34 33 ralrimiva ⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) )
35 34 ex ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) ) )
36 5 35 sylbid ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) ) )
37 36 ralrimiv ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ∀ 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) )
38 islly ⊢ ( ( 𝐽 ↾t 𝐵 ) ∈ Locally 𝐴 ↔ ( ( 𝐽 ↾t 𝐵 ) ∈ Top ∧ ∀ 𝑥 ∈ ( 𝐽 ↾t 𝐵 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑣 ) ∈ 𝐴 ) ) )
39 3 37 38 sylanbrc ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐽 ↾t 𝐵 ) ∈ Locally 𝐴 )