This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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