Theorem elfzoel2 13636

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 4334	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ≠ ∅)
2		fzof 13634	. . . . . 6 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
3	2	fdmi 6729	. . . . 5 ⊢ dom ..^ = (ℤ × ℤ)
4	3	ndmov 7595	. . . 4 ⊢ (¬ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) = ∅)
5	4	necon1ai 2967	. . 3 ⊢ ((𝐵..^𝐶) ≠ ∅ → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
6	1, 5	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
7	6	simprd 495	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   ≠ wne 2939  ∅c0 4322  𝒫 cpw 4602   × cxp 5674  (class class class)co 7412  ℤcz 12563  ..^cfzo 13632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729  ax-cnex 11170  ax-resscn 11171

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-neg 11452  df-z 12564  df-uz 12828  df-fz 13490  df-fzo 13633

This theorem is referenced by:  elfzoelz  13637  elfzo2  13640  elfzole1  13645  elfzolt2  13646  elfzolt3  13647  elfzolt2b  13648  elfzolt3b  13649  elfzop1le2  13650  fzonel  13651  elfzouz2  13652  fzonnsub  13662  fzoss1  13664  fzospliti  13669  fzodisj  13671  fzoaddel  13690  fzo0addelr  13692  elfzoext  13694  elincfzoext  13695  fzosubel  13696  fzoend  13728  ssfzo12  13730  fzofzp1  13734  elfzo1elm1fzo0  13738  fzonfzoufzol  13740  elfznelfzob  13743  peano2fzor  13744  fzostep1  13753  modsumfzodifsn  13914  addmodlteq  13916  cshwidxm1  14762  cshimadifsn0  14786  fzomaxdiflem  15294  fzo0dvdseq  16271  fzocongeq  16272  addmodlteqALT  16273  efgsp1  19647  efgsres  19648  crctcshwlkn0lem2  29333  crctcshwlkn0lem3  29334  crctcshwlkn0lem5  29336  crctcshwlkn0lem6  29337  crctcshwlkn0  29343  crctcsh  29346  eucrctshift  29764  eucrct2eupth  29766  fzssfzo  33849  signsvfn  33892  elfzolem1  44330  dvnmul  44958  iblspltprt  44988  stoweidlem3  45018  fourierdlem12  45134  fourierdlem50  45171  fourierdlem64  45185  fourierdlem79  45200  natglobalincr  45890  fzoopth  46334  iccpartiltu  46389  iccpartgt  46394  bgoldbtbndlem2  46773