supxrbnd2 - Metamath Proof Explorer

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

Theorem supxrbnd2 12111

Description: The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.)

**Assertion**
Ref	Expression
supxrbnd2	⊢ (𝐴 ⊆ ℝ^* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup(𝐴, ℝ^*, < ) < +∞))

Distinct variable group: 𝑥,𝑦,𝐴

**Proof of Theorem supxrbnd2**
Step	Hyp	Ref	Expression
1		ralnex 2988	. . . 4 ⊢ (∀𝑥 ∈ ℝ ¬ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
2		ssel2 3583	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ^*)
3		rexr 10045	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
4		xrlenlt 10063	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (𝑦 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑦))
5	4	con2bid 344	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
6	2, 3, 5	syl2an 494	. . . . . . . 8 ⊢ (((𝐴 ⊆ ℝ^* ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
7	6	an32s 845	. . . . . . 7 ⊢ (((𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
8	7	rexbidva 3044	. . . . . 6 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑥))
9		rexnal 2991	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑥 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
10	8, 9	syl6rbb 277	. . . . 5 ⊢ ((𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ) → (¬ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))
11	10	ralbidva 2981	. . . 4 ⊢ (𝐴 ⊆ ℝ^* → (∀𝑥 ∈ ℝ ¬ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))
12	1, 11	syl5bbr 274	. . 3 ⊢ (𝐴 ⊆ ℝ^* → (¬ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))
13		supxrunb2 12109	. . 3 ⊢ (𝐴 ⊆ ℝ^* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup(𝐴, ℝ^*, < ) = +∞))
14		supxrcl 12104	. . . 4 ⊢ (𝐴 ⊆ ℝ^* → sup(𝐴, ℝ^, < ) ∈ ℝ^)
15		nltpnft 11955	. . . 4 ⊢ (sup(𝐴, ℝ^, < ) ∈ ℝ^ → (sup(𝐴, ℝ^, < ) = +∞ ↔ ¬ sup(𝐴, ℝ^, < ) < +∞))
16	14, 15	syl 17	. . 3 ⊢ (𝐴 ⊆ ℝ^* → (sup(𝐴, ℝ^, < ) = +∞ ↔ ¬ sup(𝐴, ℝ^, < ) < +∞))
17	12, 13, 16	3bitrd 294	. 2 ⊢ (𝐴 ⊆ ℝ^* → (¬ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ¬ sup(𝐴, ℝ^*, < ) < +∞))
18	17	con4bid 307	1 ⊢ (𝐴 ⊆ ℝ^* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup(𝐴, ℝ^*, < ) < +∞))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1480 ∈ wcel 1987 ∀wral 2908 ∃wrex 2909 ⊆ wss 3560 class class class wbr 4623 supcsup 8306 ℝcr 9895 +∞cpnf 10031 ℝ^*cxr 10033 < clt 10034 ≤ cle 10035

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-sep 4751 ax-nul 4759 ax-pow 4813 ax-pr 4877 ax-un 6914 ax-cnex 9952 ax-resscn 9953 ax-1cn 9954 ax-icn 9955 ax-addcl 9956 ax-addrcl 9957 ax-mulcl 9958 ax-mulrcl 9959 ax-mulcom 9960 ax-addass 9961 ax-mulass 9962 ax-distr 9963 ax-i2m1 9964 ax-1ne0 9965 ax-1rid 9966 ax-rnegex 9967 ax-rrecex 9968 ax-cnre 9969 ax-pre-lttri 9970 ax-pre-lttrn 9971 ax-pre-ltadd 9972 ax-pre-mulgt0 9973 ax-pre-sup 9974

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2913 df-rex 2914 df-reu 2915 df-rmo 2916 df-rab 2917 df-v 3192 df-sbc 3423 df-csb 3520 df-dif 3563 df-un 3565 df-in 3567 df-ss 3574 df-nul 3898 df-if 4065 df-pw 4138 df-sn 4156 df-pr 4158 df-op 4162 df-uni 4410 df-br 4624 df-opab 4684 df-mpt 4685 df-id 4999 df-po 5005 df-so 5006 df-xp 5090 df-rel 5091 df-cnv 5092 df-co 5093 df-dm 5094 df-rn 5095 df-res 5096 df-ima 5097 df-iota 5820 df-fun 5859 df-fn 5860 df-f 5861 df-f1 5862 df-fo 5863 df-f1o 5864 df-fv 5865 df-riota 6576 df-ov 6618 df-oprab 6619 df-mpt2 6620 df-er 7702 df-en 7916 df-dom 7917 df-sdom 7918 df-sup 8308 df-pnf 10036 df-mnf 10037 df-xr 10038 df-ltxr 10039 df-le 10040 df-sub 10228 df-neg 10229

This theorem is referenced by: ovolunlem1 23205 supxrre3 39040

W3C validator