Metamath Proof Explorer

Theorem xrinfmsslem

Description: Lemma for xrinfmss . (Contributed by NM, 19-Jan-2006)

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

Proof

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