Metamath Proof Explorer

Theorem elnpi

Description: Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

Ref Expression
Assertion elnpi 
|- ( A e. P. <-> ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. P. -> A e. _V )
2 simpl1 
 |-  ( ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x  A e. _V )
3 psseq2 
 |-  ( z = A -> ( (/) C. z <-> (/) C. A ) )
4 psseq1 
 |-  ( z = A -> ( z C. Q. <-> A C. Q. ) )
5 3 4 anbi12d 
 |-  ( z = A -> ( ( (/) C. z /\ z C. Q. ) <-> ( (/) C. A /\ A C. Q. ) ) )
6 eleq2 
 |-  ( z = A -> ( y e. z <-> y e. A ) )
7 6 imbi2d 
 |-  ( z = A -> ( ( y  y e. z ) <-> ( y  y e. A ) ) )
8 7 albidv 
 |-  ( z = A -> ( A. y ( y  y e. z ) <-> A. y ( y  y e. A ) ) )
9 rexeq 
 |-  ( z = A -> ( E. y e. z x  E. y e. A x
10 8 9 anbi12d 
 |-  ( z = A -> ( ( A. y ( y  y e. z ) /\ E. y e. z x  ( A. y ( y  y e. A ) /\ E. y e. A x
11 10 raleqbi1dv 
 |-  ( z = A -> ( A. x e. z ( A. y ( y  y e. z ) /\ E. y e. z x  A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x
12 5 11 anbi12d 
 |-  ( z = A -> ( ( ( (/) C. z /\ z C. Q. ) /\ A. x e. z ( A. y ( y  y e. z ) /\ E. y e. z x  ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x
13 df-np 
 |-  P. = { z | ( ( (/) C. z /\ z C. Q. ) /\ A. x e. z ( A. y ( y  y e. z ) /\ E. y e. z x
14 12 13 elab2g 
 |-  ( A e. _V -> ( A e. P. <-> ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x
15 id 
 |-  ( ( A e. _V /\ (/) C. A /\ A C. Q. ) -> ( A e. _V /\ (/) C. A /\ A C. Q. ) )
16 15 3expib 
 |-  ( A e. _V -> ( ( (/) C. A /\ A C. Q. ) -> ( A e. _V /\ (/) C. A /\ A C. Q. ) ) )
17 3simpc 
 |-  ( ( A e. _V /\ (/) C. A /\ A C. Q. ) -> ( (/) C. A /\ A C. Q. ) )
18 16 17 impbid1 
 |-  ( A e. _V -> ( ( (/) C. A /\ A C. Q. ) <-> ( A e. _V /\ (/) C. A /\ A C. Q. ) ) )
19 18 anbi1d 
 |-  ( A e. _V -> ( ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x  ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x
20 14 19 bitrd 
 |-  ( A e. _V -> ( A e. P. <-> ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x
21 1 2 20 pm5.21nii 
 |-  ( A e. P. <-> ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x