Theorem elfzoel2 13799

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ≠ wne 2955  ∅c0 4277  𝒫 cpw 4556   × cxp 5649  (class class class)co 7424  ℤcz 12700  ..^cfzo 13795

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7427  df-oprab 7428  df-mpo 7429  df-1st 8005  df-2nd 8006  df-neg 11551  df-z 12701  df-uz 12973  df-fz 13647  df-fzo 13796

This theorem is used by:  elfzoelz  13800  elfzo2  13803  elfzole1  13809  elfzolt2  13810  elfzolt3  13811  elfzolt2b  13812  elfzolt3b  13813  elfzop1le2  13814  fzonel  13815  elfzouz2  13816  fzonnsub  13826  fzoss1  13828  fzospliti  13833  fzodisj  13835  elfzolem1  13846  elfzo0subge1  13847  elfzo0suble  13848  fzoaddel  13859  fzo0addelr  13861  elfzoextl  13863  elfzoext  13864  elincfzoext  13865  fzosubel  13866  fzoend  13899  ssfzo12  13901  fzoopth  13904  fzofzp1  13906  elfzo1elm1fzo0  13910  fzonfzoufzol  13913  elfznelfzob  13916  peano2fzor  13917  fzostep1  13928  modsumfzodifsn  14094  addmodlteq  14096  cshwidxm1  14966  cshimadifsn0  14989  fzomaxdiflem  15519  fzo0dvdseq  16502  fzocongeq  16503  addmodlteqALT  16504  efgsp1  19960  efgsres  19961  crctcshwlkn0lem2  30409  crctcshwlkn0lem3  30410  crctcshwlkn0lem5  30412  crctcshwlkn0lem6  30413  crctcshwlkn0  30419  crctcsh  30422  eucrctshift  30853  eucrct2eupth  30855  fzssfzo  35221  signsvfn  35261  dvnmul  47061  iblspltprt  47091  stoweidlem3  47121  fourierdlem12  47237  fourierdlem50  47274  fourierdlem64  47288  fourierdlem79  47303  ormkglobd  47995  chnerlem2  48001  nnmul2  48508  submodlt  48534  muldvdsfacgt  48564  muldvdsfacm1  48565  iccpartiltu  48612  iccpartgt  48617  bgoldbtbndlem2  49012  gpgedgvtx1  49268