hasheq0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hasheq0		Structured version Visualization version GIF version

Theorem hasheq0 14381

Description: Two ways of saying a set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.)

**Assertion**
Ref	Expression
hasheq0	⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))

**Proof of Theorem hasheq0**
Step	Hyp	Ref	Expression
1		pnfnre 11276	. . . . . . 7 ⊢ +∞ ∉ ℝ
2	1	neli 3038	. . . . . 6 ⊢ ¬ +∞ ∈ ℝ
3		hashinf 14353	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞)
4	3	eleq1d 2819	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) ∈ ℝ ↔ +∞ ∈ ℝ))
5	2, 4	mtbiri 327	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) ∈ ℝ)
6		id 22	. . . . . 6 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) = 0)
7		0re 11237	. . . . . 6 ⊢ 0 ∈ ℝ
8	6, 7	eqeltrdi 2842	. . . . 5 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) ∈ ℝ)
9	5, 8	nsyl 140	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) = 0)
10		id 22	. . . . . . 7 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
11		0fi 9056	. . . . . . 7 ⊢ ∅ ∈ Fin
12	10, 11	eqeltrdi 2842	. . . . . 6 ⊢ (𝐴 = ∅ → 𝐴 ∈ Fin)
13	12	con3i 154	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → ¬ 𝐴 = ∅)
14	13	adantl 481	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 = ∅)
15	9, 14	2falsed 376	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))
16	15	ex 412	. 2 ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)))
17		hashen 14365	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ ∅ ∈ Fin) → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
18	11, 17	mpan2 691	. . 3 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
19		fz10 13562	. . . . . 6 ⊢ (1...0) = ∅
20	19	fveq2i 6879	. . . . 5 ⊢ (♯‘(1...0)) = (♯‘∅)
21		0nn0 12516	. . . . . 6 ⊢ 0 ∈ ℕ₀
22		hashfz1 14364	. . . . . 6 ⊢ (0 ∈ ℕ₀ → (♯‘(1...0)) = 0)
23	21, 22	ax-mp 5	. . . . 5 ⊢ (♯‘(1...0)) = 0
24	20, 23	eqtr3i 2760	. . . 4 ⊢ (♯‘∅) = 0
25	24	eqeq2i 2748	. . 3 ⊢ ((♯‘𝐴) = (♯‘∅) ↔ (♯‘𝐴) = 0)
26		en0 9032	. . 3 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
27	18, 25, 26	3bitr3g 313	. 2 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))
28	16, 27	pm2.61d2 181	1 ⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∅c0 4308 class class class wbr 5119 ‘cfv 6531 (class class class)co 7405 ≈ cen 8956 Fincfn 8959 ℝcr 11128 0cc0 11129 1c1 11130 +∞cpnf 11266 ℕ₀cn0 12501 ...cfz 13524 ♯chash 14348

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-er 8719 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-nn 12241 df-n0 12502 df-z 12589 df-uz 12853 df-fz 13525 df-hash 14349

This theorem is referenced by: hashneq0 14382 hashnncl 14384 hash0 14385 hashelne0d 14386 hashgt0 14406 hashle00 14418 seqcoll2 14483 prprrab 14491 hashle2pr 14495 hashge2el2difr 14499 ccat0 14594 ccat1st1st 14646 wrdind 14740 wrd2ind 14741 swrdccat3blem 14757 rev0 14782 repsw0 14795 cshwidx0 14824 fz1f1o 15726 hashbc0 17025 0hashbc 17027 ram0 17042 cshws0 17121 symgvalstruct 19378 gsmsymgrfix 19409 sylow1lem1 19579 sylow1lem4 19582 sylow2blem3 19603 frgpnabllem1 19854 0ringnnzr 20485 01eq0ringOLD 20491 vieta1lem2 26271 tgldimor 28481 uhgr0vsize0 29218 uhgr0edgfi 29219 usgr1v0e 29305 fusgrfisbase 29307 vtxd0nedgb 29468 vtxdusgr0edgnelALT 29476 usgrvd0nedg 29513 vtxdginducedm1lem4 29522 finsumvtxdg2size 29530 cyclnspth 29783 iswwlksnx 29822 umgrclwwlkge2 29972 clwwisshclwws 29996 hashecclwwlkn1 30058 umgrhashecclwwlk 30059 vdn0conngrumgrv2 30177 frgrwopreg 30304 frrusgrord0lem 30320 wlkl0 30348 frgrregord013 30376 frgrregord13 30377 frgrogt3nreg 30378 friendshipgt3 30379 hashne0 32789 wrdt2ind 32929 chnind 32991 chnub 32992 tocyc01 33129 lvecdim0i 33645 hasheuni 34116 signstfvn 34601 signstfveq0a 34608 signshnz 34623 spthcycl 35151 usgrgt2cycl 35152 acycgr1v 35171 umgracycusgr 35176 cusgracyclt3v 35178 elmrsubrn 35542 fsuppind 42613 lindsrng01 48444

W3C validator