Theorem elfzoel2 13606

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274  𝒫 cpw 4542   × cxp 5623  (class class class)co 7361  ℤcz 12518  ..^cfzo 13602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-neg 11374  df-z 12519  df-uz 12783  df-fz 13456  df-fzo 13603

This theorem is referenced by:  elfzoelz  13607  elfzo2  13610  elfzole1  13616  elfzolt2  13617  elfzolt3  13618  elfzolt2b  13619  elfzolt3b  13620  elfzop1le2  13621  fzonel  13622  elfzouz2  13623  fzonnsub  13633  fzoss1  13635  fzospliti  13640  fzodisj  13642  elfzolem1  13653  elfzo0subge1  13654  elfzo0suble  13655  fzoaddel  13666  fzo0addelr  13668  elfzoextl  13670  elfzoext  13671  elincfzoext  13672  fzosubel  13673  fzoend  13706  ssfzo12  13708  fzoopth  13711  fzofzp1  13713  elfzo1elm1fzo0  13717  fzonfzoufzol  13720  elfznelfzob  13723  peano2fzor  13724  fzostep1  13735  modsumfzodifsn  13900  addmodlteq  13902  cshwidxm1  14763  cshimadifsn0  14786  fzomaxdiflem  15299  fzo0dvdseq  16286  fzocongeq  16287  addmodlteqALT  16288  efgsp1  19706  efgsres  19707  crctcshwlkn0lem2  29897  crctcshwlkn0lem3  29898  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  crctcshwlkn0  29907  crctcsh  29910  eucrctshift  30331  eucrct2eupth  30333  fzssfzo  34702  signsvfn  34745  dvnmul  46392  iblspltprt  46422  stoweidlem3  46452  fourierdlem12  46568  fourierdlem50  46605  fourierdlem64  46619  fourierdlem79  46634  ormkglobd  47324  natglobalincr  47326  chnerlem2  47332  nnmul2  47793  submodlt  47819  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartiltu  47897  iccpartgt  47902  bgoldbtbndlem2  48297  gpgedgvtx1  48553