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 14277

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 11164	. . . . . . 7 ⊢ +∞ ∉ ℝ
2	1	neli 3035	. . . . . 6 ⊢ ¬ +∞ ∈ ℝ
3		hashinf 14249	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞)
4	3	eleq1d 2818	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) ∈ ℝ ↔ +∞ ∈ ℝ))
5	2, 4	mtbiri 327	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) ∈ ℝ)
6		id 22	. . . . . 6 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) = 0)
7		0re 11125	. . . . . 6 ⊢ 0 ∈ ℝ
8	6, 7	eqeltrdi 2841	. . . . 5 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) ∈ ℝ)
9	5, 8	nsyl 140	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) = 0)
10		id 22	. . . . . . 7 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
11		0fi 8975	. . . . . . 7 ⊢ ∅ ∈ Fin
12	10, 11	eqeltrdi 2841	. . . . . 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 14261	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ ∅ ∈ Fin) → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
18	11, 17	mpan2 691	. . 3 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
19		fz10 13452	. . . . . 6 ⊢ (1...0) = ∅
20	19	fveq2i 6834	. . . . 5 ⊢ (♯‘(1...0)) = (♯‘∅)
21		0nn0 12407	. . . . . 6 ⊢ 0 ∈ ℕ₀
22		hashfz1 14260	. . . . . 6 ⊢ (0 ∈ ℕ₀ → (♯‘(1...0)) = 0)
23	21, 22	ax-mp 5	. . . . 5 ⊢ (♯‘(1...0)) = 0
24	20, 23	eqtr3i 2758	. . . 4 ⊢ (♯‘∅) = 0
25	24	eqeq2i 2746	. . 3 ⊢ ((♯‘𝐴) = (♯‘∅) ↔ (♯‘𝐴) = 0)
26		en0 8951	. . 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 1541 ∈ wcel 2113 ∅c0 4282 class class class wbr 5095 ‘cfv 6489 (class class class)co 7355 ≈ cen 8876 Fincfn 8879 ℝcr 11016 0cc0 11017 1c1 11018 +∞cpnf 11154 ℕ₀cn0 12392 ...cfz 13414 ♯chash 14244

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-om 7806 df-1st 7930 df-2nd 7931 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-er 8631 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-card 9843 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-nn 12137 df-n0 12393 df-z 12480 df-uz 12743 df-fz 13415 df-hash 14245

This theorem is referenced by: hashneq0 14278 hashnncl 14280 hash0 14281 hashelne0d 14282 hashgt0 14302 hashle00 14314 seqcoll2 14379 prprrab 14387 hashle2pr 14391 hashge2el2difr 14395 ccat0 14490 ccat1st1st 14543 wrdind 14636 wrd2ind 14637 swrdccat3blem 14653 rev0 14678 repsw0 14691 cshwidx0 14720 fz1f1o 15624 hashbc0 16924 0hashbc 16926 ram0 16941 cshws0 17020 chnind 18535 chnub 18536 symgvalstruct 19317 gsmsymgrfix 19348 sylow1lem1 19518 sylow1lem4 19521 sylow2blem3 19542 frgpnabllem1 19793 0ringnnzr 20449 01eq0ringOLD 20455 vieta1lem2 26266 tgldimor 28500 uhgr0vsize0 29238 uhgr0edgfi 29239 usgr1v0e 29325 fusgrfisbase 29327 vtxd0nedgb 29488 vtxdusgr0edgnelALT 29496 usgrvd0nedg 29533 vtxdginducedm1lem4 29542 finsumvtxdg2size 29550 cyclnspth 29800 iswwlksnx 29839 umgrclwwlkge2 29992 clwwisshclwws 30016 hashecclwwlkn1 30078 umgrhashecclwwlk 30079 vdn0conngrumgrv2 30197 frgrwopreg 30324 frrusgrord0lem 30340 wlkl0 30368 frgrregord013 30396 frgrregord13 30397 frgrogt3nreg 30398 friendshipgt3 30399 hashne0 32818 wrdt2ind 32963 tocyc01 33128 esplyfval0 33650 vieta 33664 lvecdim0i 33690 hasheuni 34170 signstfvn 34654 signstfveq0a 34661 signshnz 34676 spthcycl 35245 usgrgt2cycl 35246 acycgr1v 35265 umgracycusgr 35270 cusgracyclt3v 35272 elmrsubrn 35636 fsuppind 42748 lindsrng01 48630

W3C validator