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

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( Locally A = A /\ ( j e. A /\ x e. j ) ) -> j e. A )
2 simpl 
 |-  ( ( Locally A = A /\ ( j e. A /\ x e. j ) ) -> Locally A = A )
3 1 2 eleqtrrd 
 |-  ( ( Locally A = A /\ ( j e. A /\ x e. j ) ) -> j e. Locally A )
4 simprr 
 |-  ( ( Locally A = A /\ ( j e. A /\ x e. j ) ) -> x e. j )
5 llyrest 
 |-  ( ( j e. Locally A /\ x e. j ) -> ( j |`t x ) e. Locally A )
6 3 4 5 syl2anc 
 |-  ( ( Locally A = A /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. Locally A )
7 6 2 eleqtrd 
 |-  ( ( Locally A = A /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. 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 e. A /\ x e. j ) ) -> j e. A )
12 simpl 
 |-  ( ( N-Locally A = A /\ ( j e. A /\ x e. j ) ) -> N-Locally A = A )
13 11 12 eleqtrrd 
 |-  ( ( N-Locally A = A /\ ( j e. A /\ x e. j ) ) -> j e. N-Locally A )
14 simprr 
 |-  ( ( N-Locally A = A /\ ( j e. A /\ x e. j ) ) -> x e. j )
15 nllyrest 
 |-  ( ( j e. N-Locally A /\ x e. j ) -> ( j |`t x ) e. N-Locally A )
16 13 14 15 syl2anc 
 |-  ( ( N-Locally A = A /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. N-Locally A )
17 16 12 eleqtrd 
 |-  ( ( N-Locally A = A /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. 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 )