![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > hasheq0 | Structured version Visualization version GIF version |
Description: Two ways of saying a set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) |
Ref | Expression |
---|---|
hasheq0 | ⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfnre 11237 | . . . . . . 7 ⊢ +∞ ∉ ℝ | |
2 | 1 | neli 3047 | . . . . . 6 ⊢ ¬ +∞ ∈ ℝ |
3 | hashinf 14277 | . . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞) | |
4 | 3 | eleq1d 2817 | . . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) ∈ ℝ ↔ +∞ ∈ ℝ)) |
5 | 2, 4 | mtbiri 326 | . . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) ∈ ℝ) |
6 | id 22 | . . . . . 6 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) = 0) | |
7 | 0re 11198 | . . . . . 6 ⊢ 0 ∈ ℝ | |
8 | 6, 7 | eqeltrdi 2840 | . . . . 5 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) ∈ ℝ) |
9 | 5, 8 | nsyl 140 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) = 0) |
10 | id 22 | . . . . . . 7 ⊢ (𝐴 = ∅ → 𝐴 = ∅) | |
11 | 0fin 9154 | . . . . . . 7 ⊢ ∅ ∈ Fin | |
12 | 10, 11 | eqeltrdi 2840 | . . . . . 6 ⊢ (𝐴 = ∅ → 𝐴 ∈ Fin) |
13 | 12 | con3i 154 | . . . . 5 ⊢ (¬ 𝐴 ∈ Fin → ¬ 𝐴 = ∅) |
14 | 13 | adantl 482 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 = ∅) |
15 | 9, 14 | 2falsed 376 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) |
16 | 15 | ex 413 | . 2 ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))) |
17 | hashen 14289 | . . . 4 ⊢ ((𝐴 ∈ Fin ∧ ∅ ∈ Fin) → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅)) | |
18 | 11, 17 | mpan2 689 | . . 3 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅)) |
19 | fz10 13504 | . . . . . 6 ⊢ (1...0) = ∅ | |
20 | 19 | fveq2i 6881 | . . . . 5 ⊢ (♯‘(1...0)) = (♯‘∅) |
21 | 0nn0 12469 | . . . . . 6 ⊢ 0 ∈ ℕ0 | |
22 | hashfz1 14288 | . . . . . 6 ⊢ (0 ∈ ℕ0 → (♯‘(1...0)) = 0) | |
23 | 21, 22 | ax-mp 5 | . . . . 5 ⊢ (♯‘(1...0)) = 0 |
24 | 20, 23 | eqtr3i 2761 | . . . 4 ⊢ (♯‘∅) = 0 |
25 | 24 | eqeq2i 2744 | . . 3 ⊢ ((♯‘𝐴) = (♯‘∅) ↔ (♯‘𝐴) = 0) |
26 | en0 8996 | . . 3 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) | |
27 | 18, 25, 26 | 3bitr3g 312 | . 2 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) |
28 | 16, 27 | pm2.61d2 181 | 1 ⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∅c0 4318 class class class wbr 5141 ‘cfv 6532 (class class class)co 7393 ≈ cen 8919 Fincfn 8922 ℝcr 11091 0cc0 11092 1c1 11093 +∞cpnf 11227 ℕ0cn0 12454 ...cfz 13466 ♯chash 14272 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7708 ax-cnex 11148 ax-resscn 11149 ax-1cn 11150 ax-icn 11151 ax-addcl 11152 ax-addrcl 11153 ax-mulcl 11154 ax-mulrcl 11155 ax-mulcom 11156 ax-addass 11157 ax-mulass 11158 ax-distr 11159 ax-i2m1 11160 ax-1ne0 11161 ax-1rid 11162 ax-rnegex 11163 ax-rrecex 11164 ax-cnre 11165 ax-pre-lttri 11166 ax-pre-lttrn 11167 ax-pre-ltadd 11168 ax-pre-mulgt0 11169 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-int 4944 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6289 df-ord 6356 df-on 6357 df-lim 6358 df-suc 6359 df-iota 6484 df-fun 6534 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 df-fv 6540 df-riota 7349 df-ov 7396 df-oprab 7397 df-mpo 7398 df-om 7839 df-1st 7957 df-2nd 7958 df-frecs 8248 df-wrecs 8279 df-recs 8353 df-rdg 8392 df-1o 8448 df-er 8686 df-en 8923 df-dom 8924 df-sdom 8925 df-fin 8926 df-card 9916 df-pnf 11232 df-mnf 11233 df-xr 11234 df-ltxr 11235 df-le 11236 df-sub 11428 df-neg 11429 df-nn 12195 df-n0 12455 df-z 12541 df-uz 12805 df-fz 13467 df-hash 14273 |
This theorem is referenced by: hashneq0 14306 hashnncl 14308 hash0 14309 hashelne0d 14310 hashgt0 14330 hashle00 14342 seqcoll2 14408 prprrab 14416 hashle2pr 14420 hashge2el2difr 14424 ccat0 14508 ccat1st1st 14560 wrdind 14654 wrd2ind 14655 swrdccat3blem 14671 rev0 14696 repsw0 14709 cshwidx0 14738 fz1f1o 15638 hashbc0 16920 0hashbc 16922 ram0 16937 cshws0 17017 symgvalstruct 19228 symgvalstructOLD 19229 gsmsymgrfix 19260 sylow1lem1 19430 sylow1lem4 19433 sylow2blem3 19454 frgpnabllem1 19701 0ringnnzr 20252 01eq0ringOLD 20256 vieta1lem2 25753 tgldimor 27618 uhgr0vsize0 28361 uhgr0edgfi 28362 usgr1v0e 28448 fusgrfisbase 28450 vtxd0nedgb 28610 vtxdusgr0edgnelALT 28618 usgrvd0nedg 28655 vtxdginducedm1lem4 28664 finsumvtxdg2size 28672 cyclnspth 28922 iswwlksnx 28959 umgrclwwlkge2 29109 clwwisshclwws 29133 hashecclwwlkn1 29195 umgrhashecclwwlk 29196 vdn0conngrumgrv2 29314 frgrwopreg 29441 frrusgrord0lem 29457 wlkl0 29485 frgrregord013 29513 frgrregord13 29514 frgrogt3nreg 29515 friendshipgt3 29516 wrdt2ind 31988 tocyc01 32148 lvecdim0i 32529 hasheuni 32914 signstfvn 33411 signstfveq0a 33418 signshnz 33433 spthcycl 33951 usgrgt2cycl 33952 acycgr1v 33971 umgracycusgr 33976 cusgracyclt3v 33978 elmrsubrn 34342 fsuppind 40951 lindsrng01 46797 |
Copyright terms: Public domain | W3C validator |