Theorem elfzoel2 13703

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ≠ wne 2960  ∅c0 4286  𝒫 cpw 4564   × cxp 5661  (class class class)co 7419  ℤcz 12606  ..^cfzo 13699

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7992  df-2nd 7993  df-neg 11459  df-z 12607  df-uz 12879  df-fz 13552  df-fzo 13700

This theorem is used by:  elfzoelz  13704  elfzo2  13707  elfzole1  13713  elfzolt2  13714  elfzolt3  13715  elfzolt2b  13716  elfzolt3b  13717  elfzop1le2  13718  fzonel  13719  elfzouz2  13720  fzonnsub  13730  fzoss1  13732  fzospliti  13737  fzodisj  13739  elfzolem1  13750  elfzo0subge1  13751  elfzo0suble  13752  fzoaddel  13763  fzo0addelr  13765  elfzoextl  13767  elfzoext  13768  elincfzoext  13769  fzosubel  13770  fzoend  13803  ssfzo12  13805  fzoopth  13808  fzofzp1  13810  elfzo1elm1fzo0  13814  fzonfzoufzol  13817  elfznelfzob  13820  peano2fzor  13821  fzostep1  13832  modsumfzodifsn  13998  addmodlteq  14000  cshwidxm1  14868  cshimadifsn0  14891  fzomaxdiflem  15418  fzo0dvdseq  16403  fzocongeq  16404  addmodlteqALT  16405  efgsp1  19851  efgsres  19852  crctcshwlkn0lem2  30227  crctcshwlkn0lem3  30228  crctcshwlkn0lem5  30230  crctcshwlkn0lem6  30231  crctcshwlkn0  30237  crctcsh  30240  eucrctshift  30665  eucrct2eupth  30667  fzssfzo  34994  signsvfn  35034  dvnmul  46715  iblspltprt  46745  stoweidlem3  46775  fourierdlem12  46891  fourierdlem50  46928  fourierdlem64  46942  fourierdlem79  46957  ormkglobd  47649  natglobalincr  47651  chnerlem2  47657  nnmul2  48125  submodlt  48151  muldvdsfacgt  48181  muldvdsfacm1  48182  iccpartiltu  48229  iccpartgt  48234  bgoldbtbndlem2  48629  gpgedgvtx1  48885