Theorem elfzoel2 13619

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ≠ wne 2925  ∅c0 4296  𝒫 cpw 4563   × cxp 5636  (class class class)co 7387  ℤcz 12529  ..^cfzo 13615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-neg 11408  df-z 12530  df-uz 12794  df-fz 13469  df-fzo 13616

This theorem is referenced by:  elfzoelz  13620  elfzo2  13623  elfzole1  13628  elfzolt2  13629  elfzolt3  13630  elfzolt2b  13631  elfzolt3b  13632  elfzop1le2  13633  fzonel  13634  elfzouz2  13635  fzonnsub  13645  fzoss1  13647  fzospliti  13652  fzodisj  13654  elfzolem1  13665  elfzo0subge1  13666  elfzo0suble  13667  fzoaddel  13678  fzo0addelr  13680  elfzoextl  13682  elfzoext  13683  elincfzoext  13684  fzosubel  13685  fzoend  13718  ssfzo12  13720  fzoopth  13723  fzofzp1  13725  elfzo1elm1fzo0  13729  fzonfzoufzol  13731  elfznelfzob  13734  peano2fzor  13735  fzostep1  13744  modsumfzodifsn  13909  addmodlteq  13911  cshwidxm1  14772  cshimadifsn0  14796  fzomaxdiflem  15309  fzo0dvdseq  16293  fzocongeq  16294  addmodlteqALT  16295  efgsp1  19667  efgsres  19668  crctcshwlkn0lem2  29741  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  crctcshwlkn0  29751  crctcsh  29754  eucrctshift  30172  eucrct2eupth  30174  fzssfzo  34530  signsvfn  34573  dvnmul  45941  iblspltprt  45971  stoweidlem3  46001  fourierdlem12  46117  fourierdlem50  46154  fourierdlem64  46168  fourierdlem79  46183  ormkglobd  46873  natglobalincr  46875  submodlt  47351  iccpartiltu  47423  iccpartgt  47428  bgoldbtbndlem2  47807  gpgedgvtx1  48053