ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zsupssdc GIF version

Theorem zsupssdc 11955
Description: An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 7932.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
Hypotheses
Ref Expression
zsupssdc.a (𝜑 → ðī ⊆ â„Ī)
zsupssdc.m (𝜑 → ∃ð‘Ĩ ð‘Ĩ ∈ ðī)
zsupssdc.dc (𝜑 → ∀ð‘Ĩ ∈ â„Ī DECID ð‘Ĩ ∈ ðī)
zsupssdc.ub (𝜑 → ∃ð‘Ĩ ∈ â„Ī ∀ð‘Ķ ∈ ðī ð‘Ķ â‰Ī ð‘Ĩ)
Assertion
Ref Expression
zsupssdc (𝜑 → ∃ð‘Ĩ ∈ ðī (∀ð‘Ķ ∈ ðī ÂŽ ð‘Ĩ < ð‘Ķ ∧ ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < ð‘Ĩ → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧)))
Distinct variable groups:   ð‘Ĩ,ðī,ð‘Ķ,𝑧   ð‘Ĩ,ðĩ   𝜑,ð‘Ķ
Allowed substitution hints:   𝜑(ð‘Ĩ,𝑧)   ðĩ(ð‘Ķ,𝑧)

Proof of Theorem zsupssdc
Dummy variables 𝑎 𝑚 𝑛 ð‘Ī 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zsupssdc.ub . . 3 (𝜑 → ∃ð‘Ĩ ∈ â„Ī ∀ð‘Ķ ∈ ðī ð‘Ķ â‰Ī ð‘Ĩ)
2 breq1 4007 . . . . . 6 (ð‘Ķ = 𝑚 → (ð‘Ķ â‰Ī ð‘Ĩ ↔ 𝑚 â‰Ī ð‘Ĩ))
32cbvralvw 2708 . . . . 5 (∀ð‘Ķ ∈ ðī ð‘Ķ â‰Ī ð‘Ĩ ↔ ∀𝑚 ∈ ðī 𝑚 â‰Ī ð‘Ĩ)
4 breq2 4008 . . . . . 6 (ð‘Ĩ = 𝑛 → (𝑚 â‰Ī ð‘Ĩ ↔ 𝑚 â‰Ī 𝑛))
54ralbidv 2477 . . . . 5 (ð‘Ĩ = 𝑛 → (∀𝑚 ∈ ðī 𝑚 â‰Ī ð‘Ĩ ↔ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛))
63, 5bitrid 192 . . . 4 (ð‘Ĩ = 𝑛 → (∀ð‘Ķ ∈ ðī ð‘Ķ â‰Ī ð‘Ĩ ↔ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛))
76cbvrexvw 2709 . . 3 (∃ð‘Ĩ ∈ â„Ī ∀ð‘Ķ ∈ ðī ð‘Ķ â‰Ī ð‘Ĩ ↔ ∃𝑛 ∈ â„Ī ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)
81, 7sylib 122 . 2 (𝜑 → ∃𝑛 ∈ â„Ī ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)
9 zsupssdc.m . . . . . . 7 (𝜑 → ∃ð‘Ĩ ð‘Ĩ ∈ ðī)
10 eleq1w 2238 . . . . . . . 8 (ð‘Ĩ = 𝑎 → (ð‘Ĩ ∈ ðī ↔ 𝑎 ∈ ðī))
1110cbvexv 1918 . . . . . . 7 (∃ð‘Ĩ ð‘Ĩ ∈ ðī ↔ ∃𝑎 𝑎 ∈ ðī)
129, 11sylib 122 . . . . . 6 (𝜑 → ∃𝑎 𝑎 ∈ ðī)
1312adantr 276 . . . . 5 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → ∃𝑎 𝑎 ∈ ðī)
14 uzssz 9547 . . . . . . 7 (â„Īâ‰Ĩ‘-𝑛) ⊆ â„Ī
15 rabss2 3239 . . . . . . 7 ((â„Īâ‰Ĩ‘-𝑛) ⊆ â„Ī → {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī} ⊆ {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī})
1614, 15ax-mp 5 . . . . . 6 {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī} ⊆ {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}
17 negeq 8150 . . . . . . . . . . . . . 14 (𝑏 = ð‘Ī → -𝑏 = -ð‘Ī)
1817eleq1d 2246 . . . . . . . . . . . . 13 (𝑏 = ð‘Ī → (-𝑏 ∈ ðī ↔ -ð‘Ī ∈ ðī))
19 simp1rl 1062 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → 𝑛 ∈ â„Ī)
2019znegcld 9377 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → -𝑛 ∈ â„Ī)
21 simp2 998 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → ð‘Ī ∈ â„Ī)
2221zred 9375 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → ð‘Ī ∈ ℝ)
2319zred 9375 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → 𝑛 ∈ ℝ)
24 breq1 4007 . . . . . . . . . . . . . . . 16 (𝑚 = -ð‘Ī → (𝑚 â‰Ī 𝑛 ↔ -ð‘Ī â‰Ī 𝑛))
25 simp1rr 1063 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)
26 simp3 999 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → -ð‘Ī ∈ ðī)
2724, 25, 26rspcdva 2847 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → -ð‘Ī â‰Ī 𝑛)
2822, 23, 27lenegcon1d 8484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → -𝑛 â‰Ī ð‘Ī)
29 eluz2 9534 . . . . . . . . . . . . . 14 (ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) ↔ (-𝑛 ∈ â„Ī ∧ ð‘Ī ∈ â„Ī ∧ -𝑛 â‰Ī ð‘Ī))
3020, 21, 28, 29syl3anbrc 1181 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛))
3118, 30, 26elrabd 2896 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ â„Ī ∧ -ð‘Ī ∈ ðī) → ð‘Ī ∈ {𝑏 ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -𝑏 ∈ ðī})
3231rabssdv 3236 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī} ⊆ {𝑏 ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -𝑏 ∈ ðī})
3318cbvrabv 2737 . . . . . . . . . . 11 {𝑏 ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -𝑏 ∈ ðī} = {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī}
3432, 33sseqtrdi 3204 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī} ⊆ {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī})
3516a1i 9 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī} ⊆ {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī})
3634, 35eqssd 3173 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī} = {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī})
3736infeq1d 7011 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) = inf({ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ))
3837adantr 276 . . . . . . 7 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) = inf({ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ))
39 simprl 529 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → 𝑛 ∈ â„Ī)
4039znegcld 9377 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → -𝑛 ∈ â„Ī)
4140adantr 276 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → -𝑛 ∈ â„Ī)
42 eqid 2177 . . . . . . . 8 {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī} = {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī}
43 negeq 8150 . . . . . . . . . 10 (ð‘Ī = -𝑎 → -ð‘Ī = --𝑎)
4443eleq1d 2246 . . . . . . . . 9 (ð‘Ī = -𝑎 → (-ð‘Ī ∈ ðī ↔ --𝑎 ∈ ðī))
45 zsupssdc.a . . . . . . . . . . . . 13 (𝜑 → ðī ⊆ â„Ī)
4645ad2antrr 488 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → ðī ⊆ â„Ī)
47 simpr 110 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → 𝑎 ∈ ðī)
4846, 47sseldd 3157 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → 𝑎 ∈ â„Ī)
4948znegcld 9377 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → -𝑎 ∈ â„Ī)
50 breq1 4007 . . . . . . . . . . . 12 (𝑚 = 𝑎 → (𝑚 â‰Ī 𝑛 ↔ 𝑎 â‰Ī 𝑛))
51 simplrr 536 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)
5250, 51, 47rspcdva 2847 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → 𝑎 â‰Ī 𝑛)
5348zred 9375 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → 𝑎 ∈ ℝ)
5439adantr 276 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → 𝑛 ∈ â„Ī)
5554zred 9375 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → 𝑛 ∈ ℝ)
5653, 55lenegd 8481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → (𝑎 â‰Ī 𝑛 ↔ -𝑛 â‰Ī -𝑎))
5752, 56mpbid 147 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → -𝑛 â‰Ī -𝑎)
58 eluz2 9534 . . . . . . . . . 10 (-𝑎 ∈ (â„Īâ‰Ĩ‘-𝑛) ↔ (-𝑛 ∈ â„Ī ∧ -𝑎 ∈ â„Ī ∧ -𝑛 â‰Ī -𝑎))
5941, 49, 57, 58syl3anbrc 1181 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → -𝑎 ∈ (â„Īâ‰Ĩ‘-𝑛))
6048zcnd 9376 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → 𝑎 ∈ ℂ)
6160negnegd 8259 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → --𝑎 = 𝑎)
6261, 47eqeltrd 2254 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → --𝑎 ∈ ðī)
6344, 59, 62elrabd 2896 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → -𝑎 ∈ {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī})
64 eleq1 2240 . . . . . . . . . . 11 (ð‘Ĩ = -ð‘Ī → (ð‘Ĩ ∈ ðī ↔ -ð‘Ī ∈ ðī))
6564dcbid 838 . . . . . . . . . 10 (ð‘Ĩ = -ð‘Ī → (DECID ð‘Ĩ ∈ ðī ↔ DECID -ð‘Ī ∈ ðī))
66 zsupssdc.dc . . . . . . . . . . 11 (𝜑 → ∀ð‘Ĩ ∈ â„Ī DECID ð‘Ĩ ∈ ðī)
6766ad2antrr 488 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ (-𝑛...-𝑎)) → ∀ð‘Ĩ ∈ â„Ī DECID ð‘Ĩ ∈ ðī)
68 elfzelz 10025 . . . . . . . . . . . 12 (ð‘Ī ∈ (-𝑛...-𝑎) → ð‘Ī ∈ â„Ī)
6968adantl 277 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ (-𝑛...-𝑎)) → ð‘Ī ∈ â„Ī)
7069znegcld 9377 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ (-𝑛...-𝑎)) → -ð‘Ī ∈ â„Ī)
7165, 67, 70rspcdva 2847 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ ð‘Ī ∈ (-𝑛...-𝑎)) → DECID -ð‘Ī ∈ ðī)
7271adantlr 477 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) ∧ ð‘Ī ∈ (-𝑛...-𝑎)) → DECID -ð‘Ī ∈ ðī)
7341, 42, 63, 72infssuzcldc 11952 . . . . . . 7 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → inf({ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī})
7438, 73eqeltrd 2254 . . . . . 6 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ {ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī})
7516, 74sselid 3154 . . . . 5 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī})
7613, 75exlimddv 1898 . . . 4 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī})
77 negeq 8150 . . . . . . 7 (𝑛 = inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → -𝑛 = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ))
7877eleq1d 2246 . . . . . 6 (𝑛 = inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → (-𝑛 ∈ ðī ↔ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ðī))
79 negeq 8150 . . . . . . . 8 (ð‘Ī = 𝑛 → -ð‘Ī = -𝑛)
8079eleq1d 2246 . . . . . . 7 (ð‘Ī = 𝑛 → (-ð‘Ī ∈ ðī ↔ -𝑛 ∈ ðī))
8180cbvrabv 2737 . . . . . 6 {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī} = {𝑛 ∈ â„Ī âˆĢ -𝑛 ∈ ðī}
8278, 81elrab2 2897 . . . . 5 (inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī} ↔ (inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ â„Ī ∧ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ðī))
8382simprbi 275 . . . 4 (inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī} → -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ðī)
8476, 83syl 14 . . 3 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ðī)
85 ssrab2 3241 . . . . . . . . 9 {ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī} ⊆ â„Ī
8685, 75sselid 3154 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ â„Ī)
8786zred 9375 . . . . . . 7 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ℝ)
8887renegcld 8337 . . . . . 6 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ℝ)
8941, 42, 63, 72infssuzledc 11951 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → inf({ð‘Ī ∈ (â„Īâ‰Ĩ‘-𝑛) âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) â‰Ī -𝑎)
9038, 89eqbrtrd 4026 . . . . . . 7 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) â‰Ī -𝑎)
9187, 53, 90lenegcon2d 8485 . . . . . 6 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → 𝑎 â‰Ī -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ))
9253, 88, 91lensymd 8079 . . . . 5 (((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) ∧ 𝑎 ∈ ðī) → ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < 𝑎)
9392ralrimiva 2550 . . . 4 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → ∀𝑎 ∈ ðī ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < 𝑎)
94 breq2 4008 . . . . . 6 (𝑎 = ð‘Ķ → (-inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < 𝑎 ↔ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ))
9594notbid 667 . . . . 5 (𝑎 = ð‘Ķ → (ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < 𝑎 ↔ ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ))
9695cbvralv 2704 . . . 4 (∀𝑎 ∈ ðī ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < 𝑎 ↔ ∀ð‘Ķ ∈ ðī ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ)
9793, 96sylib 122 . . 3 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → ∀ð‘Ķ ∈ ðī ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ)
98 breq2 4008 . . . . . . 7 (𝑧 = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → (ð‘Ķ < 𝑧 ↔ ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < )))
9998rspcev 2842 . . . . . 6 ((-inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ðī ∧ ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < )) → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧)
10099ex 115 . . . . 5 (-inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ðī → (ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧))
10184, 100syl 14 . . . 4 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → (ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧))
102101ralrimivw 2551 . . 3 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧))
103 breq1 4007 . . . . . . 7 (ð‘Ĩ = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → (ð‘Ĩ < ð‘Ķ ↔ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ))
104103notbid 667 . . . . . 6 (ð‘Ĩ = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → (ÂŽ ð‘Ĩ < ð‘Ķ ↔ ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ))
105104ralbidv 2477 . . . . 5 (ð‘Ĩ = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → (∀ð‘Ķ ∈ ðī ÂŽ ð‘Ĩ < ð‘Ķ ↔ ∀ð‘Ķ ∈ ðī ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ))
106 breq2 4008 . . . . . . 7 (ð‘Ĩ = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → (ð‘Ķ < ð‘Ĩ ↔ ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < )))
107106imbi1d 231 . . . . . 6 (ð‘Ĩ = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ((ð‘Ķ < ð‘Ĩ → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧) ↔ (ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧)))
108107ralbidv 2477 . . . . 5 (ð‘Ĩ = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → (∀ð‘Ķ ∈ ðĩ (ð‘Ķ < ð‘Ĩ → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧) ↔ ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧)))
109105, 108anbi12d 473 . . . 4 (ð‘Ĩ = -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ((∀ð‘Ķ ∈ ðī ÂŽ ð‘Ĩ < ð‘Ķ ∧ ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < ð‘Ĩ → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧)) ↔ (∀ð‘Ķ ∈ ðī ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ ∧ ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧))))
110109rspcev 2842 . . 3 ((-inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) ∈ ðī ∧ (∀ð‘Ķ ∈ ðī ÂŽ -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) < ð‘Ķ ∧ ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < -inf({ð‘Ī ∈ â„Ī âˆĢ -ð‘Ī ∈ ðī}, ℝ, < ) → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧))) → ∃ð‘Ĩ ∈ ðī (∀ð‘Ķ ∈ ðī ÂŽ ð‘Ĩ < ð‘Ķ ∧ ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < ð‘Ĩ → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧)))
11184, 97, 102, 110syl12anc 1236 . 2 ((𝜑 ∧ (𝑛 ∈ â„Ī ∧ ∀𝑚 ∈ ðī 𝑚 â‰Ī 𝑛)) → ∃ð‘Ĩ ∈ ðī (∀ð‘Ķ ∈ ðī ÂŽ ð‘Ĩ < ð‘Ķ ∧ ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < ð‘Ĩ → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧)))
1128, 111rexlimddv 2599 1 (𝜑 → ∃ð‘Ĩ ∈ ðī (∀ð‘Ķ ∈ ðī ÂŽ ð‘Ĩ < ð‘Ķ ∧ ∀ð‘Ķ ∈ ðĩ (ð‘Ķ < ð‘Ĩ → ∃𝑧 ∈ ðī ð‘Ķ < 𝑧)))
Colors of variables: wff set class
Syntax hints:  ÂŽ wn 3   → wi 4   ∧ wa 104  DECID wdc 834   ∧ w3a 978   = wceq 1353  âˆƒwex 1492   ∈ wcel 2148  âˆ€wral 2455  âˆƒwrex 2456  {crab 2459   ⊆ wss 3130   class class class wbr 4004  â€˜cfv 5217  (class class class)co 5875  infcinf 6982  â„cr 7810   < clt 7992   â‰Ī cle 7993  -cneg 8129  â„Īcz 9253  â„Īâ‰Ĩcuz 9528  ...cfz 10008
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-addcom 7911  ax-addass 7913  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-0id 7919  ax-rnegex 7920  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-apti 7926  ax-pre-ltadd 7927
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-po 4297  df-iso 4298  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-isom 5226  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-sup 6983  df-inf 6984  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-sub 8130  df-neg 8131  df-inn 8920  df-n0 9177  df-z 9254  df-uz 9529  df-fz 10009  df-fzo 10143
This theorem is referenced by:  suprzcl2dc  11956
  Copyright terms: Public domain W3C validator