![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluzel2 | Unicode version |
Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Ref | Expression |
---|---|
eluzel2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzf 9531 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | frel 5371 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
. . 3
![]() ![]() ![]() |
4 | relelfvdm 5548 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mpan 424 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1 | fdmi 5374 |
. 2
![]() ![]() ![]() ![]() ![]() |
7 | 5, 6 | eleqtrdi 2270 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-14 2151 ax-ext 2159 ax-sep 4122 ax-pow 4175 ax-pr 4210 ax-cnex 7902 ax-resscn 7903 |
This theorem depends on definitions: df-bi 117 df-3or 979 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2740 df-sbc 2964 df-un 3134 df-in 3136 df-ss 3143 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-br 4005 df-opab 4066 df-mpt 4067 df-id 4294 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-fv 5225 df-ov 5878 df-neg 8131 df-z 9254 df-uz 9529 |
This theorem is referenced by: eluz2 9534 uztrn 9544 uzneg 9546 uzss 9548 uz11 9550 eluzadd 9556 uzm1 9558 uzin 9560 uzind4 9588 elfz5 10017 elfzel1 10024 eluzfz1 10031 fzsplit2 10050 fzopth 10061 fzpred 10070 fzpreddisj 10071 fzdifsuc 10081 uzsplit 10092 uzdisj 10093 elfzp12 10099 fzm1 10100 uznfz 10103 nn0disj 10138 fzolb 10153 fzoss2 10172 fzouzdisj 10180 ige2m2fzo 10198 elfzonelfzo 10230 frec2uzrand 10405 frecfzen2 10427 seq3p1 10462 seqp1cd 10466 seq3clss 10467 seq3feq2 10470 seq3fveq 10471 seq3shft2 10473 ser3mono 10478 seq3split 10479 seq3caopr3 10481 seq3caopr2 10482 seq3f1olemp 10502 seq3f1oleml 10503 seq3f1o 10504 seq3id3 10507 seq3id 10508 seq3homo 10510 seq3z 10511 seq3distr 10513 ser3ge0 10517 ser3le 10518 leexp2a 10573 hashfz 10801 hashfzo 10802 hashfzp1 10804 seq3coll 10822 rexanuz2 11000 cau4 11125 clim2ser 11345 clim2ser2 11346 climserle 11353 fsum3cvg 11386 fsum3cvg2 11402 fsumsersdc 11403 fsum3ser 11405 fsumm1 11424 fsum1p 11426 telfsumo 11474 fsumparts 11478 cvgcmpub 11484 isumsplit 11499 cvgratnnlemmn 11533 clim2prod 11547 clim2divap 11548 prodfrecap 11554 prodfdivap 11555 ntrivcvgap 11556 fproddccvg 11580 fprodm1 11606 fprodabs 11624 fprodeq0 11625 uzwodc 12038 pcaddlem 12338 inffz 14822 |
Copyright terms: Public domain | W3C validator |