Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prcdnq Structured version   Unicode version

Theorem prcdnq 8863
 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.)
Assertion
Ref Expression
prcdnq

Proof of Theorem prcdnq
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 8796 . . . . . . 7
2 relxp 4976 . . . . . . 7
3 relss 4956 . . . . . . 7
41, 2, 3mp2 9 . . . . . 6
54brrelexi 4911 . . . . 5
6 eleq1 2496 . . . . . . . . 9
76anbi2d 685 . . . . . . . 8
8 breq2 4209 . . . . . . . 8
97, 8anbi12d 692 . . . . . . 7
109imbi1d 309 . . . . . 6
11 breq1 4208 . . . . . . . 8
1211anbi2d 685 . . . . . . 7
13 eleq1 2496 . . . . . . 7
1412, 13imbi12d 312 . . . . . 6
15 elnpi 8858 . . . . . . . . . . 11
1615simprbi 451 . . . . . . . . . 10
1716r19.21bi 2797 . . . . . . . . 9
1817simpld 446 . . . . . . . 8
191819.21bi 1774 . . . . . . 7
2019imp 419 . . . . . 6
2110, 14, 20vtocl2g 3008 . . . . 5
225, 21sylan2 461 . . . 4