Theorem zssinfcl 10439

Description: The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.)

Hypotheses

Ref	Expression
zssinfcl.ex	⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐵 𝑧 < 𝑦)))
zssinfcl.ss	⊢ (𝜑 → 𝐵 ⊆ ℤ)
zssinfcl.zz	⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ ℤ)

Assertion

Ref	Expression
zssinfcl	⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ 𝐵)

Distinct variable groups:   𝑥,𝐵,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧

Proof of Theorem zssinfcl

Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zssinfcl.zz	. . . . 5 ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ ℤ)
2	1	zred 9557	. . . 4 ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ ℝ)
3		1red 8149	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
4	2, 3	readdcld 8164	. . 3 ⊢ (𝜑 → (inf(𝐵, ℝ, < ) + 1) ∈ ℝ)
5	2	ltp1d 9065	. . 3 ⊢ (𝜑 → inf(𝐵, ℝ, < ) < (inf(𝐵, ℝ, < ) + 1))
6		lttri3 8214	. . . . 5 ⊢ ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
7	6	adantl 277	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
8		zssinfcl.ex	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐵 𝑧 < 𝑦)))
9	7, 8	infglbti 7180	. . 3 ⊢ (𝜑 → (((inf(𝐵, ℝ, < ) + 1) ∈ ℝ ∧ inf(𝐵, ℝ, < ) < (inf(𝐵, ℝ, < ) + 1)) → ∃𝑧 ∈ 𝐵 𝑧 < (inf(𝐵, ℝ, < ) + 1)))
10	4, 5, 9	mp2and 433	. 2 ⊢ (𝜑 → ∃𝑧 ∈ 𝐵 𝑧 < (inf(𝐵, ℝ, < ) + 1))
11	2	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → inf(𝐵, ℝ, < ) ∈ ℝ)
12		zssinfcl.ss	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ ℤ)
13	12	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → 𝐵 ⊆ ℤ)
14		simprl 529	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → 𝑧 ∈ 𝐵)
15	13, 14	sseldd 3225	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → 𝑧 ∈ ℤ)
16	15	zred 9557	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → 𝑧 ∈ ℝ)
17	7, 8	inflbti 7179	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ 𝐵 → ¬ 𝑧 < inf(𝐵, ℝ, < )))
18	17	imp 124	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ¬ 𝑧 < inf(𝐵, ℝ, < ))
19	18	adantrr 479	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → ¬ 𝑧 < inf(𝐵, ℝ, < ))
20	11, 16, 19	nltled 8255	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → inf(𝐵, ℝ, < ) ≤ 𝑧)
21		simprr 531	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → 𝑧 < (inf(𝐵, ℝ, < ) + 1))
22	1	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → inf(𝐵, ℝ, < ) ∈ ℤ)
23		zleltp1 9490	. . . . . 6 ⊢ ((𝑧 ∈ ℤ ∧ inf(𝐵, ℝ, < ) ∈ ℤ) → (𝑧 ≤ inf(𝐵, ℝ, < ) ↔ 𝑧 < (inf(𝐵, ℝ, < ) + 1)))
24	15, 22, 23	syl2anc 411	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → (𝑧 ≤ inf(𝐵, ℝ, < ) ↔ 𝑧 < (inf(𝐵, ℝ, < ) + 1)))
25	21, 24	mpbird 167	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → 𝑧 ≤ inf(𝐵, ℝ, < ))
26	11, 16	letri3d 8250	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → (inf(𝐵, ℝ, < ) = 𝑧 ↔ (inf(𝐵, ℝ, < ) ≤ 𝑧 ∧ 𝑧 ≤ inf(𝐵, ℝ, < ))))
27	20, 25, 26	mpbir2and 950	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → inf(𝐵, ℝ, < ) = 𝑧)
28	27, 14	eqeltrd 2306	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 < (inf(𝐵, ℝ, < ) + 1))) → inf(𝐵, ℝ, < ) ∈ 𝐵)
29	10, 28	rexlimddv 2653	1 ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∀wral 2508  ∃wrex 2509   ⊆ wss 3197   class class class wbr 4082  (class class class)co 5994  infcinf 7138  ℝcr 7986  1c1 7988   + caddc 7990   < clt 8169   ≤ cle 8170  ℤcz 9434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-setind 4626  ax-cnex 8078  ax-resscn 8079  ax-1cn 8080  ax-1re 8081  ax-icn 8082  ax-addcl 8083  ax-addrcl 8084  ax-mulcl 8085  ax-addcom 8087  ax-addass 8089  ax-distr 8091  ax-i2m1 8092  ax-0lt1 8093  ax-0id 8095  ax-rnegex 8096  ax-cnre 8098  ax-pre-ltirr 8099  ax-pre-ltwlin 8100  ax-pre-lttrn 8101  ax-pre-apti 8102  ax-pre-ltadd 8103

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-opab 4145  df-id 4381  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-iota 5274  df-fun 5316  df-fv 5322  df-riota 5947  df-ov 5997  df-oprab 5998  df-mpo 5999  df-sup 7139  df-inf 7140  df-pnf 8171  df-mnf 8172  df-xr 8173  df-ltxr 8174  df-le 8175  df-sub 8307  df-neg 8308  df-inn 9099  df-n0 9358  df-z 9435

This theorem is referenced by: (None)