Metamath Proof Explorer


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 ) )