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 14298

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 11185	. . . . . . 7 ⊢ +∞ ∉ ℝ
2	1	neli 3039	. . . . . 6 ⊢ ¬ +∞ ∈ ℝ
3		hashinf 14270	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞)
4	3	eleq1d 2822	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) ∈ ℝ ↔ +∞ ∈ ℝ))
5	2, 4	mtbiri 327	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) ∈ ℝ)
6		id 22	. . . . . 6 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) = 0)
7		0re 11146	. . . . . 6 ⊢ 0 ∈ ℝ
8	6, 7	eqeltrdi 2845	. . . . 5 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) ∈ ℝ)
9	5, 8	nsyl 140	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) = 0)
10		id 22	. . . . . . 7 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
11		0fi 8991	. . . . . . 7 ⊢ ∅ ∈ Fin
12	10, 11	eqeltrdi 2845	. . . . . 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 14282	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ ∅ ∈ Fin) → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
18	11, 17	mpan2 692	. . 3 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
19		fz10 13473	. . . . . 6 ⊢ (1...0) = ∅
20	19	fveq2i 6845	. . . . 5 ⊢ (♯‘(1...0)) = (♯‘∅)
21		0nn0 12428	. . . . . 6 ⊢ 0 ∈ ℕ₀
22		hashfz1 14281	. . . . . 6 ⊢ (0 ∈ ℕ₀ → (♯‘(1...0)) = 0)
23	21, 22	ax-mp 5	. . . . 5 ⊢ (♯‘(1...0)) = 0
24	20, 23	eqtr3i 2762	. . . 4 ⊢ (♯‘∅) = 0
25	24	eqeq2i 2750	. . 3 ⊢ ((♯‘𝐴) = (♯‘∅) ↔ (♯‘𝐴) = 0)
26		en0 8967	. . 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 1542 ∈ wcel 2114 ∅c0 4287 class class class wbr 5100 ‘cfv 6500 (class class class)co 7368 ≈ cen 8892 Fincfn 8895 ℝcr 11037 0cc0 11038 1c1 11039 +∞cpnf 11175 ℕ₀cn0 12413 ...cfz 13435 ♯chash 14265

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-n0 12414 df-z 12501 df-uz 12764 df-fz 13436 df-hash 14266

This theorem is referenced by: hashneq0 14299 hashnncl 14301 hash0 14302 hashelne0d 14303 hashgt0 14323 hashle00 14335 seqcoll2 14400 prprrab 14408 hashle2pr 14412 hashge2el2difr 14416 ccat0 14511 ccat1st1st 14564 wrdind 14657 wrd2ind 14658 swrdccat3blem 14674 rev0 14699 repsw0 14712 cshwidx0 14741 fz1f1o 15645 hashbc0 16945 0hashbc 16947 ram0 16962 cshws0 17041 chnind 18556 chnub 18557 symgvalstruct 19338 gsmsymgrfix 19369 sylow1lem1 19539 sylow1lem4 19542 sylow2blem3 19563 frgpnabllem1 19814 0ringnnzr 20470 01eq0ringOLD 20476 vieta1lem2 26287 tgldimor 28586 uhgr0vsize0 29324 uhgr0edgfi 29325 usgr1v0e 29411 fusgrfisbase 29413 vtxd0nedgb 29574 vtxdusgr0edgnelALT 29582 usgrvd0nedg 29619 vtxdginducedm1lem4 29628 finsumvtxdg2size 29636 cyclnspth 29886 iswwlksnx 29925 umgrclwwlkge2 30078 clwwisshclwws 30102 hashecclwwlkn1 30164 umgrhashecclwwlk 30165 vdn0conngrumgrv2 30283 frgrwopreg 30410 frrusgrord0lem 30426 wlkl0 30454 frgrregord013 30482 frgrregord13 30483 frgrogt3nreg 30484 friendshipgt3 30485 hashne0 32900 wrdt2ind 33045 tocyc01 33211 esplyfval0 33740 vieta 33756 lvecdim0i 33782 hasheuni 34262 signstfvn 34746 signstfveq0a 34753 signshnz 34768 spthcycl 35342 usgrgt2cycl 35343 acycgr1v 35362 umgracycusgr 35367 cusgracyclt3v 35369 elmrsubrn 35733 fsuppind 42945 lindsrng01 48825

W3C validator