Theorem hash1snb 13823

Description: The size of a set is 1 if and only if it is a singleton (containing a set). (Contributed by Alexander van der Vekens, 7-Dec-2017.)

Assertion

Ref	Expression
hash1snb	⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 ↔ ∃𝑎 𝑉 = {𝑎}))

Distinct variable group:   𝑉,𝑎

Allowed substitution hint:   𝑊(𝑎)

Proof of Theorem hash1snb

Step	Hyp	Ref	Expression
1		id 22	. . . . . . . . 9 ⊢ ((♯‘𝑉) = 1 → (♯‘𝑉) = 1)
2		hash1 13808	. . . . . . . . 9 ⊢ (♯‘1o) = 1
3	1, 2	eqtr4di 2812	. . . . . . . 8 ⊢ ((♯‘𝑉) = 1 → (♯‘𝑉) = (♯‘1o))
4	3	adantl 486	. . . . . . 7 ⊢ ((𝑉 ∈ Fin ∧ (♯‘𝑉) = 1) → (♯‘𝑉) = (♯‘1o))
5		1onn 8276	. . . . . . . . 9 ⊢ 1o ∈ ω
6		nnfi 8734	. . . . . . . . 9 ⊢ (1o ∈ ω → 1o ∈ Fin)
7	5, 6	mp1i 13	. . . . . . . 8 ⊢ ((♯‘𝑉) = 1 → 1o ∈ Fin)
8		hashen 13750	. . . . . . . 8 ⊢ ((𝑉 ∈ Fin ∧ 1o ∈ Fin) → ((♯‘𝑉) = (♯‘1o) ↔ 𝑉 ≈ 1o))
9	7, 8	sylan2 596	. . . . . . 7 ⊢ ((𝑉 ∈ Fin ∧ (♯‘𝑉) = 1) → ((♯‘𝑉) = (♯‘1o) ↔ 𝑉 ≈ 1o))
10	4, 9	mpbid 235	. . . . . 6 ⊢ ((𝑉 ∈ Fin ∧ (♯‘𝑉) = 1) → 𝑉 ≈ 1o)
11		en1 8596	. . . . . 6 ⊢ (𝑉 ≈ 1o ↔ ∃𝑎 𝑉 = {𝑎})
12	10, 11	sylib 221	. . . . 5 ⊢ ((𝑉 ∈ Fin ∧ (♯‘𝑉) = 1) → ∃𝑎 𝑉 = {𝑎})
13	12	ex 417	. . . 4 ⊢ (𝑉 ∈ Fin → ((♯‘𝑉) = 1 → ∃𝑎 𝑉 = {𝑎}))
14	13	a1d 25	. . 3 ⊢ (𝑉 ∈ Fin → (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 → ∃𝑎 𝑉 = {𝑎})))
15		hashinf 13738	. . . . 5 ⊢ ((𝑉 ∈ 𝑊 ∧ ¬ 𝑉 ∈ Fin) → (♯‘𝑉) = +∞)
16		eqeq1 2763	. . . . . 6 ⊢ ((♯‘𝑉) = +∞ → ((♯‘𝑉) = 1 ↔ +∞ = 1))
17		1re 10672	. . . . . . . 8 ⊢ 1 ∈ ℝ
18		renepnf 10720	. . . . . . . 8 ⊢ (1 ∈ ℝ → 1 ≠ +∞)
19		df-ne 2953	. . . . . . . . 9 ⊢ (1 ≠ +∞ ↔ ¬ 1 = +∞)
20		pm2.21 123	. . . . . . . . 9 ⊢ (¬ 1 = +∞ → (1 = +∞ → ∃𝑎 𝑉 = {𝑎}))
21	19, 20	sylbi 220	. . . . . . . 8 ⊢ (1 ≠ +∞ → (1 = +∞ → ∃𝑎 𝑉 = {𝑎}))
22	17, 18, 21	mp2b 10	. . . . . . 7 ⊢ (1 = +∞ → ∃𝑎 𝑉 = {𝑎})
23	22	eqcoms 2767	. . . . . 6 ⊢ (+∞ = 1 → ∃𝑎 𝑉 = {𝑎})
24	16, 23	syl6bi 256	. . . . 5 ⊢ ((♯‘𝑉) = +∞ → ((♯‘𝑉) = 1 → ∃𝑎 𝑉 = {𝑎}))
25	15, 24	syl 17	. . . 4 ⊢ ((𝑉 ∈ 𝑊 ∧ ¬ 𝑉 ∈ Fin) → ((♯‘𝑉) = 1 → ∃𝑎 𝑉 = {𝑎}))
26	25	expcom 418	. . 3 ⊢ (¬ 𝑉 ∈ Fin → (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 → ∃𝑎 𝑉 = {𝑎})))
27	14, 26	pm2.61i 185	. 2 ⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 → ∃𝑎 𝑉 = {𝑎}))
28		fveq2 6659	. . . 4 ⊢ (𝑉 = {𝑎} → (♯‘𝑉) = (♯‘{𝑎}))
29		hashsng 13773	. . . . 5 ⊢ (𝑎 ∈ V → (♯‘{𝑎}) = 1)
30	29	elv 3416	. . . 4 ⊢ (♯‘{𝑎}) = 1
31	28, 30	eqtrdi 2810	. . 3 ⊢ (𝑉 = {𝑎} → (♯‘𝑉) = 1)
32	31	exlimiv 1932	. 2 ⊢ (∃𝑎 𝑉 = {𝑎} → (♯‘𝑉) = 1)
33	27, 32	impbid1 228	1 ⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 ↔ ∃𝑎 𝑉 = {𝑎}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112   ≠ wne 2952  Vcvv 3410  {csn 4523   class class class wbr 5033  ‘cfv 6336  ωcom 7580  1_oc1o 8106   ≈ cen 8525  Fincfn 8528  ℝcr 10567  1c1 10569  +∞cpnf 10703  ♯chash 13733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10624  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-1st 7694  df-2nd 7695  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-oadd 8117  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-dju 9356  df-card 9394  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-nn 11668  df-n0 11928  df-z 12014  df-uz 12276  df-fz 12933  df-hash 13734

This theorem is referenced by:  hash1n0  13825  hashle2pr  13880  hashge2el2difr  13884  hash1to3  13894  cshwrepswhash1  16487  symgvalstruct  18585  mat1scmat  21232  tgldim0eq  26389  lfuhgr1v0e  27136  usgr1v0e  27208  nbgr1vtx  27240  uvtx01vtx  27279  cplgr1vlem  27311  cplgr1v  27312  1loopgrvd2  27385  vdgn1frgrv2  28173  frgrwopreg1  28195  frgrwopreg2  28196  extdg1id  31252  c0snmgmhm  44898