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