Theorem elfzoel2 13685

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

Assertion

Ref	Expression
elfzoel2	⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

Proof of Theorem elfzoel2

Step	Hyp	Ref	Expression
1		ne0i 4302	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ≠ ∅)
2		fzof 13683	. . . . . 6 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
3	2	fdmi 6718	. . . . 5 ⊢ dom ..^ = (ℤ × ℤ)
4	3	ndmov 7595	. . . 4 ⊢ (¬ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) = ∅)
5	4	necon1ai 2991	. . 3 ⊢ ((𝐵..^𝐶) ≠ ∅ → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
6	1, 5	syl 18	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
7	6	simprd 500	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ≠ wne 2964  ∅c0 4294  𝒫 cpw 4567   × cxp 5660  (class class class)co 7411  ℤcz 12590  ..^cfzo 13681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7985  df-2nd 7986  df-neg 11443  df-z 12591  df-uz 12862  df-fz 13535  df-fzo 13682

This theorem is referenced by:  elfzoelz  13686  elfzo2  13689  elfzole1  13695  elfzolt2  13696  elfzolt3  13697  elfzolt2b  13698  elfzolt3b  13699  elfzop1le2  13700  fzonel  13701  elfzouz2  13702  fzonnsub  13712  fzoss1  13714  fzospliti  13719  fzodisj  13721  elfzolem1  13732  elfzo0subge1  13733  elfzo0suble  13734  fzoaddel  13745  fzo0addelr  13747  elfzoextl  13749  elfzoext  13750  elincfzoext  13751  fzosubel  13752  fzoend  13785  ssfzo12  13787  fzoopth  13790  fzofzp1  13792  elfzo1elm1fzo0  13796  fzonfzoufzol  13799  elfznelfzob  13802  peano2fzor  13803  fzostep1  13814  modsumfzodifsn  13979  addmodlteq  13981  cshwidxm1  14843  cshimadifsn0  14866  fzomaxdiflem  15393  fzo0dvdseq  16380  fzocongeq  16381  addmodlteqALT  16382  efgsp1  19806  efgsres  19807  crctcshwlkn0lem2  30100  crctcshwlkn0lem3  30101  crctcshwlkn0lem5  30103  crctcshwlkn0lem6  30104  crctcshwlkn0  30110  crctcsh  30113  eucrctshift  30534  eucrct2eupth  30536  fzssfzo  34873  signsvfn  34913  dvnmul  46548  iblspltprt  46578  stoweidlem3  46608  fourierdlem12  46724  fourierdlem50  46761  fourierdlem64  46775  fourierdlem79  46790  ormkglobd  47482  natglobalincr  47484  chnerlem2  47490  nnmul2  47955  submodlt  47981  muldvdsfacgt  48011  muldvdsfacm1  48012  iccpartiltu  48059  iccpartgt  48064  bgoldbtbndlem2  48459  gpgedgvtx1  48715