Metamath Proof Explorer

Theorem supsr

Description: A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion supsr ⊢A≠∅∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z

Proof

Step Hyp Ref Expression
1 n0 ⊢A≠∅↔∃uu∈A
2 ltrelsr ⊢<𝑹⊆𝑹×𝑹
3 2 brel ⊢y<𝑹x→y∈𝑹∧x∈𝑹
4 3 simpld ⊢y<𝑹x→y∈𝑹
5 4 ralimi ⊢∀y∈Ay<𝑹x→∀y∈Ay∈𝑹
6 dfss3 ⊢A⊆𝑹↔∀y∈Ay∈𝑹
7 5 6 sylibr ⊢∀y∈Ay<𝑹x→A⊆𝑹
8 7 sseld ⊢∀y∈Ay<𝑹x→u∈A→u∈𝑹
9 8 rexlimivw ⊢∃x∈𝑹∀y∈Ay<𝑹x→u∈A→u∈𝑹
10 9 impcom ⊢u∈A∧∃x∈𝑹∀y∈Ay<𝑹x→u∈𝑹
11 eleq1 ⊢u=ifu∈𝑹u1𝑹→u∈A↔ifu∈𝑹u1𝑹∈A
12 11 anbi1d ⊢u=ifu∈𝑹u1𝑹→u∈A∧∃x∈𝑹∀y∈Ay<𝑹x↔ifu∈𝑹u1𝑹∈A∧∃x∈𝑹∀y∈Ay<𝑹x
13 12 imbi1d ⊢u=ifu∈𝑹u1𝑹→u∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z↔ifu∈𝑹u1𝑹∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
14 opeq1 ⊢v=w→v1𝑷=w1𝑷
15 14 eceq1d ⊢v=w→v1𝑷~𝑹=w1𝑷~𝑹
16 15 oveq2d ⊢v=w→ifu∈𝑹u1𝑹+𝑹v1𝑷~𝑹=ifu∈𝑹u1𝑹+𝑹w1𝑷~𝑹
17 16 eleq1d ⊢v=w→ifu∈𝑹u1𝑹+𝑹v1𝑷~𝑹∈A↔ifu∈𝑹u1𝑹+𝑹w1𝑷~𝑹∈A
18 17 cbvabv ⊢v|ifu∈𝑹u1𝑹+𝑹v1𝑷~𝑹∈A=w|ifu∈𝑹u1𝑹+𝑹w1𝑷~𝑹∈A
19 1sr ⊢1𝑹∈𝑹
20 19 elimel ⊢ifu∈𝑹u1𝑹∈𝑹
21 18 20 supsrlem ⊢ifu∈𝑹u1𝑹∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
22 13 21 dedth ⊢u∈𝑹→u∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
23 10 22 mpcom ⊢u∈A∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
24 23 ex ⊢u∈A→∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
25 24 exlimiv ⊢∃uu∈A→∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
26 1 25 sylbi ⊢A≠∅→∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z
27 26 imp ⊢A≠∅∧∃x∈𝑹∀y∈Ay<𝑹x→∃x∈𝑹∀y∈A¬x<𝑹y∧∀y∈𝑹y<𝑹x→∃z∈Ay<𝑹z