Metamath Proof Explorer

Theorem llyi

Description: The property of a locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion llyi ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 islly ⊢ ( 𝐽 ∈ Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
2 1 simprbi ⊢ ( 𝐽 ∈ Locally 𝐴 → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
3 pweq ⊢ ( 𝑥 = 𝑈 → 𝒫 𝑥 = 𝒫 𝑈 )
4 3 ineq2d ⊢ ( 𝑥 = 𝑈 → ( 𝐽 ∩ 𝒫 𝑥 ) = ( 𝐽 ∩ 𝒫 𝑈 ) )
5 4 rexeqdv ⊢ ( 𝑥 = 𝑈 → ( ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
6 5 raleqbi1dv ⊢ ( 𝑥 = 𝑈 → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
7 6 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
8 2 7 sylan ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ) → ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
9 eleq1 ⊢ ( 𝑦 = 𝑃 → ( 𝑦 ∈ 𝑢 ↔ 𝑃 ∈ 𝑢 ) )
10 9 anbi1d ⊢ ( 𝑦 = 𝑃 → ( ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
11 10 anbi2d ⊢ ( 𝑦 = 𝑃 → ( ( 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ↔ ( 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ∧ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) )
12 anass ⊢ ( ( ( 𝑢 ∈ 𝐽 ∧ 𝑢 ⊆ 𝑈 ) ∧ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ↔ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑈 ∧ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) )
13 elin ⊢ ( 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ↔ ( 𝑢 ∈ 𝐽 ∧ 𝑢 ∈ 𝒫 𝑈 ) )
14 velpw ⊢ ( 𝑢 ∈ 𝒫 𝑈 ↔ 𝑢 ⊆ 𝑈 )
15 14 anbi2i ⊢ ( ( 𝑢 ∈ 𝐽 ∧ 𝑢 ∈ 𝒫 𝑈 ) ↔ ( 𝑢 ∈ 𝐽 ∧ 𝑢 ⊆ 𝑈 ) )
16 13 15 bitri ⊢ ( 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ↔ ( 𝑢 ∈ 𝐽 ∧ 𝑢 ⊆ 𝑈 ) )
17 16 anbi1i ⊢ ( ( 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ∧ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ↔ ( ( 𝑢 ∈ 𝐽 ∧ 𝑢 ⊆ 𝑈 ) ∧ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
18 3anass ⊢ ( ( 𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ( 𝑢 ⊆ 𝑈 ∧ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
19 18 anbi2i ⊢ ( ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ↔ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑈 ∧ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) )
20 12 17 19 3bitr4i ⊢ ( ( 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ∧ ( 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ↔ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
21 11 20 bitrdi ⊢ ( 𝑦 = 𝑃 → ( ( 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ↔ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) )
22 21 rexbidv2 ⊢ ( 𝑦 = 𝑃 → ( ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
23 22 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑈 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
24 8 23 stoic3 ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )