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 = w -> ( (/) C. z <-> (/) C. w ) )
4 psseq1 
 |-  ( z = w -> ( z C. Q. <-> w C. Q. ) )
5 3 4 anbi12d 
 |-  ( z = w -> ( ( (/) C. z /\ z C. Q. ) <-> ( (/) C. w /\ w C. Q. ) ) )
6 elequ2 
 |-  ( z = w -> ( y e. z <-> y e. w ) )
7 6 imbi2d 
 |-  ( z = w -> ( ( y  y e. z ) <-> ( y  y e. w ) ) )
8 7 albidv 
 |-  ( z = w -> ( A. y ( y  y e. z ) <-> A. y ( y  y e. w ) ) )
9 rexeq 
 |-  ( z = w -> ( E. y e. z x  E. y e. w x
10 8 9 anbi12d 
 |-  ( z = w -> ( ( A. y ( y  y e. z ) /\ E. y e. z x  ( A. y ( y  y e. w ) /\ E. y e. w x
11 10 raleqbi1dv 
 |-  ( z = w -> ( A. x e. z ( A. y ( y  y e. z ) /\ E. y e. z x  A. x e. w ( A. y ( y  y e. w ) /\ E. y e. w x
12 5 11 anbi12d 
 |-  ( z = w -> ( ( ( (/) C. z /\ z C. Q. ) /\ A. x e. z ( A. y ( y  y e. z ) /\ E. y e. z x  ( ( (/) C. w /\ w C. Q. ) /\ A. x e. w ( A. y ( y  y e. w ) /\ E. y e. w x
13 psseq2 
 |-  ( w = A -> ( (/) C. w <-> (/) C. A ) )
14 psseq1 
 |-  ( w = A -> ( w C. Q. <-> A C. Q. ) )
15 13 14 anbi12d 
 |-  ( w = A -> ( ( (/) C. w /\ w C. Q. ) <-> ( (/) C. A /\ A C. Q. ) ) )
16 eleq2 
 |-  ( w = A -> ( y e. w <-> y e. A ) )
17 16 imbi2d 
 |-  ( w = A -> ( ( y  y e. w ) <-> ( y  y e. A ) ) )
18 17 albidv 
 |-  ( w = A -> ( A. y ( y  y e. w ) <-> A. y ( y  y e. A ) ) )
19 rexeq 
 |-  ( w = A -> ( E. y e. w x  E. y e. A x
20 18 19 anbi12d 
 |-  ( w = A -> ( ( A. y ( y  y e. w ) /\ E. y e. w x  ( A. y ( y  y e. A ) /\ E. y e. A x
21 20 raleqbi1dv 
 |-  ( w = A -> ( A. x e. w ( A. y ( y  y e. w ) /\ E. y e. w x  A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x
22 15 21 anbi12d 
 |-  ( w = A -> ( ( ( (/) C. w /\ w C. Q. ) /\ A. x e. w ( A. y ( y  y e. w ) /\ E. y e. w x  ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x
23 df-np 
 |-  P. = { z | ( ( (/) C. z /\ z C. Q. ) /\ A. x e. z ( A. y ( y  y e. z ) /\ E. y e. z x
24 12 22 23 elab2gw 
 |-  ( 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
25 id 
 |-  ( ( A e. _V /\ (/) C. A /\ A C. Q. ) -> ( A e. _V /\ (/) C. A /\ A C. Q. ) )
26 25 3expib 
 |-  ( A e. _V -> ( ( (/) C. A /\ A C. Q. ) -> ( A e. _V /\ (/) C. A /\ A C. Q. ) ) )
27 3simpc 
 |-  ( ( A e. _V /\ (/) C. A /\ A C. Q. ) -> ( (/) C. A /\ A C. Q. ) )
28 26 27 impbid1 
 |-  ( A e. _V -> ( ( (/) C. A /\ A C. Q. ) <-> ( A e. _V /\ (/) C. A /\ A C. Q. ) ) )
29 28 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
30 24 29 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
31 1 2 30 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