Metamath Proof Explorer

Theorem prpssnq

Description: A positive real is a subset of the positive fractions. (Contributed by NM, 29-Feb-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	prpssnq	\|- ( A e. P. -> A C. Q. )

Proof

Step	Hyp	Ref	Expression
1		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
2		simpl3	\|- ( ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x A C. Q. )
3	1 2	sylbi	\|- ( A e. P. -> A C. Q. )

Step

Hyp

Ref

Expression

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

simpl3

 |-  ( ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x  A C. Q. )

1 2

sylbi

 |-  ( A e. P. -> A C. Q. )