Theorem elfzoel2 13663

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 4293	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ≠ ∅)
2		fzof 13661	. . . . . 6 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
3	2	fdmi 6703	. . . . 5 ⊢ dom ..^ = (ℤ × ℤ)
4	3	ndmov 7580	. . . 4 ⊢ (¬ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) = ∅)
5	4	necon1ai 2984	. . 3 ⊢ ((𝐵..^𝐶) ≠ ∅ → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
6	1, 5	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
7	6	simprd 499	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142   ≠ wne 2957  ∅c0 4285  𝒫 cpw 4555   × cxp 5645  (class class class)co 7396  ℤcz 12568  ..^cfzo 13659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-neg 11417  df-z 12569  df-uz 12840  df-fz 13513  df-fzo 13660

This theorem is referenced by:  elfzoelz  13664  elfzo2  13667  elfzole1  13673  elfzolt2  13674  elfzolt3  13675  elfzolt2b  13676  elfzolt3b  13677  elfzop1le2  13678  fzonel  13679  elfzouz2  13680  fzonnsub  13690  fzoss1  13692  fzospliti  13697  fzodisj  13699  elfzolem1  13710  elfzo0subge1  13711  elfzo0suble  13712  fzoaddel  13723  fzo0addelr  13725  elfzoextl  13727  elfzoext  13728  elincfzoext  13729  fzosubel  13730  fzoend  13763  ssfzo12  13765  fzoopth  13768  fzofzp1  13770  elfzo1elm1fzo0  13774  fzonfzoufzol  13777  elfznelfzob  13780  peano2fzor  13781  fzostep1  13792  modsumfzodifsn  13957  addmodlteq  13959  cshwidxm1  14820  cshimadifsn0  14843  fzomaxdiflem  15370  fzo0dvdseq  16357  fzocongeq  16358  addmodlteqALT  16359  efgsp1  19777  efgsres  19778  crctcshwlkn0lem2  30008  crctcshwlkn0lem3  30009  crctcshwlkn0lem5  30011  crctcshwlkn0lem6  30012  crctcshwlkn0  30018  crctcsh  30021  eucrctshift  30442  eucrct2eupth  30444  fzssfzo  34833  signsvfn  34873  dvnmul  46514  iblspltprt  46544  stoweidlem3  46574  fourierdlem12  46690  fourierdlem50  46727  fourierdlem64  46741  fourierdlem79  46756  ormkglobd  47448  natglobalincr  47450  chnerlem2  47456  nnmul2  47921  submodlt  47947  muldvdsfacgt  47977  muldvdsfacm1  47978  iccpartiltu  48025  iccpartgt  48030  bgoldbtbndlem2  48425  gpgedgvtx1  48681