Metamath Proof Explorer

Theorem xrge0infss

Description: Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion xrge0infss ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 ssel2 ⊢ ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ( 0 [,] +∞ ) )
2 0xr ⊢ 0 ∈ ℝ*
3 pnfxr ⊢ +∞ ∈ ℝ*
4 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝑦 )
5 2 3 4 mp3an12 ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝑦 )
6 eliccxr ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → 𝑦 ∈ ℝ* )
7 xrlenlt ⊢ ( ( 0 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 0 ≤ 𝑦 ↔ ¬ 𝑦 < 0 ) )
8 2 6 7 sylancr ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ( 0 ≤ 𝑦 ↔ ¬ 𝑦 < 0 ) )
9 5 8 mpbid ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ¬ 𝑦 < 0 )
10 1 9 syl ⊢ ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑦 ∈ 𝐴 ) → ¬ 𝑦 < 0 )
11 10 ralrimiva ⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 0 )
12 11 ad3antrrr ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ∧ 𝑤 ≤ 0 ) → ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 0 )
13 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
14 ssralv ⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
15 13 14 ax-mp ⊢ ( ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
16 simplll ⊢ ( ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝑦 ) → 𝑤 ∈ ℝ* )
17 2 a1i ⊢ ( ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝑦 ) → 0 ∈ ℝ* )
18 simplr ⊢ ( ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝑦 ) → 𝑦 ∈ ( 0 [,] +∞ ) )
19 13 18 sseldi ⊢ ( ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝑦 ) → 𝑦 ∈ ℝ* )
20 simpllr ⊢ ( ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝑦 ) → 𝑤 ≤ 0 )
21 simpr ⊢ ( ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝑦 ) → 0 < 𝑦 )
22 16 17 19 20 21 xrlelttrd ⊢ ( ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝑦 ) → 𝑤 < 𝑦 )
23 22 ex ⊢ ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 0 < 𝑦 → 𝑤 < 𝑦 ) )
24 23 imim1d ⊢ ( ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) → ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
25 24 ralimdva ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) → ( ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
26 15 25 syl5 ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝑤 ≤ 0 ) → ( ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
27 26 adantll ⊢ ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ 𝑤 ≤ 0 ) → ( ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
28 27 imp ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ 𝑤 ≤ 0 ) ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
29 28 adantrl ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ 𝑤 ≤ 0 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
30 29 an32s ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ∧ 𝑤 ≤ 0 ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
31 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
32 breq2 ⊢ ( 𝑥 = 0 → ( 𝑦 < 𝑥 ↔ 𝑦 < 0 ) )
33 32 notbid ⊢ ( 𝑥 = 0 → ( ¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < 0 ) )
34 33 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 0 ) )
35 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 < 𝑦 ↔ 0 < 𝑦 ) )
36 35 imbi1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ↔ ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
37 36 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ↔ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
38 34 37 anbi12d ⊢ ( 𝑥 = 0 → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 0 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
39 38 rspcev ⊢ ( ( 0 ∈ ( 0 [,] +∞ ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 0 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
40 31 39 mpan ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 0 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 0 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
41 12 30 40 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ∧ 𝑤 ≤ 0 ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
42 simpllr ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ∧ 0 ≤ 𝑤 ) → 𝑤 ∈ ℝ* )
43 simpr ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ∧ 0 ≤ 𝑤 ) → 0 ≤ 𝑤 )
44 elxrge0 ⊢ ( 𝑤 ∈ ( 0 [,] +∞ ) ↔ ( 𝑤 ∈ ℝ* ∧ 0 ≤ 𝑤 ) )
45 42 43 44 sylanbrc ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ∧ 0 ≤ 𝑤 ) → 𝑤 ∈ ( 0 [,] +∞ ) )
46 15 a1i ⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → ( ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) → ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
47 46 anim2d ⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
48 47 adantr ⊢ ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
49 48 imp ⊢ ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
50 49 adantr ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ∧ 0 ≤ 𝑤 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
51 breq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑦 < 𝑥 ↔ 𝑦 < 𝑤 ) )
52 51 notbid ⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < 𝑤 ) )
53 52 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ) )
54 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 < 𝑦 ↔ 𝑤 < 𝑦 ) )
55 54 imbi1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ↔ ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
56 55 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ↔ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
57 53 56 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
58 57 rspcev ⊢ ( ( 𝑤 ∈ ( 0 [,] +∞ ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
59 45 50 58 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ∧ 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
60 simplr ⊢ ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → 𝑤 ∈ ℝ* )
61 2 a1i ⊢ ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → 0 ∈ ℝ* )
62 xrletri ⊢ ( ( 𝑤 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 𝑤 ≤ 0 ∨ 0 ≤ 𝑤 ) )
63 60 61 62 syl2anc ⊢ ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → ( 𝑤 ≤ 0 ∨ 0 ≤ 𝑤 ) )
64 41 59 63 mpjaodan ⊢ ( ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ℝ* ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
65 sstr ⊢ ( ( 𝐴 ⊆ ( 0 [,] +∞ ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
66 13 65 mpan2 ⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → 𝐴 ⊆ ℝ* )
67 xrinfmss ⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑤 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
68 66 67 syl ⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∃ 𝑤 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑤 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑤 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
69 64 68 r19.29a ⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )