MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrsupsslem Structured version   Visualization version   GIF version

Theorem xrsupsslem 12539
Description: Lemma for xrsupss 12541. (Contributed by NM, 25-Oct-2005.)
Assertion
Ref Expression
xrsupsslem ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Proof of Theorem xrsupsslem
StepHypRef Expression
1 raleq 3362 . . . . . 6 (𝐴 = ∅ → (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ ∅ ¬ 𝑥 < 𝑦))
2 rexeq 3363 . . . . . . . 8 (𝐴 = ∅ → (∃𝑧𝐴 𝑦 < 𝑧 ↔ ∃𝑧 ∈ ∅ 𝑦 < 𝑧))
32imbi2d 342 . . . . . . 7 (𝐴 = ∅ → ((𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧)))
43ralbidv 3162 . . . . . 6 (𝐴 = ∅ → (∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧)))
51, 4anbi12d 630 . . . . 5 (𝐴 = ∅ → ((∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧))))
65rexbidv 3257 . . . 4 (𝐴 = ∅ → (∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) ↔ ∃𝑥 ∈ ℝ* (∀𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧))))
7 sup3 11435 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
8 rexr 10522 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
98anim1i 614 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))) → (𝑥 ∈ ℝ* ∧ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
109reximi2 3206 . . . . . . . 8 (∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
117, 10syl 17 . . . . . . 7 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
12 elxr 12350 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* ↔ (𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞))
13 simpr 485 . . . . . . . . . . . . . 14 ((((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) ∧ (𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))) → (𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
14 pnfnlt 12362 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ* → ¬ +∞ < 𝑥)
1514adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ*𝑦 = +∞) → ¬ +∞ < 𝑥)
16 breq1 4959 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = +∞ → (𝑦 < 𝑥 ↔ +∞ < 𝑥))
1716notbid 319 . . . . . . . . . . . . . . . . . . 19 (𝑦 = +∞ → (¬ 𝑦 < 𝑥 ↔ ¬ +∞ < 𝑥))
1817adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ*𝑦 = +∞) → (¬ 𝑦 < 𝑥 ↔ ¬ +∞ < 𝑥))
1915, 18mpbird 258 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ*𝑦 = +∞) → ¬ 𝑦 < 𝑥)
2019pm2.21d 121 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ*𝑦 = +∞) → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))
2120ex 413 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ* → (𝑦 = +∞ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
2221ad2antlr 723 . . . . . . . . . . . . . 14 ((((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) ∧ (𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))) → (𝑦 = +∞ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
23 ssel 3878 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ⊆ ℝ → (𝑧𝐴𝑧 ∈ ℝ))
24 mnflt 12357 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ → -∞ < 𝑧)
2523, 24syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ⊆ ℝ → (𝑧𝐴 → -∞ < 𝑧))
2625ancld 551 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ⊆ ℝ → (𝑧𝐴 → (𝑧𝐴 ∧ -∞ < 𝑧)))
2726eximdv 1893 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ⊆ ℝ → (∃𝑧 𝑧𝐴 → ∃𝑧(𝑧𝐴 ∧ -∞ < 𝑧)))
28 n0 4224 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ≠ ∅ ↔ ∃𝑧 𝑧𝐴)
29 df-rex 3109 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑧𝐴 -∞ < 𝑧 ↔ ∃𝑧(𝑧𝐴 ∧ -∞ < 𝑧))
3027, 28, 293imtr4g 297 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ⊆ ℝ → (𝐴 ≠ ∅ → ∃𝑧𝐴 -∞ < 𝑧))
3130imp 407 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → ∃𝑧𝐴 -∞ < 𝑧)
3231a1d 25 . . . . . . . . . . . . . . . . . 18 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (-∞ < 𝑥 → ∃𝑧𝐴 -∞ < 𝑧))
3332ad2antrr 722 . . . . . . . . . . . . . . . . 17 ((((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 = -∞) → (-∞ < 𝑥 → ∃𝑧𝐴 -∞ < 𝑧))
34 breq1 4959 . . . . . . . . . . . . . . . . . . 19 (𝑦 = -∞ → (𝑦 < 𝑥 ↔ -∞ < 𝑥))
35 breq1 4959 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = -∞ → (𝑦 < 𝑧 ↔ -∞ < 𝑧))
3635rexbidv 3257 . . . . . . . . . . . . . . . . . . 19 (𝑦 = -∞ → (∃𝑧𝐴 𝑦 < 𝑧 ↔ ∃𝑧𝐴 -∞ < 𝑧))
3734, 36imbi12d 346 . . . . . . . . . . . . . . . . . 18 (𝑦 = -∞ → ((𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ (-∞ < 𝑥 → ∃𝑧𝐴 -∞ < 𝑧)))
3837adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 = -∞) → ((𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ (-∞ < 𝑥 → ∃𝑧𝐴 -∞ < 𝑧)))
3933, 38mpbird 258 . . . . . . . . . . . . . . . 16 ((((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) ∧ 𝑦 = -∞) → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))
4039ex 413 . . . . . . . . . . . . . . 15 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) → (𝑦 = -∞ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
4140adantr 481 . . . . . . . . . . . . . 14 ((((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) ∧ (𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))) → (𝑦 = -∞ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
4213, 22, 413jaod 1419 . . . . . . . . . . . . 13 ((((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) ∧ (𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))) → ((𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞) → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
4312, 42syl5bi 243 . . . . . . . . . . . 12 ((((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) ∧ (𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))) → (𝑦 ∈ ℝ* → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
4443ex 413 . . . . . . . . . . 11 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) → ((𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) → (𝑦 ∈ ℝ* → (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
4544ralimdv2 3141 . . . . . . . . . 10 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) → ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
4645anim2d 611 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ*) → ((∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) → (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
4746reximdva 3234 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
48473adant3 1123 . . . . . . 7 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → (∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))))
4911, 48mpd 15 . . . . . 6 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
50493expa 1109 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
51 ralnex 3198 . . . . . . . . 9 (∀𝑥 ∈ ℝ ¬ ∀𝑦𝐴 𝑦𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
52 rexnal 3200 . . . . . . . . . . . 12 (∃𝑦𝐴 ¬ 𝑦𝑥 ↔ ¬ ∀𝑦𝐴 𝑦𝑥)
53 ssel2 3879 . . . . . . . . . . . . . . 15 ((𝐴 ⊆ ℝ ∧ 𝑦𝐴) → 𝑦 ∈ ℝ)
54 letric 10576 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦𝑥𝑥𝑦))
5554ord 859 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (¬ 𝑦𝑥𝑥𝑦))
5653, 55sylan 580 . . . . . . . . . . . . . 14 (((𝐴 ⊆ ℝ ∧ 𝑦𝐴) ∧ 𝑥 ∈ ℝ) → (¬ 𝑦𝑥𝑥𝑦))
5756an32s 648 . . . . . . . . . . . . 13 (((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑦𝐴) → (¬ 𝑦𝑥𝑥𝑦))
5857reximdva 3234 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (∃𝑦𝐴 ¬ 𝑦𝑥 → ∃𝑦𝐴 𝑥𝑦))
5952, 58syl5bir 244 . . . . . . . . . . 11 ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (¬ ∀𝑦𝐴 𝑦𝑥 → ∃𝑦𝐴 𝑥𝑦))
6059ralimdva 3142 . . . . . . . . . 10 (𝐴 ⊆ ℝ → (∀𝑥 ∈ ℝ ¬ ∀𝑦𝐴 𝑦𝑥 → ∀𝑥 ∈ ℝ ∃𝑦𝐴 𝑥𝑦))
6160imp 407 . . . . . . . . 9 ((𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ ℝ ¬ ∀𝑦𝐴 𝑦𝑥) → ∀𝑥 ∈ ℝ ∃𝑦𝐴 𝑥𝑦)
6251, 61sylan2br 594 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → ∀𝑥 ∈ ℝ ∃𝑦𝐴 𝑥𝑦)
63 breq2 4960 . . . . . . . . . 10 (𝑦 = 𝑧 → (𝑥𝑦𝑥𝑧))
6463cbvrexv 3401 . . . . . . . . 9 (∃𝑦𝐴 𝑥𝑦 ↔ ∃𝑧𝐴 𝑥𝑧)
6564ralbii 3130 . . . . . . . 8 (∀𝑥 ∈ ℝ ∃𝑦𝐴 𝑥𝑦 ↔ ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧)
6662, 65sylib 219 . . . . . . 7 ((𝐴 ⊆ ℝ ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧)
67 pnfxr 10530 . . . . . . . 8 +∞ ∈ ℝ*
68 ssel 3878 . . . . . . . . . . . 12 (𝐴 ⊆ ℝ → (𝑦𝐴𝑦 ∈ ℝ))
69 rexr 10522 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → 𝑦 ∈ ℝ*)
70 pnfnlt 12362 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → ¬ +∞ < 𝑦)
7169, 70syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → ¬ +∞ < 𝑦)
7268, 71syl6 35 . . . . . . . . . . 11 (𝐴 ⊆ ℝ → (𝑦𝐴 → ¬ +∞ < 𝑦))
7372ralrimiv 3146 . . . . . . . . . 10 (𝐴 ⊆ ℝ → ∀𝑦𝐴 ¬ +∞ < 𝑦)
7473adantr 481 . . . . . . . . 9 ((𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧) → ∀𝑦𝐴 ¬ +∞ < 𝑦)
75 peano2re 10649 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ)
76 breq1 4959 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑦 + 1) → (𝑥𝑧 ↔ (𝑦 + 1) ≤ 𝑧))
7776rexbidv 3257 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑦 + 1) → (∃𝑧𝐴 𝑥𝑧 ↔ ∃𝑧𝐴 (𝑦 + 1) ≤ 𝑧))
7877rspcva 3552 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧) → ∃𝑧𝐴 (𝑦 + 1) ≤ 𝑧)
7978adantrr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1) ∈ ℝ ∧ (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧𝐴 ⊆ ℝ)) → ∃𝑧𝐴 (𝑦 + 1) ≤ 𝑧)
8079ancoms 459 . . . . . . . . . . . . . . . . . . 19 (((∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧𝐴 ⊆ ℝ) ∧ (𝑦 + 1) ∈ ℝ) → ∃𝑧𝐴 (𝑦 + 1) ≤ 𝑧)
8175, 80sylan2 592 . . . . . . . . . . . . . . . . . 18 (((∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧𝐴 ⊆ ℝ) ∧ 𝑦 ∈ ℝ) → ∃𝑧𝐴 (𝑦 + 1) ≤ 𝑧)
82 ssel2 3879 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ⊆ ℝ ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
83 ltp1 11317 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℝ → 𝑦 < (𝑦 + 1))
8483adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑦 < (𝑦 + 1))
8575ancli 549 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℝ → (𝑦 ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ))
86 ltletr 10568 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 < (𝑦 + 1) ∧ (𝑦 + 1) ≤ 𝑧) → 𝑦 < 𝑧))
87863expa 1109 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((𝑦 < (𝑦 + 1) ∧ (𝑦 + 1) ≤ 𝑧) → 𝑦 < 𝑧))
8885, 87sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 < (𝑦 + 1) ∧ (𝑦 + 1) ≤ 𝑧) → 𝑦 < 𝑧))
8984, 88mpand 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 + 1) ≤ 𝑧𝑦 < 𝑧))
9089ancoms 459 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 + 1) ≤ 𝑧𝑦 < 𝑧))
9182, 90sylan 580 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ⊆ ℝ ∧ 𝑧𝐴) ∧ 𝑦 ∈ ℝ) → ((𝑦 + 1) ≤ 𝑧𝑦 < 𝑧))
9291an32s 648 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧𝐴) → ((𝑦 + 1) ≤ 𝑧𝑦 < 𝑧))
9392reximdva 3234 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) → (∃𝑧𝐴 (𝑦 + 1) ≤ 𝑧 → ∃𝑧𝐴 𝑦 < 𝑧))
9493adantll 710 . . . . . . . . . . . . . . . . . 18 (((∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧𝐴 ⊆ ℝ) ∧ 𝑦 ∈ ℝ) → (∃𝑧𝐴 (𝑦 + 1) ≤ 𝑧 → ∃𝑧𝐴 𝑦 < 𝑧))
9581, 94mpd 15 . . . . . . . . . . . . . . . . 17 (((∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧𝐴 ⊆ ℝ) ∧ 𝑦 ∈ ℝ) → ∃𝑧𝐴 𝑦 < 𝑧)
9695exp31 420 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → (𝐴 ⊆ ℝ → (𝑦 ∈ ℝ → ∃𝑧𝐴 𝑦 < 𝑧)))
9796a1dd 50 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → (𝐴 ⊆ ℝ → (𝑦 < +∞ → (𝑦 ∈ ℝ → ∃𝑧𝐴 𝑦 < 𝑧))))
9897com4r 94 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ → (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → (𝐴 ⊆ ℝ → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))))
99 xrltnr 12353 . . . . . . . . . . . . . . . . . 18 (+∞ ∈ ℝ* → ¬ +∞ < +∞)
10067, 99ax-mp 5 . . . . . . . . . . . . . . . . 17 ¬ +∞ < +∞
101 breq1 4959 . . . . . . . . . . . . . . . . 17 (𝑦 = +∞ → (𝑦 < +∞ ↔ +∞ < +∞))
102100, 101mtbiri 328 . . . . . . . . . . . . . . . 16 (𝑦 = +∞ → ¬ 𝑦 < +∞)
103102pm2.21d 121 . . . . . . . . . . . . . . 15 (𝑦 = +∞ → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))
1041032a1d 26 . . . . . . . . . . . . . 14 (𝑦 = +∞ → (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → (𝐴 ⊆ ℝ → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))))
105 0re 10478 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
106 breq1 4959 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 0 → (𝑥𝑧 ↔ 0 ≤ 𝑧))
107106rexbidv 3257 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (∃𝑧𝐴 𝑥𝑧 ↔ ∃𝑧𝐴 0 ≤ 𝑧))
108107rspcva 3552 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℝ ∧ ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧) → ∃𝑧𝐴 0 ≤ 𝑧)
109105, 108mpan 686 . . . . . . . . . . . . . . . . . 18 (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → ∃𝑧𝐴 0 ≤ 𝑧)
11082, 24syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ⊆ ℝ ∧ 𝑧𝐴) → -∞ < 𝑧)
111110a1d 25 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ⊆ ℝ ∧ 𝑧𝐴) → (0 ≤ 𝑧 → -∞ < 𝑧))
112111reximdva 3234 . . . . . . . . . . . . . . . . . 18 (𝐴 ⊆ ℝ → (∃𝑧𝐴 0 ≤ 𝑧 → ∃𝑧𝐴 -∞ < 𝑧))
113109, 112mpan9 507 . . . . . . . . . . . . . . . . 17 ((∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧𝐴 ⊆ ℝ) → ∃𝑧𝐴 -∞ < 𝑧)
114113, 36syl5ibr 247 . . . . . . . . . . . . . . . 16 (𝑦 = -∞ → ((∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧𝐴 ⊆ ℝ) → ∃𝑧𝐴 𝑦 < 𝑧))
115114a1dd 50 . . . . . . . . . . . . . . 15 (𝑦 = -∞ → ((∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧𝐴 ⊆ ℝ) → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧)))
116115expd 416 . . . . . . . . . . . . . 14 (𝑦 = -∞ → (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → (𝐴 ⊆ ℝ → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))))
11798, 104, 1163jaoi 1418 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞) → (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → (𝐴 ⊆ ℝ → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))))
11812, 117sylbi 218 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → (𝐴 ⊆ ℝ → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))))
119118com13 88 . . . . . . . . . . 11 (𝐴 ⊆ ℝ → (∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧 → (𝑦 ∈ ℝ* → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))))
120119imp 407 . . . . . . . . . 10 ((𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧) → (𝑦 ∈ ℝ* → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧)))
121120ralrimiv 3146 . . . . . . . . 9 ((𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧) → ∀𝑦 ∈ ℝ* (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))
12274, 121jca 512 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧) → (∀𝑦𝐴 ¬ +∞ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧)))
123 breq1 4959 . . . . . . . . . . . 12 (𝑥 = +∞ → (𝑥 < 𝑦 ↔ +∞ < 𝑦))
124123notbid 319 . . . . . . . . . . 11 (𝑥 = +∞ → (¬ 𝑥 < 𝑦 ↔ ¬ +∞ < 𝑦))
125124ralbidv 3162 . . . . . . . . . 10 (𝑥 = +∞ → (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ↔ ∀𝑦𝐴 ¬ +∞ < 𝑦))
126 breq2 4960 . . . . . . . . . . . 12 (𝑥 = +∞ → (𝑦 < 𝑥𝑦 < +∞))
127126imbi1d 343 . . . . . . . . . . 11 (𝑥 = +∞ → ((𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧)))
128127ralbidv 3162 . . . . . . . . . 10 (𝑥 = +∞ → (∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ* (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧)))
129125, 128anbi12d 630 . . . . . . . . 9 (𝑥 = +∞ → ((∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)) ↔ (∀𝑦𝐴 ¬ +∞ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))))
130129rspcev 3554 . . . . . . . 8 ((+∞ ∈ ℝ* ∧ (∀𝑦𝐴 ¬ +∞ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
13167, 122, 130sylancr 587 . . . . . . 7 ((𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ ℝ ∃𝑧𝐴 𝑥𝑧) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
13266, 131syldan 591 . . . . . 6 ((𝐴 ⊆ ℝ ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
133132adantlr 711 . . . . 5 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ ¬ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
13450, 133pm2.61dan 809 . . . 4 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
135 mnfxr 10534 . . . . . 6 -∞ ∈ ℝ*
136 ral0 4364 . . . . . . 7 𝑦 ∈ ∅ ¬ -∞ < 𝑦
137 nltmnf 12363 . . . . . . . . 9 (𝑦 ∈ ℝ* → ¬ 𝑦 < -∞)
138137pm2.21d 121 . . . . . . . 8 (𝑦 ∈ ℝ* → (𝑦 < -∞ → ∃𝑧 ∈ ∅ 𝑦 < 𝑧))
139138rgen 3113 . . . . . . 7 𝑦 ∈ ℝ* (𝑦 < -∞ → ∃𝑧 ∈ ∅ 𝑦 < 𝑧)
140136, 139pm3.2i 471 . . . . . 6 (∀𝑦 ∈ ∅ ¬ -∞ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < -∞ → ∃𝑧 ∈ ∅ 𝑦 < 𝑧))
141 breq1 4959 . . . . . . . . . 10 (𝑥 = -∞ → (𝑥 < 𝑦 ↔ -∞ < 𝑦))
142141notbid 319 . . . . . . . . 9 (𝑥 = -∞ → (¬ 𝑥 < 𝑦 ↔ ¬ -∞ < 𝑦))
143142ralbidv 3162 . . . . . . . 8 (𝑥 = -∞ → (∀𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ ∅ ¬ -∞ < 𝑦))
144 breq2 4960 . . . . . . . . . 10 (𝑥 = -∞ → (𝑦 < 𝑥𝑦 < -∞))
145144imbi1d 343 . . . . . . . . 9 (𝑥 = -∞ → ((𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧) ↔ (𝑦 < -∞ → ∃𝑧 ∈ ∅ 𝑦 < 𝑧)))
146145ralbidv 3162 . . . . . . . 8 (𝑥 = -∞ → (∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ* (𝑦 < -∞ → ∃𝑧 ∈ ∅ 𝑦 < 𝑧)))
147143, 146anbi12d 630 . . . . . . 7 (𝑥 = -∞ → ((∀𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ ∅ ¬ -∞ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < -∞ → ∃𝑧 ∈ ∅ 𝑦 < 𝑧))))
148147rspcev 3554 . . . . . 6 ((-∞ ∈ ℝ* ∧ (∀𝑦 ∈ ∅ ¬ -∞ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < -∞ → ∃𝑧 ∈ ∅ 𝑦 < 𝑧))) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧)))
149135, 140, 148mp2an 688 . . . . 5 𝑥 ∈ ℝ* (∀𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧))
150149a1i 11 . . . 4 (𝐴 ⊆ ℝ → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ ∅ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ ∅ 𝑦 < 𝑧)))
1516, 134, 150pm2.61ne 3068 . . 3 (𝐴 ⊆ ℝ → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
152151adantl 482 . 2 ((𝐴 ⊆ ℝ*𝐴 ⊆ ℝ) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
153 ssel 3878 . . . . . 6 (𝐴 ⊆ ℝ* → (𝑦𝐴𝑦 ∈ ℝ*))
154153, 70syl6 35 . . . . 5 (𝐴 ⊆ ℝ* → (𝑦𝐴 → ¬ +∞ < 𝑦))
155154ralrimiv 3146 . . . 4 (𝐴 ⊆ ℝ* → ∀𝑦𝐴 ¬ +∞ < 𝑦)
156 breq2 4960 . . . . . . 7 (𝑧 = +∞ → (𝑦 < 𝑧𝑦 < +∞))
157156rspcev 3554 . . . . . 6 ((+∞ ∈ 𝐴𝑦 < +∞) → ∃𝑧𝐴 𝑦 < 𝑧)
158157ex 413 . . . . 5 (+∞ ∈ 𝐴 → (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))
159158ralrimivw 3148 . . . 4 (+∞ ∈ 𝐴 → ∀𝑦 ∈ ℝ* (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧))
160155, 159anim12i 612 . . 3 ((𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴) → (∀𝑦𝐴 ¬ +∞ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < +∞ → ∃𝑧𝐴 𝑦 < 𝑧)))
16167, 160, 130sylancr 587 . 2 ((𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
162152, 161jaodan 950 1 ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842  w3o 1077  w3a 1078   = wceq 1520  wex 1759  wcel 2079  wne 2982  wral 3103  wrex 3104  wss 3854  c0 4206   class class class wbr 4956  (class class class)co 7007  cr 10371  0cc0 10372  1c1 10373   + caddc 10375  +∞cpnf 10507  -∞cmnf 10508  *cxr 10509   < clt 10510  cle 10511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-cnex 10428  ax-resscn 10429  ax-1cn 10430  ax-icn 10431  ax-addcl 10432  ax-addrcl 10433  ax-mulcl 10434  ax-mulrcl 10435  ax-mulcom 10436  ax-addass 10437  ax-mulass 10438  ax-distr 10439  ax-i2m1 10440  ax-1ne0 10441  ax-1rid 10442  ax-rnegex 10443  ax-rrecex 10444  ax-cnre 10445  ax-pre-lttri 10446  ax-pre-lttrn 10447  ax-pre-ltadd 10448  ax-pre-mulgt0 10449  ax-pre-sup 10450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-po 5354  df-so 5355  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-riota 6968  df-ov 7010  df-oprab 7011  df-mpo 7012  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-pnf 10512  df-mnf 10513  df-xr 10514  df-ltxr 10515  df-le 10516  df-sub 10708  df-neg 10709
This theorem is referenced by:  xrsupss  12541
  Copyright terms: Public domain W3C validator