![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluz2 | Unicode version |
Description: Membership in an upper
set of integers. We use the fact that a
function's value (under our function value definition) is empty outside
of its domain to show ![]() ![]() ![]() |
Ref | Expression |
---|---|
eluz2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluzel2 9233 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simp1 964 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eluz1 9232 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | ibar 297 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitrd 187 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3anass 949 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | syl6bbr 197 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 2, 7 | pm5.21nii 676 |
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-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-pow 4058 ax-pr 4091 ax-cnex 7636 ax-resscn 7637 |
This theorem depends on definitions: df-bi 116 df-3or 946 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-rab 2399 df-v 2659 df-sbc 2879 df-un 3041 df-in 3043 df-ss 3050 df-pw 3478 df-sn 3499 df-pr 3500 df-op 3502 df-uni 3703 df-br 3896 df-opab 3950 df-mpt 3951 df-id 4175 df-xp 4505 df-rel 4506 df-cnv 4507 df-co 4508 df-dm 4509 df-rn 4510 df-res 4511 df-ima 4512 df-iota 5046 df-fun 5083 df-fn 5084 df-f 5085 df-fv 5089 df-ov 5731 df-neg 7859 df-z 8959 df-uz 9229 |
This theorem is referenced by: eluzuzle 9236 eluzelz 9237 eluzle 9240 uztrn 9244 eluzp1p1 9253 uznn0sub 9259 uz3m2nn 9270 1eluzge0 9271 2eluzge1 9273 raluz2 9276 rexuz2 9278 peano2uz 9280 nn0pzuz 9284 uzind4 9285 nn0ge2m1nnALT 9312 elfzuzb 9693 uzsubsubfz 9720 ige2m1fz 9783 4fvwrd4 9810 elfzo2 9820 elfzouz2 9831 fzossrbm1 9843 fzossfzop1 9882 ssfzo12bi 9895 elfzonelfzo 9900 elfzomelpfzo 9901 fzosplitprm1 9904 fzostep1 9907 fzind2 9909 flqword2 9955 fldiv4p1lem1div2 9971 uzennn 10102 seq3split 10145 iseqf1olemqk 10160 seq3f1olemqsumkj 10164 seq3f1olemqsumk 10165 seq3f1olemqsum 10166 bcval5 10402 seq3coll 10478 seq3shft 10503 resqrexlemoverl 10685 resqrexlemga 10687 fsum3cvg3 11057 fisumrev2 11107 isumshft 11151 cvgratnnlemseq 11187 cvgratnnlemabsle 11188 cvgratnnlemsumlt 11189 cvgratz 11193 oddge22np1 11426 nn0o 11452 dvdsnprmd 11652 prmgt1 11658 oddprmgt2 11660 oddprmge3 11661 strleund 11890 strleun 11891 |
Copyright terms: Public domain | W3C validator |