This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem islly

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

Ref Expression
Assertion islly ( 𝐽 ∈ Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ineq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∩ 𝒫 𝑥 ) = ( 𝐽 ∩ 𝒫 𝑥 ) )
2 oveq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ↾t 𝑢 ) = ( 𝐽 ↾t 𝑢 ) )
3 2 eleq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
4 3 anbi2d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
5 1 4 rexeqbidv ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
6 5 ralbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
7 6 raleqbi1dv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
8 df-lly ⊢ Locally 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) }
9 7 8 elrab2 ⊢ ( 𝐽 ∈ Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )