![]() |
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 8852 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | leidd 8089 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ancli 317 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eluz1 9122 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mpbird 166 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-cnex 7533 ax-resscn 7534 ax-pre-ltirr 7554 |
This theorem depends on definitions: df-bi 116 df-3or 928 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-nel 2358 df-ral 2375 df-rex 2376 df-rab 2379 df-v 2635 df-sbc 2855 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-opab 3922 df-mpt 3923 df-id 4144 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-iota 5014 df-fun 5051 df-fv 5057 df-ov 5693 df-pnf 7621 df-mnf 7622 df-xr 7623 df-ltxr 7624 df-le 7625 df-neg 7753 df-z 8849 df-uz 9119 |
This theorem is referenced by: uzn0 9133 uz11 9140 eluzfz1 9594 eluzfz2 9595 elfz3 9597 elfz1end 9618 fzssp1 9630 fzpred 9633 fzp1ss 9636 fzpr 9640 fztp 9641 elfz0add 9683 fzolb 9713 zpnn0elfzo 9767 fzosplitsnm1 9769 fzofzp1 9787 fzosplitsn 9793 fzostep1 9797 frec2uzuzd 9958 frecuzrdgrrn 9964 frec2uzrdg 9965 frecuzrdgrcl 9966 frecuzrdgsuc 9970 frecuzrdgrclt 9971 frecuzrdgg 9972 frecuzrdgsuctlem 9979 uzsinds 9997 seq3val 10013 seq3-1 10014 seqf 10015 seq3p1 10016 seq3fveq 10021 seq3-1p 10030 seq3caopr3 10031 iseqf1olemjpcl 10045 iseqf1olemqpcl 10046 seq3f1oleml 10053 seq3f1o 10054 seq3homo 10060 faclbnd3 10266 bcm1k 10283 bcn2 10287 seq3coll 10362 rexuz3 10538 r19.2uz 10541 resqrexlemcvg 10567 resqrexlemgt0 10568 resqrexlemoverl 10569 cau3lem 10662 caubnd2 10665 climconst 10833 climuni 10836 climcau 10890 serf0 10895 fsumparts 11013 isum1p 11035 isumrpcl 11037 cvgratz 11075 mertenslemi1 11078 eftlub 11129 zsupcllemstep 11368 zsupcllemex 11369 ialgr0 11453 eucalg 11468 pw2dvds 11571 lmconst 12067 |
Copyright terms: Public domain | W3C validator |