Theorem elfzoel2 13396

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 4268	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ≠ ∅)
2		fzof 13394	. . . . . 6 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
3	2	fdmi 6604	. . . . 5 ⊢ dom ..^ = (ℤ × ℤ)
4	3	ndmov 7446	. . . 4 ⊢ (¬ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) = ∅)
5	4	necon1ai 2971	. . 3 ⊢ ((𝐵..^𝐶) ≠ ∅ → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
6	1, 5	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
7	6	simprd 496	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ≠ wne 2943  ∅c0 4256  𝒫 cpw 4533   × cxp 5582  (class class class)co 7267  ℤcz 12329  ..^cfzo 13392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pr 5350  ax-un 7578  ax-cnex 10937  ax-resscn 10938

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5074  df-opab 5136  df-mpt 5157  df-id 5484  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-fv 6434  df-ov 7270  df-oprab 7271  df-mpo 7272  df-1st 7820  df-2nd 7821  df-neg 11218  df-z 12330  df-uz 12593  df-fz 13250  df-fzo 13393

This theorem is referenced by:  elfzoelz  13397  elfzo2  13400  elfzole1  13405  elfzolt2  13406  elfzolt3  13407  elfzolt2b  13408  elfzolt3b  13409  elfzop1le2  13410  fzonel  13411  elfzouz2  13412  fzonnsub  13422  fzoss1  13424  fzospliti  13429  fzodisj  13431  fzoaddel  13450  fzo0addelr  13452  elfzoext  13454  elincfzoext  13455  fzosubel  13456  fzoend  13488  ssfzo12  13490  fzofzp1  13494  elfzo1elm1fzo0  13498  fzonfzoufzol  13500  elfznelfzob  13503  peano2fzor  13504  fzostep1  13513  modsumfzodifsn  13674  addmodlteq  13676  cshwidxm1  14530  cshimadifsn0  14553  fzomaxdiflem  15064  fzo0dvdseq  16042  fzocongeq  16043  addmodlteqALT  16044  efgsp1  19353  efgsres  19354  crctcshwlkn0lem2  28184  crctcshwlkn0lem3  28185  crctcshwlkn0lem5  28187  crctcshwlkn0lem6  28188  crctcshwlkn0  28194  crctcsh  28197  eucrctshift  28615  eucrct2eupth  28617  fzssfzo  32526  signsvfn  32569  elfzolem1  42841  dvnmul  43465  iblspltprt  43495  stoweidlem3  43525  fourierdlem12  43641  fourierdlem50  43678  fourierdlem64  43692  fourierdlem79  43707  fzoopth  44797  iccpartiltu  44852  iccpartgt  44857  bgoldbtbndlem2  45236  natglobalincr  46490