Theorem elnp

Description: Membership in positive reals. (Contributed by NM, 16-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	elnp	|- ( A e. P. <-> ( ( (/) 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		pssss	|- ( A C. Q. -> A C_ Q. )
3		nqex	|- Q. e. _V
4	3	ssex	|- ( A C_ Q. -> A e. _V )
5	2 4	syl	|- ( A C. Q. -> A e. _V )
6	5	ad2antlr	|- ( ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x A e. _V )
7		psseq2	|- ( z = A -> ( (/) C. z <-> (/) C. A ) )
8		psseq1	|- ( z = A -> ( z C. Q. <-> A C. Q. ) )
9	7 8	anbi12d	|- ( z = A -> ( ( (/) C. z /\ z C. Q. ) <-> ( (/) C. A /\ A C. Q. ) ) )
10		eleq2	|- ( z = A -> ( y e. z <-> y e. A ) )
11	10	imbi2d	|- ( z = A -> ( ( y y e. z ) <-> ( y y e. A ) ) )
12	11	albidv	|- ( z = A -> ( A. y ( y y e. z ) <-> A. y ( y y e. A ) ) )
13		rexeq	|- ( z = A -> ( E. y e. z x E. y e. A x
14	12 13	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
15	14	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
16	9 15	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
17		df-np	|- P. = { z | ( ( (/) C. z /\ z C. Q. ) /\ A. x e. z ( A. y ( y y e. z ) /\ E. y e. z x
18	16 17	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
19	1 6 18	pm5.21nii	|- ( A e. P. <-> ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x