![]() |
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 9563 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simp1 999 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eluz1 9562 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | ibar 301 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitrd 188 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3anass 984 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | bitr4di 198 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 2, 7 | pm5.21nii 705 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4192 ax-pr 4227 ax-cnex 7932 ax-resscn 7933 |
This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-rab 2477 df-v 2754 df-sbc 2978 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-br 4019 df-opab 4080 df-mpt 4081 df-id 4311 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-fv 5243 df-ov 5899 df-neg 8161 df-z 9284 df-uz 9559 |
This theorem is referenced by: eluzuzle 9566 eluzelz 9567 eluzle 9570 uztrn 9574 eluzp1p1 9583 uznn0sub 9589 uz3m2nn 9603 1eluzge0 9604 2eluzge1 9606 raluz2 9609 rexuz2 9611 peano2uz 9613 nn0pzuz 9617 uzind4 9618 nn0ge2m1nnALT 9648 elfzuzb 10049 uzsubsubfz 10077 ige2m1fz 10140 4fvwrd4 10170 elfzo2 10180 elfzouz2 10191 fzossrbm1 10203 fzossfzop1 10242 ssfzo12bi 10255 elfzonelfzo 10260 elfzomelpfzo 10261 fzosplitprm1 10264 fzostep1 10267 fzind2 10269 flqword2 10320 fldiv4p1lem1div2 10336 uzennn 10467 seq3split 10510 iseqf1olemqk 10525 seq3f1olemqsumkj 10529 seq3f1olemqsumk 10530 seq3f1olemqsum 10531 bcval5 10775 seq3coll 10854 seq3shft 10879 resqrexlemoverl 11062 resqrexlemga 11064 fsum3cvg3 11436 fisumrev2 11486 isumshft 11530 cvgratnnlemseq 11566 cvgratnnlemabsle 11567 cvgratnnlemsumlt 11568 cvgratz 11572 oddge22np1 11918 nn0o 11944 suprzubdc 11985 zsupssdc 11987 uzwodc 12070 dvdsnprmd 12157 prmgt1 12164 oddprmgt2 12166 oddprmge3 12167 prm23ge5 12296 nninfdclemcl 12499 nninfdclemp1 12501 nninfdclemlt 12502 strleund 12615 strleun 12616 cnfldstr 13866 2logb9irr 14846 2logb9irrap 14852 lgsdilem2 14895 |
Copyright terms: Public domain | W3C validator |