Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > uzid | Unicode version |
Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
Ref | Expression |
---|---|
uzid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre 9026 | . . . 4 | |
2 | 1 | leidd 8244 | . . 3 |
3 | 2 | ancli 321 | . 2 |
4 | eluz1 9298 | . 2 | |
5 | 3, 4 | mpbird 166 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1465 class class class wbr 3899 cfv 5093 cle 7769 cz 9022 cuz 9294 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 588 ax-in2 589 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-13 1476 ax-14 1477 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-sep 4016 ax-pow 4068 ax-pr 4101 ax-un 4325 ax-setind 4422 ax-cnex 7679 ax-resscn 7680 ax-pre-ltirr 7700 |
This theorem depends on definitions: df-bi 116 df-3or 948 df-3an 949 df-tru 1319 df-fal 1322 df-nf 1422 df-sb 1721 df-eu 1980 df-mo 1981 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-ne 2286 df-nel 2381 df-ral 2398 df-rex 2399 df-rab 2402 df-v 2662 df-sbc 2883 df-dif 3043 df-un 3045 df-in 3047 df-ss 3054 df-pw 3482 df-sn 3503 df-pr 3504 df-op 3506 df-uni 3707 df-br 3900 df-opab 3960 df-mpt 3961 df-id 4185 df-xp 4515 df-rel 4516 df-cnv 4517 df-co 4518 df-dm 4519 df-iota 5058 df-fun 5095 df-fv 5101 df-ov 5745 df-pnf 7770 df-mnf 7771 df-xr 7772 df-ltxr 7773 df-le 7774 df-neg 7904 df-z 9023 df-uz 9295 |
This theorem is referenced by: uzn0 9309 uz11 9316 eluzfz1 9779 eluzfz2 9780 elfz3 9782 elfz1end 9803 fzssp1 9815 fzpred 9818 fzp1ss 9821 fzpr 9825 fztp 9826 elfz0add 9868 fzolb 9898 zpnn0elfzo 9952 fzosplitsnm1 9954 fzofzp1 9972 fzosplitsn 9978 fzostep1 9982 frec2uzuzd 10143 frecuzrdgrrn 10149 frec2uzrdg 10150 frecuzrdgrcl 10151 frecuzrdgsuc 10155 frecuzrdgrclt 10156 frecuzrdgg 10157 frecuzrdgsuctlem 10164 uzsinds 10183 seq3val 10199 seqvalcd 10200 seq3-1 10201 seqf 10202 seq3p1 10203 seq3fveq 10212 seq3-1p 10221 seq3caopr3 10222 iseqf1olemjpcl 10236 iseqf1olemqpcl 10237 seq3f1oleml 10244 seq3f1o 10245 seq3homo 10251 faclbnd3 10457 bcm1k 10474 bcn2 10478 seq3coll 10553 rexuz3 10730 r19.2uz 10733 resqrexlemcvg 10759 resqrexlemgt0 10760 resqrexlemoverl 10761 cau3lem 10854 caubnd2 10857 climconst 11027 climuni 11030 climcau 11084 serf0 11089 fsumparts 11207 isum1p 11229 isumrpcl 11231 cvgratz 11269 mertenslemi1 11272 eftlub 11323 zsupcllemstep 11565 zsupcllemex 11566 ialgr0 11652 eucalg 11667 pw2dvds 11771 ennnfonelem1 11847 lmconst 12312 cvgcmp2nlemabs 13154 trilpolemlt1 13161 |
Copyright terms: Public domain | W3C validator |