Theorem elfzoel2 13682

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 4294	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ≠ ∅)
2		fzof 13680	. . . . . 6 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
3	2	fdmi 6717	. . . . 5 ⊢ dom ..^ = (ℤ × ℤ)
4	3	ndmov 7594	. . . 4 ⊢ (¬ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) = ∅)
5	4	necon1ai 2985	. . 3 ⊢ ((𝐵..^𝐶) ≠ ∅ → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
6	1, 5	syl 18	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
7	6	simprd 500	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ≠ wne 2958  ∅c0 4286  𝒫 cpw 4562   × cxp 5659  (class class class)co 7410  ℤcz 12586  ..^cfzo 13678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11439  df-z 12587  df-uz 12858  df-fz 13531  df-fzo 13679

This theorem is referenced by:  elfzoelz  13683  elfzo2  13686  elfzole1  13692  elfzolt2  13693  elfzolt3  13694  elfzolt2b  13695  elfzolt3b  13696  elfzop1le2  13697  fzonel  13698  elfzouz2  13699  fzonnsub  13709  fzoss1  13711  fzospliti  13716  fzodisj  13718  elfzolem1  13729  elfzo0subge1  13730  elfzo0suble  13731  fzoaddel  13742  fzo0addelr  13744  elfzoextl  13746  elfzoext  13747  elincfzoext  13748  fzosubel  13749  fzoend  13782  ssfzo12  13784  fzoopth  13787  fzofzp1  13789  elfzo1elm1fzo0  13793  fzonfzoufzol  13796  elfznelfzob  13799  peano2fzor  13800  fzostep1  13811  modsumfzodifsn  13976  addmodlteq  13978  cshwidxm1  14840  cshimadifsn0  14863  fzomaxdiflem  15390  fzo0dvdseq  16376  fzocongeq  16377  addmodlteqALT  16378  efgsp1  19802  efgsres  19803  crctcshwlkn0lem2  30160  crctcshwlkn0lem3  30161  crctcshwlkn0lem5  30163  crctcshwlkn0lem6  30164  crctcshwlkn0  30170  crctcsh  30173  eucrctshift  30594  eucrct2eupth  30596  fzssfzo  34929  signsvfn  34969  dvnmul  46657  iblspltprt  46687  stoweidlem3  46717  fourierdlem12  46833  fourierdlem50  46870  fourierdlem64  46884  fourierdlem79  46899  ormkglobd  47591  natglobalincr  47593  chnerlem2  47599  nnmul2  48067  submodlt  48093  muldvdsfacgt  48123  muldvdsfacm1  48124  iccpartiltu  48171  iccpartgt  48176  bgoldbtbndlem2  48571  gpgedgvtx1  48827