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

Metamath Proof Explorer

Theorem loclly

Description: If A is a local property, then both Locally A and N-Locally A simplify to A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion loclly ( Locally 𝐴 = 𝐴 ↔ 𝑛-Locally 𝐴 = 𝐴 )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → 𝑗 ∈ 𝐴 )
2 simpl ⊢ ( ( Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → Locally 𝐴 = 𝐴 )
3 1 2 eleqtrrd ⊢ ( ( Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → 𝑗 ∈ Locally 𝐴 )
4 simprr ⊢ ( ( Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → 𝑥 ∈ 𝑗 )
5 llyrest ⊢ ( ( 𝑗 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ Locally 𝐴 )
6 3 4 5 syl2anc ⊢ ( ( Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ Locally 𝐴 )
7 6 2 eleqtrd ⊢ ( ( Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 )
8 7 restnlly ⊢ ( Locally 𝐴 = 𝐴 → 𝑛-Locally 𝐴 = Locally 𝐴 )
9 id ⊢ ( Locally 𝐴 = 𝐴 → Locally 𝐴 = 𝐴 )
10 8 9 eqtrd ⊢ ( Locally 𝐴 = 𝐴 → 𝑛-Locally 𝐴 = 𝐴 )
11 simprl ⊢ ( ( 𝑛-Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → 𝑗 ∈ 𝐴 )
12 simpl ⊢ ( ( 𝑛-Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → 𝑛-Locally 𝐴 = 𝐴 )
13 11 12 eleqtrrd ⊢ ( ( 𝑛-Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → 𝑗 ∈ 𝑛-Locally 𝐴 )
14 simprr ⊢ ( ( 𝑛-Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → 𝑥 ∈ 𝑗 )
15 nllyrest ⊢ ( ( 𝑗 ∈ 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝑛-Locally 𝐴 )
16 13 14 15 syl2anc ⊢ ( ( 𝑛-Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝑛-Locally 𝐴 )
17 16 12 eleqtrd ⊢ ( ( 𝑛-Locally 𝐴 = 𝐴 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 )
18 17 restnlly ⊢ ( 𝑛-Locally 𝐴 = 𝐴 → 𝑛-Locally 𝐴 = Locally 𝐴 )
19 id ⊢ ( 𝑛-Locally 𝐴 = 𝐴 → 𝑛-Locally 𝐴 = 𝐴 )
20 18 19 eqtr3d ⊢ ( 𝑛-Locally 𝐴 = 𝐴 → Locally 𝐴 = 𝐴 )
21 10 20 impbii ⊢ ( Locally 𝐴 = 𝐴 ↔ 𝑛-Locally 𝐴 = 𝐴 )