Theorem s1len 14654

Description: Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
s1len	⊢ (♯‘⟨“𝐴”⟩) = 1

Proof of Theorem s1len

Step	Hyp	Ref	Expression
1		df-s1 14644	. . 3 ⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
2	1	fveq2i 6923	. 2 ⊢ (♯‘⟨“𝐴”⟩) = (♯‘{⟨0, ( I ‘𝐴)⟩})
3		opex 5484	. . 3 ⊢ ⟨0, ( I ‘𝐴)⟩ ∈ V
4		hashsng 14418	. . 3 ⊢ (⟨0, ( I ‘𝐴)⟩ ∈ V → (♯‘{⟨0, ( I ‘𝐴)⟩}) = 1)
5	3, 4	ax-mp 5	. 2 ⊢ (♯‘{⟨0, ( I ‘𝐴)⟩}) = 1
6	2, 5	eqtri 2768	1 ⊢ (♯‘⟨“𝐴”⟩) = 1

Syntax hints:   = wceq 1537   ∈ wcel 2108  Vcvv 3488  {csn 4648  ⟨cop 4654   I cid 5592  ‘cfv 6573  0cc0 11184  1c1 11185  ♯chash 14379  ⟨“cs1 14643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640  df-uz 12904  df-fz 13568  df-hash 14380  df-s1 14644

This theorem is referenced by:  s1dm  14656  lsws1  14659  eqs1  14660  wrdl1s1  14662  ccats1alpha  14667  ccatws1len  14668  ccat2s1len  14671  ccats1val2  14675  ccat2s1p1  14677  ccat2s1p2  14678  cats1un  14769  revs1  14813  cats1fvn  14907  cats1len  14909  s2fv0  14936  s2fv1  14937  s2len  14938  s2prop  14956  s2eq2s1eq  14985  ofs2  15020  psgnpmtr  19552  efgsval2  19775  efgs1  19777  efgsp1  19779  efgsfo  19781  efgredlemc  19787  pgpfaclem1  20125  wwlksnext  29926  wwlksnextbi  29927  clwlkclwwlk2  30035  loopclwwlkn1b  30074  clwwlkn1loopb  30075  clwwlkel  30078  clwwlkwwlksb  30086  clwwlknon1  30129  1ewlk  30147  1pthdlem1  30167  1pthdlem2  30168  1wlkdlem1  30169  1wlkdlem4  30172  1pthond  30176  lp1cycl  30184  ccatws1f1o  32918  cycpmco2lem2  33120  cycpmco2lem5  33123  cycpmco2lem6  33124  1arithidomlem2  33529  signstf0  34545  signstfvn  34546  signstfvp  34548  signsvf1  34558  signsvfn  34559  signshf  34565  loop1cycl  35105  upwordsing  46803