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 𝐴 = 𝐴 )