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