Theorem elfzoel2 13572

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ≠ wne 2930  ∅c0 4283  𝒫 cpw 4552   × cxp 5620  (class class class)co 7356  ℤcz 12486  ..^cfzo 13568

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-neg 11365  df-z 12487  df-uz 12750  df-fz 13422  df-fzo 13569

This theorem is referenced by:  elfzoelz  13573  elfzo2  13576  elfzole1  13581  elfzolt2  13582  elfzolt3  13583  elfzolt2b  13584  elfzolt3b  13585  elfzop1le2  13586  fzonel  13587  elfzouz2  13588  fzonnsub  13598  fzoss1  13600  fzospliti  13605  fzodisj  13607  elfzolem1  13618  elfzo0subge1  13619  elfzo0suble  13620  fzoaddel  13631  fzo0addelr  13633  elfzoextl  13635  elfzoext  13636  elincfzoext  13637  fzosubel  13638  fzoend  13671  ssfzo12  13673  fzoopth  13676  fzofzp1  13678  elfzo1elm1fzo0  13682  fzonfzoufzol  13685  elfznelfzob  13688  peano2fzor  13689  fzostep1  13700  modsumfzodifsn  13865  addmodlteq  13867  cshwidxm1  14728  cshimadifsn0  14751  fzomaxdiflem  15264  fzo0dvdseq  16248  fzocongeq  16249  addmodlteqALT  16250  efgsp1  19664  efgsres  19665  crctcshwlkn0lem2  29833  crctcshwlkn0lem3  29834  crctcshwlkn0lem5  29836  crctcshwlkn0lem6  29837  crctcshwlkn0  29843  crctcsh  29846  eucrctshift  30267  eucrct2eupth  30269  fzssfzo  34645  signsvfn  34688  dvnmul  46129  iblspltprt  46159  stoweidlem3  46189  fourierdlem12  46305  fourierdlem50  46342  fourierdlem64  46356  fourierdlem79  46371  ormkglobd  47061  natglobalincr  47063  chnerlem2  47069  submodlt  47538  iccpartiltu  47610  iccpartgt  47615  bgoldbtbndlem2  47994  gpgedgvtx1  48250