Metamath Proof Explorer

Theorem xrsupsslem

Description: Lemma for xrsupss . (Contributed by NM, 25-Oct-2005)

Ref Expression
Assertion xrsupsslem ( ( 𝐴 ⊆ ℝ* ∧ ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 raleq ⊢ ( 𝐴 = ∅ → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ) )
2 rexeq ⊢ ( 𝐴 = ∅ → ( ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) )
3 2 imbi2d ⊢ ( 𝐴 = ∅ → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) )
4 3 ralbidv ⊢ ( 𝐴 = ∅ → ( ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) )
5 1 4 anbi12d ⊢ ( 𝐴 = ∅ → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) ) )
6 5 rexbidv ⊢ ( 𝐴 = ∅ → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) ) )
7 sup3 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
8 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
9 8 anim1i ⊢ ( ( 𝑥 ∈ ℝ ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ( 𝑥 ∈ ℝ* ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
10 9 reximi2 ⊢ ( ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
11 7 10 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
12 elxr ⊢ ( 𝑦 ∈ ℝ* ↔ ( 𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞ ) )
13 simpr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) ∧ ( 𝑦 ∈ ℝ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ( 𝑦 ∈ ℝ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
14 pnfnlt ⊢ ( 𝑥 ∈ ℝ* → ¬ +∞ < 𝑥 )
15 14 adantr ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 = +∞ ) → ¬ +∞ < 𝑥 )
16 breq1 ⊢ ( 𝑦 = +∞ → ( 𝑦 < 𝑥 ↔ +∞ < 𝑥 ) )
17 16 notbid ⊢ ( 𝑦 = +∞ → ( ¬ 𝑦 < 𝑥 ↔ ¬ +∞ < 𝑥 ) )
18 17 adantl ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 = +∞ ) → ( ¬ 𝑦 < 𝑥 ↔ ¬ +∞ < 𝑥 ) )
19 15 18 mpbird ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 = +∞ ) → ¬ 𝑦 < 𝑥 )
20 19 pm2.21d ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 = +∞ ) → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
21 20 ex ⊢ ( 𝑥 ∈ ℝ* → ( 𝑦 = +∞ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
22 21 ad2antlr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) ∧ ( 𝑦 ∈ ℝ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ( 𝑦 = +∞ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
23 ssel ⊢ ( 𝐴 ⊆ ℝ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℝ ) )
24 mnflt ⊢ ( 𝑧 ∈ ℝ → -∞ < 𝑧 )
25 23 24 syl6 ⊢ ( 𝐴 ⊆ ℝ → ( 𝑧 ∈ 𝐴 → -∞ < 𝑧 ) )
26 25 ancld ⊢ ( 𝐴 ⊆ ℝ → ( 𝑧 ∈ 𝐴 → ( 𝑧 ∈ 𝐴 ∧ -∞ < 𝑧 ) ) )
27 26 eximdv ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑧 𝑧 ∈ 𝐴 → ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ -∞ < 𝑧 ) ) )
28 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
29 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ -∞ < 𝑧 ) )
30 27 28 29 3imtr4g ⊢ ( 𝐴 ⊆ ℝ → ( 𝐴 ≠ ∅ → ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 ) )
31 30 imp ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 )
32 31 a1d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( -∞ < 𝑥 → ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 ) )
33 32 ad2antrr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 = -∞ ) → ( -∞ < 𝑥 → ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 ) )
34 breq1 ⊢ ( 𝑦 = -∞ → ( 𝑦 < 𝑥 ↔ -∞ < 𝑥 ) )
35 breq1 ⊢ ( 𝑦 = -∞ → ( 𝑦 < 𝑧 ↔ -∞ < 𝑧 ) )
36 35 rexbidv ⊢ ( 𝑦 = -∞ → ( ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 ) )
37 34 36 imbi12d ⊢ ( 𝑦 = -∞ → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( -∞ < 𝑥 → ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 ) ) )
38 37 adantl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 = -∞ ) → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( -∞ < 𝑥 → ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 ) ) )
39 33 38 mpbird ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 = -∞ ) → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
40 39 ex ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) → ( 𝑦 = -∞ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
41 40 adantr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) ∧ ( 𝑦 ∈ ℝ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ( 𝑦 = -∞ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
42 13 22 41 3jaod ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) ∧ ( 𝑦 ∈ ℝ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ( ( 𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞ ) → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
43 12 42 biimtrid ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) ∧ ( 𝑦 ∈ ℝ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ( 𝑦 ∈ ℝ* → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
44 43 ex ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) → ( ( 𝑦 ∈ ℝ → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ( 𝑦 ∈ ℝ* → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
45 44 ralimdv2 ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) → ( ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
46 45 anim2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ* ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
47 46 reximdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
48 47 3adant3 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
49 11 48 mpd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
50 49 3expa ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
51 ralnex ⊢ ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
52 rexnal ⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑥 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
53 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
54 letric ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 ≤ 𝑥 ∨ 𝑥 ≤ 𝑦 ) )
55 54 ord ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑦 ≤ 𝑥 → 𝑥 ≤ 𝑦 ) )
56 53 55 sylan ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑦 ≤ 𝑥 → 𝑥 ≤ 𝑦 ) )
57 56 an32s ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑦 ≤ 𝑥 → 𝑥 ≤ 𝑦 ) )
58 57 reximdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑥 → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
59 52 58 biimtrrid ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
60 59 ralimdva ⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
61 60 imp ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
62 51 61 sylan2br ⊢ ( ( 𝐴 ⊆ ℝ ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
63 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ≤ 𝑧 ) )
64 63 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 )
65 64 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 )
66 62 65 sylib ⊢ ( ( 𝐴 ⊆ ℝ ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 )
67 pnfxr ⊢ +∞ ∈ ℝ*
68 ssel ⊢ ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) )
69 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
70 pnfnlt ⊢ ( 𝑦 ∈ ℝ* → ¬ +∞ < 𝑦 )
71 69 70 syl ⊢ ( 𝑦 ∈ ℝ → ¬ +∞ < 𝑦 )
72 68 71 syl6 ⊢ ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ 𝐴 → ¬ +∞ < 𝑦 ) )
73 72 ralrimiv ⊢ ( 𝐴 ⊆ ℝ → ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 )
74 73 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ) → ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 )
75 peano2re ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ )
76 breq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ≤ 𝑧 ↔ ( 𝑦 + 1 ) ≤ 𝑧 ) )
77 76 rexbidv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑦 + 1 ) ≤ 𝑧 ) )
78 77 rspcva ⊢ ( ( ( 𝑦 + 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ) → ∃ 𝑧 ∈ 𝐴 ( 𝑦 + 1 ) ≤ 𝑧 )
79 78 adantrr ⊢ ( ( ( 𝑦 + 1 ) ∈ ℝ ∧ ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ∧ 𝐴 ⊆ ℝ ) ) → ∃ 𝑧 ∈ 𝐴 ( 𝑦 + 1 ) ≤ 𝑧 )
80 79 ancoms ⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑦 + 1 ) ∈ ℝ ) → ∃ 𝑧 ∈ 𝐴 ( 𝑦 + 1 ) ≤ 𝑧 )
81 75 80 sylan2 ⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ 𝐴 ( 𝑦 + 1 ) ≤ 𝑧 )
82 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
83 ltp1 ⊢ ( 𝑦 ∈ ℝ → 𝑦 < ( 𝑦 + 1 ) )
84 83 adantr ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑦 < ( 𝑦 + 1 ) )
85 75 ancli ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ) )
86 ltletr ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑦 < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) ≤ 𝑧 ) → 𝑦 < 𝑧 ) )
87 86 3expa ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝑦 < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) ≤ 𝑧 ) → 𝑦 < 𝑧 ) )
88 85 87 sylan ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑦 < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) ≤ 𝑧 ) → 𝑦 < 𝑧 ) )
89 84 88 mpand ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑦 + 1 ) ≤ 𝑧 → 𝑦 < 𝑧 ) )
90 89 ancoms ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 + 1 ) ≤ 𝑧 → 𝑦 < 𝑧 ) )
91 82 90 sylan ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 + 1 ) ≤ 𝑧 → 𝑦 < 𝑧 ) )
92 91 an32s ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 + 1 ) ≤ 𝑧 → 𝑦 < 𝑧 ) )
93 92 reximdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝑦 + 1 ) ≤ 𝑧 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
94 93 adantll ⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝑦 + 1 ) ≤ 𝑧 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
95 81 94 mpd ⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 )
96 95 exp31 ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ ℝ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
97 96 a1dd ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ( 𝐴 ⊆ ℝ → ( 𝑦 < +∞ → ( 𝑦 ∈ ℝ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
98 97 com4r ⊢ ( 𝑦 ∈ ℝ → ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ( 𝐴 ⊆ ℝ → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
99 xrltnr ⊢ ( +∞ ∈ ℝ* → ¬ +∞ < +∞ )
100 67 99 ax-mp ⊢ ¬ +∞ < +∞
101 breq1 ⊢ ( 𝑦 = +∞ → ( 𝑦 < +∞ ↔ +∞ < +∞ ) )
102 100 101 mtbiri ⊢ ( 𝑦 = +∞ → ¬ 𝑦 < +∞ )
103 102 pm2.21d ⊢ ( 𝑦 = +∞ → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
104 103 2a1d ⊢ ( 𝑦 = +∞ → ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ( 𝐴 ⊆ ℝ → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
105 0re ⊢ 0 ∈ ℝ
106 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑧 ↔ 0 ≤ 𝑧 ) )
107 106 rexbidv ⊢ ( 𝑥 = 0 → ( ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 0 ≤ 𝑧 ) )
108 107 rspcva ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ) → ∃ 𝑧 ∈ 𝐴 0 ≤ 𝑧 )
109 105 108 mpan ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ∃ 𝑧 ∈ 𝐴 0 ≤ 𝑧 )
110 82 24 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) → -∞ < 𝑧 )
111 110 a1d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) → ( 0 ≤ 𝑧 → -∞ < 𝑧 ) )
112 111 reximdva ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑧 ∈ 𝐴 0 ≤ 𝑧 → ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 ) )
113 109 112 mpan9 ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ∧ 𝐴 ⊆ ℝ ) → ∃ 𝑧 ∈ 𝐴 -∞ < 𝑧 )
114 113 36 imbitrrid ⊢ ( 𝑦 = -∞ → ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ∧ 𝐴 ⊆ ℝ ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
115 114 a1dd ⊢ ( 𝑦 = -∞ → ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ∧ 𝐴 ⊆ ℝ ) → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
116 115 expd ⊢ ( 𝑦 = -∞ → ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ( 𝐴 ⊆ ℝ → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
117 98 104 116 3jaoi ⊢ ( ( 𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞ ) → ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ( 𝐴 ⊆ ℝ → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
118 12 117 sylbi ⊢ ( 𝑦 ∈ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ( 𝐴 ⊆ ℝ → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
119 118 com13 ⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 → ( 𝑦 ∈ ℝ* → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
120 119 imp ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ) → ( 𝑦 ∈ ℝ* → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
121 120 ralrimiv ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ) → ∀ 𝑦 ∈ ℝ* ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
122 74 121 jca ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
123 breq1 ⊢ ( 𝑥 = +∞ → ( 𝑥 < 𝑦 ↔ +∞ < 𝑦 ) )
124 123 notbid ⊢ ( 𝑥 = +∞ → ( ¬ 𝑥 < 𝑦 ↔ ¬ +∞ < 𝑦 ) )
125 124 ralbidv ⊢ ( 𝑥 = +∞ → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 ) )
126 breq2 ⊢ ( 𝑥 = +∞ → ( 𝑦 < 𝑥 ↔ 𝑦 < +∞ ) )
127 126 imbi1d ⊢ ( 𝑥 = +∞ → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
128 127 ralbidv ⊢ ( 𝑥 = +∞ → ( ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ* ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
129 125 128 anbi12d ⊢ ( 𝑥 = +∞ → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
130 129 rspcev ⊢ ( ( +∞ ∈ ℝ* ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
131 67 122 130 sylancr ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑥 ≤ 𝑧 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
132 66 131 syldan ⊢ ( ( 𝐴 ⊆ ℝ ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
133 132 adantlr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
134 50 133 pm2.61dan ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
135 mnfxr ⊢ -∞ ∈ ℝ*
136 ral0 ⊢ ∀ 𝑦 ∈ ∅ ¬ -∞ < 𝑦
137 nltmnf ⊢ ( 𝑦 ∈ ℝ* → ¬ 𝑦 < -∞ )
138 137 pm2.21d ⊢ ( 𝑦 ∈ ℝ* → ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) )
139 138 rgen ⊢ ∀ 𝑦 ∈ ℝ* ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 )
140 136 139 pm3.2i ⊢ ( ∀ 𝑦 ∈ ∅ ¬ -∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) )
141 breq1 ⊢ ( 𝑥 = -∞ → ( 𝑥 < 𝑦 ↔ -∞ < 𝑦 ) )
142 141 notbid ⊢ ( 𝑥 = -∞ → ( ¬ 𝑥 < 𝑦 ↔ ¬ -∞ < 𝑦 ) )
143 142 ralbidv ⊢ ( 𝑥 = -∞ → ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ ∅ ¬ -∞ < 𝑦 ) )
144 breq2 ⊢ ( 𝑥 = -∞ → ( 𝑦 < 𝑥 ↔ 𝑦 < -∞ ) )
145 144 imbi1d ⊢ ( 𝑥 = -∞ → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ↔ ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) )
146 145 ralbidv ⊢ ( 𝑥 = -∞ → ( ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ* ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) )
147 143 146 anbi12d ⊢ ( 𝑥 = -∞ → ( ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ ∅ ¬ -∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) ) )
148 147 rspcev ⊢ ( ( -∞ ∈ ℝ* ∧ ( ∀ 𝑦 ∈ ∅ ¬ -∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < -∞ → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) )
149 135 140 148 mp2an ⊢ ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) )
150 149 a1i ⊢ ( 𝐴 ⊆ ℝ → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 < 𝑧 ) ) )
151 6 134 150 pm2.61ne ⊢ ( 𝐴 ⊆ ℝ → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
152 151 adantl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ⊆ ℝ ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
153 ssel ⊢ ( 𝐴 ⊆ ℝ* → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ* ) )
154 153 70 syl6 ⊢ ( 𝐴 ⊆ ℝ* → ( 𝑦 ∈ 𝐴 → ¬ +∞ < 𝑦 ) )
155 154 ralrimiv ⊢ ( 𝐴 ⊆ ℝ* → ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 )
156 breq2 ⊢ ( 𝑧 = +∞ → ( 𝑦 < 𝑧 ↔ 𝑦 < +∞ ) )
157 156 rspcev ⊢ ( ( +∞ ∈ 𝐴 ∧ 𝑦 < +∞ ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 )
158 157 ex ⊢ ( +∞ ∈ 𝐴 → ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
159 158 ralrimivw ⊢ ( +∞ ∈ 𝐴 → ∀ 𝑦 ∈ ℝ* ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
160 155 159 anim12i ⊢ ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ +∞ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < +∞ → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
161 67 160 130 sylancr ⊢ ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
162 152 161 jaodan ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )