Theorem hasheq0 13809

Description: Two ways of saying a finite 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 10753	. . . . . . 7 ⊢ +∞ ∉ ℝ
2	1	neli 3040	. . . . . 6 ⊢ ¬ +∞ ∈ ℝ
3		hashinf 13780	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞)
4	3	eleq1d 2817	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) ∈ ℝ ↔ +∞ ∈ ℝ))
5	2, 4	mtbiri 330	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) ∈ ℝ)
6		id 22	. . . . . 6 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) = 0)
7		0re 10714	. . . . . 6 ⊢ 0 ∈ ℝ
8	6, 7	eqeltrdi 2841	. . . . 5 ⊢ ((♯‘𝐴) = 0 → (♯‘𝐴) ∈ ℝ)
9	5, 8	nsyl 142	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (♯‘𝐴) = 0)
10		id 22	. . . . . . 7 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
11		0fin 8763	. . . . . . 7 ⊢ ∅ ∈ Fin
12	10, 11	eqeltrdi 2841	. . . . . 6 ⊢ (𝐴 = ∅ → 𝐴 ∈ Fin)
13	12	con3i 157	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → ¬ 𝐴 = ∅)
14	13	adantl 485	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 = ∅)
15	9, 14	2falsed 380	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))
16	15	ex 416	. 2 ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)))
17		hashen 13792	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ ∅ ∈ Fin) → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
18	11, 17	mpan2 691	. . 3 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = (♯‘∅) ↔ 𝐴 ≈ ∅))
19		fz10 13012	. . . . . 6 ⊢ (1...0) = ∅
20	19	fveq2i 6671	. . . . 5 ⊢ (♯‘(1...0)) = (♯‘∅)
21		0nn0 11984	. . . . . 6 ⊢ 0 ∈ ℕ0
22		hashfz1 13791	. . . . . 6 ⊢ (0 ∈ ℕ0 → (♯‘(1...0)) = 0)
23	21, 22	ax-mp 5	. . . . 5 ⊢ (♯‘(1...0)) = 0
24	20, 23	eqtr3i 2763	. . . 4 ⊢ (♯‘∅) = 0
25	24	eqeq2i 2751	. . 3 ⊢ ((♯‘𝐴) = (♯‘∅) ↔ (♯‘𝐴) = 0)
26		en0 8611	. . 3 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
27	18, 25, 26	3bitr3g 316	. 2 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))
28	16, 27	pm2.61d2 184	1 ⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2113  ∅c0 4209   class class class wbr 5027  ‘cfv 6333  (class class class)co 7164   ≈ cen 8545  Fincfn 8548  ℝcr 10607  0cc0 10608  1c1 10609  +∞cpnf 10743  ℕ₀cn0 11969  ...cfz 12974  ♯chash 13775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-1st 7707  df-2nd 7708  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-nn 11710  df-n0 11970  df-z 12056  df-uz 12318  df-fz 12975  df-hash 13776

This theorem is referenced by:  hashneq0  13810  hashnncl  13812  hash0  13813  hashelne0d  13814  hashgt0  13834  hashle00  13846  seqcoll2  13910  prprrab  13918  hashle2pr  13922  hashge2el2difr  13926  ccat0  14011  ccat1st1st  14066  wrdind  14166  wrd2ind  14167  swrdccat3blem  14183  rev0  14208  repsw0  14221  cshwidx0  14250  fz1f1o  15153  hashbc0  16434  0hashbc  16436  ram0  16451  cshws0  16531  symgvalstruct  18636  gsmsymgrfix  18667  sylow1lem1  18834  sylow1lem4  18837  sylow2blem3  18858  frgpnabllem1  19105  0ringnnzr  20154  01eq0ring  20157  vieta1lem2  25051  tgldimor  26440  uhgr0vsize0  27173  uhgr0edgfi  27174  usgr1v0e  27260  fusgrfisbase  27262  vtxd0nedgb  27422  vtxdusgr0edgnelALT  27430  usgrvd0nedg  27467  vtxdginducedm1lem4  27476  finsumvtxdg2size  27484  cyclnspth  27733  iswwlksnx  27770  umgrclwwlkge2  27920  clwwisshclwws  27944  hashecclwwlkn1  28006  umgrhashecclwwlk  28007  vdn0conngrumgrv2  28125  frgrwopreg  28252  frrusgrord0lem  28268  wlkl0  28296  frgrregord013  28324  frgrregord13  28325  frgrogt3nreg  28326  friendshipgt3  28327  wrdt2ind  30792  tocyc01  30954  lvecdim0i  31253  hasheuni  31615  signstfvn  32110  signstfveq0a  32117  signshnz  32132  spthcycl  32654  usgrgt2cycl  32655  acycgr1v  32674  umgracycusgr  32679  cusgracyclt3v  32681  elmrsubrn  33045  fsuppind  39842  lindsrng01  45327