![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elprnql | GIF version |
Description: An element of a positive real's lower cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.) |
Ref | Expression |
---|---|
elprnql | ⊢ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝐵 ∈ 𝐿) → 𝐵 ∈ Q) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prssnql 6959 | . 2 ⊢ (〈𝐿, 𝑈〉 ∈ P → 𝐿 ⊆ Q) | |
2 | 1 | sselda 3012 | 1 ⊢ ((〈𝐿, 𝑈〉 ∈ P ∧ 𝐵 ∈ 𝐿) → 𝐵 ∈ Q) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∈ wcel 1436 〈cop 3428 Qcnq 6760 Pcnp 6771 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-13 1447 ax-14 1448 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 ax-coll 3922 ax-sep 3925 ax-pow 3977 ax-pr 4003 ax-un 4227 ax-iinf 4369 |
This theorem depends on definitions: df-bi 115 df-3an 924 df-tru 1290 df-nf 1393 df-sb 1690 df-eu 1948 df-mo 1949 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-ral 2360 df-rex 2361 df-reu 2362 df-rab 2364 df-v 2616 df-sbc 2829 df-csb 2922 df-dif 2988 df-un 2990 df-in 2992 df-ss 2999 df-pw 3411 df-sn 3431 df-pr 3432 df-op 3434 df-uni 3631 df-int 3666 df-iun 3709 df-br 3815 df-opab 3869 df-mpt 3870 df-id 4087 df-iom 4372 df-xp 4410 df-rel 4411 df-cnv 4412 df-co 4413 df-dm 4414 df-rn 4415 df-res 4416 df-ima 4417 df-iota 4937 df-fun 4974 df-fn 4975 df-f 4976 df-f1 4977 df-fo 4978 df-f1o 4979 df-fv 4980 df-qs 6231 df-ni 6784 df-nqqs 6828 df-inp 6946 |
This theorem is referenced by: prubl 6966 prnmaxl 6968 prarloclemlt 6973 prarloclemlo 6974 prarloclem5 6980 genpdf 6988 genipv 6989 genpelvl 6992 genpml 6997 genprndl 7001 genpassl 7004 addnqprllem 7007 addnqprl 7009 addlocprlemeqgt 7012 addlocprlemgt 7014 addlocprlem 7015 nqprl 7031 prmuloc 7046 mulnqprl 7048 addcomprg 7058 mulcomprg 7060 distrlem1prl 7062 distrlem4prl 7064 1idprl 7070 ltsopr 7076 ltexprlemm 7080 ltexprlemopl 7081 ltexprlemopu 7083 ltexprlemupu 7084 ltexprlemdisj 7086 ltexprlemloc 7087 ltexprlemfl 7089 ltexprlemrl 7090 ltexprlemfu 7091 ltexprlemru 7092 addcanprleml 7094 addcanprlemu 7095 recexprlemloc 7111 recexprlem1ssl 7113 recexprlem1ssu 7114 recexprlemss1l 7115 aptiprleml 7119 aptiprlemu 7120 caucvgprprlemopl 7177 |
Copyright terms: Public domain | W3C validator |