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 14325

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 11186	. . . . . . 7 ⊢ +∞ ∉ ℝ
2	1	neli 3038	. . . . . 6 ⊢ ¬ +∞ ∈ ℝ
3		hashinf 14297	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞)
4	3	eleq1d 2821	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) ∈ ℝ ↔ +∞ ∈ ℝ))
5	2, 4	mtbiri 327	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) ∈ ℝ)
6		id 22	. . . . . 6 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) = 0)
7		0re 11146	. . . . . 6 ⊢ 0 ∈ ℝ
8	6, 7	eqeltrdi 2844	. . . . 5 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) ∈ ℝ)
9	5, 8	nsyl 140	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) = 0)
10		id 22	. . . . . . 7 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
11		0fi 8989	. . . . . . 7 ⊢ ∅ ∈ Fin
12	10, 11	eqeltrdi 2844	. . . . . 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 14309	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ ∅ ∈ Fin) → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
18	11, 17	mpan2 692	. . 3 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
19		fz10 13499	. . . . . 6 ⊢ (1...0) = ∅
20	19	fveq2i 6843	. . . . 5 ⊢ (♯‘(1...0)) = (♯‘∅)
21		0nn0 12452	. . . . . 6 ⊢ 0 ∈ ℕ₀
22		hashfz1 14308	. . . . . 6 ⊢ (0 ∈ ℕ₀ → (♯‘(1...0)) = 0)
23	21, 22	ax-mp 5	. . . . 5 ⊢ (♯‘(1...0)) = 0
24	20, 23	eqtr3i 2761	. . . 4 ⊢ (♯‘∅) = 0
25	24	eqeq2i 2749	. . 3 ⊢ ((♯‘𝐴) = (♯‘∅) ↔ (♯‘𝐴) = 0)
26		en0 8965	. . 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 4273 class class class wbr 5085 ‘cfv 6498 (class class class)co 7367 ≈ cen 8890 Fincfn 8893 ℝcr 11037 0cc0 11038 1c1 11039 +∞cpnf 11176 ℕ₀cn0 12437 ...cfz 13461 ♯chash 14292

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 2708 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-n0 12438 df-z 12525 df-uz 12789 df-fz 13462 df-hash 14293

This theorem is referenced by: hashneq0 14326 hashnncl 14328 hash0 14329 hashelne0d 14330 hashgt0 14350 hashle00 14362 seqcoll2 14427 prprrab 14435 hashle2pr 14439 hashge2el2difr 14443 ccat0 14538 ccat1st1st 14591 wrdind 14684 wrd2ind 14685 swrdccat3blem 14701 rev0 14726 repsw0 14739 cshwidx0 14768 fz1f1o 15672 hashbc0 16976 0hashbc 16978 ram0 16993 cshws0 17072 chnind 18587 chnub 18588 symgvalstruct 19372 gsmsymgrfix 19403 sylow1lem1 19573 sylow1lem4 19576 sylow2blem3 19597 frgpnabllem1 19848 0ringnnzr 20502 01eq0ringOLD 20508 vieta1lem2 26277 tgldimor 28570 uhgr0vsize0 29308 uhgr0edgfi 29309 usgr1v0e 29395 fusgrfisbase 29397 vtxd0nedgb 29557 vtxdusgr0edgnelALT 29565 usgrvd0nedg 29602 vtxdginducedm1lem4 29611 finsumvtxdg2size 29619 cyclnspth 29869 iswwlksnx 29908 umgrclwwlkge2 30061 clwwisshclwws 30085 hashecclwwlkn1 30147 umgrhashecclwwlk 30148 vdn0conngrumgrv2 30266 frgrwopreg 30393 frrusgrord0lem 30409 wlkl0 30437 frgrregord013 30465 frgrregord13 30466 frgrogt3nreg 30467 friendshipgt3 30468 hashne0 32883 wrdt2ind 33013 tocyc01 33179 esplyfval0 33708 vieta 33724 lvecdim0i 33750 hasheuni 34229 signstfvn 34713 signstfveq0a 34720 signshnz 34735 spthcycl 35311 usgrgt2cycl 35312 acycgr1v 35331 umgracycusgr 35336 cusgracyclt3v 35338 elmrsubrn 35702 fsuppind 43023 lindsrng01 48944

W3C validator