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 ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )