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 A = A ↔ N-Locally A = A

Proof

Step Hyp Ref Expression
1 simprl ⊢ Locally A = A ∧ j ∈ A ∧ x ∈ j → j ∈ A
2 simpl ⊢ Locally A = A ∧ j ∈ A ∧ x ∈ j → Locally A = A
3 1 2 eleqtrrd ⊢ Locally A = A ∧ j ∈ A ∧ x ∈ j → j ∈ Locally A
4 simprr ⊢ Locally A = A ∧ j ∈ A ∧ x ∈ j → x ∈ j
5 llyrest ⊢ j ∈ Locally A ∧ x ∈ j → j ↾ 𝑡 x ∈ Locally A
6 3 4 5 syl2anc ⊢ Locally A = A ∧ j ∈ A ∧ x ∈ j → j ↾ 𝑡 x ∈ Locally A
7 6 2 eleqtrd ⊢ Locally A = A ∧ j ∈ A ∧ x ∈ j → j ↾ 𝑡 x ∈ A
8 7 restnlly ⊢ Locally A = A → N-Locally A = Locally A
9 id ⊢ Locally A = A → Locally A = A
10 8 9 eqtrd ⊢ Locally A = A → N-Locally A = A
11 simprl ⊢ N-Locally A = A ∧ j ∈ A ∧ x ∈ j → j ∈ A
12 simpl ⊢ N-Locally A = A ∧ j ∈ A ∧ x ∈ j → N-Locally A = A
13 11 12 eleqtrrd ⊢ N-Locally A = A ∧ j ∈ A ∧ x ∈ j → j ∈ N-Locally A
14 simprr ⊢ N-Locally A = A ∧ j ∈ A ∧ x ∈ j → x ∈ j
15 nllyrest ⊢ j ∈ N-Locally A ∧ x ∈ j → j ↾ 𝑡 x ∈ N-Locally A
16 13 14 15 syl2anc ⊢ N-Locally A = A ∧ j ∈ A ∧ x ∈ j → j ↾ 𝑡 x ∈ N-Locally A
17 16 12 eleqtrd ⊢ N-Locally A = A ∧ j ∈ A ∧ x ∈ j → j ↾ 𝑡 x ∈ A
18 17 restnlly ⊢ N-Locally A = A → N-Locally A = Locally A
19 id ⊢ N-Locally A = A → N-Locally A = A
20 18 19 eqtr3d ⊢ N-Locally A = A → Locally A = A
21 10 20 impbii ⊢ Locally A = A ↔ N-Locally A = A