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

Metamath Proof Explorer

Theorem nllyeq

Description: Equality theorem for the Locally A predicate. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion nllyeq ( 𝐴 = 𝐵 → 𝑛-Locally 𝐴 = 𝑛-Locally 𝐵 )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( 𝐴 = 𝐵 → ( ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
2 1 rexbidv ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
3 2 2ralbidv ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
4 3 rabbidv ⊢ ( 𝐴 = 𝐵 → { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 } = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 } )
5 df-nlly ⊢ 𝑛-Locally 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 }
6 df-nlly ⊢ 𝑛-Locally 𝐵 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 }
7 4 5 6 3eqtr4g ⊢ ( 𝐴 = 𝐵 → 𝑛-Locally 𝐴 = 𝑛-Locally 𝐵 )