Metamath Proof Explorer

Theorem xrsupss

Description: Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005)

Ref Expression
Assertion xrsupss ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 xrsupsslem ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
2 ssdifss ⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* )
3 ssxr ⊢ ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* → ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) )
4 df-3or ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ↔ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) )
5 neldifsn ⊢ ¬ -∞ ∈ ( 𝐴 ∖ { -∞ } )
6 5 biorfi ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ↔ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) )
7 4 6 bitr4i ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ↔ ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) )
8 3 7 sylib ⊢ ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* → ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) )
9 xrsupsslem ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* ∧ ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∖ { -∞ } ) 𝑦 < 𝑧 ) ) )
10 2 8 9 syl2anc2 ⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∖ { -∞ } ) 𝑦 < 𝑧 ) ) )
11 xrsupexmnf ⊢ ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∖ { -∞ } ) 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) )
12 snssi ⊢ ( -∞ ∈ 𝐴 → { -∞ } ⊆ 𝐴 )
13 undif ⊢ ( { -∞ } ⊆ 𝐴 ↔ ( { -∞ } ∪ ( 𝐴 ∖ { -∞ } ) ) = 𝐴 )
14 uncom ⊢ ( { -∞ } ∪ ( 𝐴 ∖ { -∞ } ) ) = ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } )
15 14 eqeq1i ⊢ ( ( { -∞ } ∪ ( 𝐴 ∖ { -∞ } ) ) = 𝐴 ↔ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 )
16 13 15 bitri ⊢ ( { -∞ } ⊆ 𝐴 ↔ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 )
17 raleq ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ) )
18 rexeq ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
19 18 imbi2d ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ↔ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
20 19 ralbidv ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
21 17 20 anbi12d ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
22 16 21 sylbi ⊢ ( { -∞ } ⊆ 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
23 12 22 syl ⊢ ( -∞ ∈ 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
24 23 rexbidv ⊢ ( -∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
25 11 24 syl5ib ⊢ ( -∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∖ { -∞ } ) 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
26 10 25 mpan9 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
27 ssxr ⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) )
28 df-3or ⊢ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) )
29 27 28 sylib ⊢ ( 𝐴 ⊆ ℝ* → ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) )
30 1 26 29 mpjaodan ⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )