Theorem prcdnq

Description: A positive real is closed downwards under the positive fractions. Definition 9-3.1 (ii) of Gleason p. 121. (Contributed by NM, 25-Feb-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	prcdnq	|- ( ( A e. P. /\ B e. A ) -> ( C C e. A ) )

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	|-
2		relxp	|- Rel ( Q. X. Q. )
3		relss	|- ( ( Rel ( Q. X. Q. ) -> Rel
4	1 2 3	mp2	|- Rel
5	4	brrelex1i	|- ( C C e. _V )
6		eleq1	|- ( x = B -> ( x e. A <-> B e. A ) )
7	6	anbi2d	|- ( x = B -> ( ( A e. P. /\ x e. A ) <-> ( A e. P. /\ B e. A ) ) )
8		breq2	|- ( x = B -> ( y y
9	7 8	anbi12d	|- ( x = B -> ( ( ( A e. P. /\ x e. A ) /\ y ( ( A e. P. /\ B e. A ) /\ y
10	9	imbi1d	|- ( x = B -> ( ( ( ( A e. P. /\ x e. A ) /\ y y e. A ) <-> ( ( ( A e. P. /\ B e. A ) /\ y y e. A ) ) )
11		breq1	|- ( y = C -> ( y C
12	11	anbi2d	|- ( y = C -> ( ( ( A e. P. /\ B e. A ) /\ y ( ( A e. P. /\ B e. A ) /\ C
13		eleq1	|- ( y = C -> ( y e. A <-> C e. A ) )
14	12 13	imbi12d	|- ( y = C -> ( ( ( ( A e. P. /\ B e. A ) /\ y y e. A ) <-> ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) ) )
15		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
16	15	simprbi	|- ( A e. P. -> A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x
17	16	r19.21bi	|- ( ( A e. P. /\ x e. A ) -> ( A. y ( y y e. A ) /\ E. y e. A x
18	17	simpld	|- ( ( A e. P. /\ x e. A ) -> A. y ( y y e. A ) )
19	18	19.21bi	|- ( ( A e. P. /\ x e. A ) -> ( y y e. A ) )
20	19	imp	|- ( ( ( A e. P. /\ x e. A ) /\ y y e. A )
21	10 14 20	vtocl2g	|- ( ( B e. A /\ C e. _V ) -> ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) )
22	5 21	sylan2	|- ( ( B e. A /\ C ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) )
23	22	adantll	|- ( ( ( A e. P. /\ B e. A ) /\ C ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) )
24	23	pm2.43i	|- ( ( ( A e. P. /\ B e. A ) /\ C C e. A )
25	24	ex	|- ( ( A e. P. /\ B e. A ) -> ( C C e. A ) )