Theorem elfzoel2 13832

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 4290	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ≠ ∅)
2		fzof 13830	. . . . . 6 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
3	2	fdmi 6751	. . . . 5 ⊢ dom ..^ = (ℤ × ℤ)
4	3	ndmov 7637	. . . 4 ⊢ (¬ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) = ∅)
5	4	necon1ai 2986	. . 3 ⊢ ((𝐵..^𝐶) ≠ ∅ → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
6	1, 5	syl 18	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
7	6	simprd 501	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ≠ wne 2959  ∅c0 4281  𝒫 cpw 4560   × cxp 5656  (class class class)co 7451  ℤcz 12733  ..^cfzo 13828

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-neg 11583  df-z 12734  df-uz 13006  df-fz 13680  df-fzo 13829

This theorem is used by:  elfzoelz  13833  elfzo2  13836  elfzole1  13842  elfzolt2  13843  elfzolt3  13844  elfzolt2b  13845  elfzolt3b  13846  elfzop1le2  13847  fzonel  13848  elfzouz2  13849  fzonnsub  13859  fzoss1  13861  fzospliti  13866  fzodisj  13868  elfzolem1  13879  elfzo0subge1  13880  elfzo0suble  13881  fzoaddel  13892  fzo0addelr  13894  elfzoextl  13896  elfzoext  13897  elincfzoext  13898  fzosubel  13899  fzoend  13932  ssfzo12  13934  fzoopth  13937  fzofzp1  13939  elfzo1elm1fzo0  13943  fzonfzoufzol  13946  elfznelfzob  13949  peano2fzor  13950  fzostep1  13961  modsumfzodifsn  14127  addmodlteq  14129  cshwidxm1  15000  cshimadifsn0  15023  fzomaxdiflem  15554  fzo0dvdseq  16537  fzocongeq  16538  addmodlteqALT  16539  efgsp1  20002  efgsres  20003  crctcshwlkn0lem2  30457  crctcshwlkn0lem3  30458  crctcshwlkn0lem5  30460  crctcshwlkn0lem6  30461  crctcshwlkn0  30467  crctcsh  30470  eucrctshift  30901  eucrct2eupth  30903  fzssfzo  35282  signsvfn  35322  dvnmul  47226  iblspltprt  47256  stoweidlem3  47286  fourierdlem12  47402  fourierdlem50  47439  fourierdlem64  47453  fourierdlem79  47468  ormkglobd  48160  chnerlem2  48166  nnmul2  48673  submodlt  48699  muldvdsfacgt  48729  muldvdsfacm1  48730  iccpartiltu  48777  iccpartgt  48782  bgoldbtbndlem2  49177  gpgedgvtx1  49433