Theorem elfzoelz 11871

Description: Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)

Assertion

Ref	Expression
elfzoelz	|- ( A e. ( B..^ C ) -> A e. ZZ )

Proof of Theorem elfzoelz

Step	Hyp	Ref	Expression
1		elfzoel1 11869	. . . 4 |- ( A e. ( B..^ C ) -> B e. ZZ )
2		elfzoel2 11870	. . . 4 |- ( A e. ( B..^ C ) -> C e. ZZ )
3		fzof 11868	. . . . 5 |- ..^ : ( ZZ X. ZZ ) --> ~P ZZ
4	3	fovcl 6359	. . . 4 |- ( ( B e. ZZ /\ C e. ZZ ) -> ( B..^ C ) e. ~P ZZ )
5	1, 2, 4	syl2anc 665	. . 3 |- ( A e. ( B..^ C ) -> ( B..^ C ) e. ~P ZZ )
6	5	elpwid 3934	. 2 |- ( A e. ( B..^ C ) -> ( B..^ C ) C_ ZZ )
7		id 22	. 2 |- ( A e. ( B..^ C ) -> A e. ( B..^ C ) )
8	6, 7	sseldd 3408	1 |- ( A e. ( B..^ C ) -> A e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1872   ~Pcpw 3924  (class class class)co 6249   ZZcz 10888  ..^cfzo 11866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-1st 6751  df-2nd 6752  df-neg 9814  df-z 10889  df-uz 11111  df-fz 11736  df-fzo 11867

This theorem is referenced by:  elfzo2  11874  elfzole1  11879  elfzolt2  11880  elfzolt3  11881  elfzolt2b  11882  elfzouz2  11885  fzonnsub  11894  fzospliti  11901  fzodisj  11903  fzonmapblen  11912  fzoaddel  11917  elincfzoext  11922  fzosubel  11923  elfznelfzob  11965  modaddmodup  12103  modaddmodlo  12104  wrdexg  12630  ccatval3  12672  ccatlid  12678  ccatass  12680  ccatrn  12681  swrd0val  12723  swrdid  12730  swrd0fv  12741  swrdfv2  12748  swrds1  12753  ccatswrd  12758  swrdswrd  12762  swrdccatin12lem2a  12787  swrdccatin2  12789  swrdccatin12lem2  12791  splfv1  12808  splfv2a  12809  revccat  12817  revrev  12818  repswrevw  12835  cshwidxmod  12851  cshwidx0  12853  cshwidxm1  12854  cshweqrep  12866  cshw1  12867  cshco  12879  fzomaxdiflem  13349  fzomaxdif  13350  fzo0dvdseq  14301  fzocongeq  14302  crt  14669  phimullem  14670  eulerthlem1  14672  eulerthlem2  14673  reumodprminv  14698  modprm0  14699  nnnn0modprm0  14700  modprmn0modprm0  14701  prmgaplem7  14970  cshwshashlem2  15010  cshwshashlem3  15011  cshwrepswhash1  15016  psgnunilem5  17078  odf1o2  17165  odngen  17169  efgsp1  17330  efgsres  17331  znf1o  19064  zntoslem  19069  znunithash  19077  dvfsumle  22915  dvfsumabs  22917  dchrisumlem1  24269  dchrisumlem2  24270  dchrisum  24272  pntlemq  24381  pntlemr  24382  pntlemj  24383  pntlemi  24384  pntlemf  24385  wlkdvspthlem  25279  fargshiftf1  25307  clwwisshclwwlem  25476  clwwisshclww  25477  eupatrl  25638  signsvfn  29423  poimirlem8  31855  poimirlem18  31865  poimirlem21  31868  poimirlem22  31869  poimirlem24  31871  hashgcdlem  35987  hashgcdeq  35988  phisum  35989  elfzop1le2  37400  iblspltprt  37733  itgspltprt  37739  stoweidlem3  37746  fourierdlem12  37864  fourierdlem20  37872  fourierdlem46  37899  fourierdlem50  37903  fourierdlem54  37907  fourierdlem63  37916  fourierdlem64  37917  fourierdlem65  37918  fourierdlem76  37929  fourierdlem79  37932  fourierdlem102  37955  fourierdlem103  37956  fourierdlem104  37957  fourierdlem114  37967  iundjiun  38149  carageniuncllem1  38193  caratheodorylem1  38198  iccpartipre  38548  iccpartiltu  38549  iccpartigtl  38550  iccpartgt  38554  icceuelpartlem  38562  icceuelpart  38563  iccpartnel  38565  bgoldbtbndlem2  38714  pfxfv  38753  ccatpfx  38763  pfxccatin12lem2  38778  m1modmmod  39927  fllog2  39982  nn0sumshdiglemA  40033  nn0sumshdiglemB  40034  nn0mullong  40039