Theorem elfzoel2 13679

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 13677	. . . . . 6 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
3	2	fdmi 6731	. . . . 5 ⊢ dom ..^ = (ℤ × ℤ)
4	3	ndmov 7602	. . . 4 ⊢ (¬ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) = ∅)
5	4	necon1ai 2958	. . 3 ⊢ ((𝐵..^𝐶) ≠ ∅ → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
6	1, 5	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
7	6	simprd 494	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099   ≠ wne 2930  ∅c0 4322  𝒫 cpw 4597   × cxp 5672  (class class class)co 7416  ℤcz 12604  ..^cfzo 13675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425  ax-un 7738  ax-cnex 11205  ax-resscn 11206

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-iun 4995  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7995  df-2nd 7996  df-neg 11488  df-z 12605  df-uz 12869  df-fz 13533  df-fzo 13676

This theorem is referenced by:  elfzoelz  13680  elfzo2  13683  elfzole1  13688  elfzolt2  13689  elfzolt3  13690  elfzolt2b  13691  elfzolt3b  13692  elfzop1le2  13693  fzonel  13694  elfzouz2  13695  fzonnsub  13705  fzoss1  13707  fzospliti  13712  fzodisj  13714  fzoaddel  13733  fzo0addelr  13735  elfzoext  13737  elincfzoext  13738  fzosubel  13739  fzoend  13771  ssfzo12  13773  fzoopth  13776  fzofzp1  13778  elfzo1elm1fzo0  13782  fzonfzoufzol  13784  elfznelfzob  13787  peano2fzor  13788  fzostep1  13797  modsumfzodifsn  13958  addmodlteq  13960  cshwidxm1  14810  cshimadifsn0  14834  fzomaxdiflem  15342  fzo0dvdseq  16320  fzocongeq  16321  addmodlteqALT  16322  efgsp1  19731  efgsres  19732  crctcshwlkn0lem2  29742  crctcshwlkn0lem3  29743  crctcshwlkn0lem5  29745  crctcshwlkn0lem6  29746  crctcshwlkn0  29752  crctcsh  29755  eucrctshift  30173  eucrct2eupth  30175  fzssfzo  34398  signsvfn  34441  elfzolem1  44972  dvnmul  45600  iblspltprt  45630  stoweidlem3  45660  fourierdlem12  45776  fourierdlem50  45813  fourierdlem64  45827  fourierdlem79  45842  natglobalincr  46532  iccpartiltu  47030  iccpartgt  47035  bgoldbtbndlem2  47414