![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > hasheq0 | Structured version Unicode version |
Description: Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) |
Ref | Expression |
---|---|
hasheq0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfnre 9539 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
2 | 1 | neli 2787 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() |
3 | hashinf 12228 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | eleq1d 2523 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | mtbiri 303 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | id 22 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 0re 9500 |
. . . . . 6
![]() ![]() ![]() ![]() | |
8 | 6, 7 | syl6eqel 2550 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 5, 8 | nsyl 121 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | id 22 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 0fin 7654 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
12 | 10, 11 | syl6eqel 2550 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 12 | con3i 135 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13 | adantl 466 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 9, 14 | 2falsed 351 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15 | ex 434 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | hashen 12238 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | 11, 17 | mpan2 671 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | fz10 11590 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
20 | 19 | fveq2i 5805 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 0nn0 10708 |
. . . . . 6
![]() ![]() ![]() ![]() | |
22 | hashfz1 12237 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
23 | 21, 22 | ax-mp 5 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 20, 23 | eqtr3i 2485 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 24 | eqeq2i 2472 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | en0 7485 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
27 | 18, 25, 26 | 3bitr3g 287 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
28 | 16, 27 | pm2.61d2 160 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485 ax-cnex 9452 ax-resscn 9453 ax-1cn 9454 ax-icn 9455 ax-addcl 9456 ax-addrcl 9457 ax-mulcl 9458 ax-mulrcl 9459 ax-mulcom 9460 ax-addass 9461 ax-mulass 9462 ax-distr 9463 ax-i2m1 9464 ax-1ne0 9465 ax-1rid 9466 ax-rnegex 9467 ax-rrecex 9468 ax-cnre 9469 ax-pre-lttri 9470 ax-pre-lttrn 9471 ax-pre-ltadd 9472 ax-pre-mulgt0 9473 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-nel 2651 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-pss 3455 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-tp 3993 df-op 3995 df-uni 4203 df-int 4240 df-iun 4284 df-br 4404 df-opab 4462 df-mpt 4463 df-tr 4497 df-eprel 4743 df-id 4747 df-po 4752 df-so 4753 df-fr 4790 df-we 4792 df-ord 4833 df-on 4834 df-lim 4835 df-suc 4836 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-riota 6164 df-ov 6206 df-oprab 6207 df-mpt2 6208 df-om 6590 df-1st 6690 df-2nd 6691 df-recs 6945 df-rdg 6979 df-1o 7033 df-er 7214 df-en 7424 df-dom 7425 df-sdom 7426 df-fin 7427 df-card 8223 df-pnf 9534 df-mnf 9535 df-xr 9536 df-ltxr 9537 df-le 9538 df-sub 9711 df-neg 9712 df-nn 10437 df-n0 10694 df-z 10761 df-uz 10976 df-fz 11558 df-hash 12224 |
This theorem is referenced by: hashneq0 12252 hashnncl 12254 hash0 12255 hashgt0 12272 hashle00 12279 seqcoll2 12338 lswcl 12391 wrdind 12492 wrd2ind 12493 swrdccat3a 12506 swrdccat3blem 12507 rev0 12525 repsw0 12536 cshwidx0 12563 fz1f1o 13308 hashbc0 14187 0hashbc 14189 ram0 14204 cshws0 14249 gsmsymgrfix 16055 sylow1lem1 16221 sylow1lem4 16224 sylow2blem3 16245 frgpnabllem1 16475 vieta1lem2 21913 tgldimor 23093 isusgra0 23447 usgrafisindb0 23493 vdusgra0nedg 23750 usgravd0nedg 23754 hasheuni 26699 signstfvn 27134 signstfveq0a 27141 signshnz 27156 wwlkn0s 30507 clwwlkgt0 30602 hashecclwwlkn1 30676 usghashecclwwlk 30677 vdn0frgrav2 30784 vdgn0frgrav2 30785 frgrawopreg 30810 frgregordn0 30831 frgrareg 30878 frgraregord013 30879 frgraregord13 30880 frgraogt3nreg 30881 friendshipgt3 30882 01eq0rng 30945 0rngnnzr 30946 lindsrng01 31154 |
Copyright terms: Public domain | W3C validator |