Metamath Proof Explorer


Theorem xrinfmss

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

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

Proof

Step Hyp Ref Expression
1 xrinfmsslem ( ( 𝐴 ⊆ ℝ* ∧ ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
2 ssdifss ( 𝐴 ⊆ ℝ* → ( 𝐴 ∖ { +∞ } ) ⊆ ℝ* )
3 ssxr ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ* → ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) )
4 3orass ( ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ↔ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ ( +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) )
5 pnfex +∞ ∈ V
6 5 snid +∞ ∈ { +∞ }
7 elndif ( +∞ ∈ { +∞ } → ¬ +∞ ∈ ( 𝐴 ∖ { +∞ } ) )
8 biorf ( ¬ +∞ ∈ ( 𝐴 ∖ { +∞ } ) → ( -∞ ∈ ( 𝐴 ∖ { +∞ } ) ↔ ( +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) )
9 6 7 8 mp2b ( -∞ ∈ ( 𝐴 ∖ { +∞ } ) ↔ ( +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) )
10 9 orbi2i ( ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ↔ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ ( +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) )
11 4 10 bitr4i ( ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ↔ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) )
12 3 11 sylib ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ* → ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) )
13 xrinfmsslem ( ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ* ∧ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) )
14 2 12 13 syl2anc2 ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) )
15 xrinfmexpnf ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ) )
16 5 snss ( +∞ ∈ 𝐴 ↔ { +∞ } ⊆ 𝐴 )
17 undif ( { +∞ } ⊆ 𝐴 ↔ ( { +∞ } ∪ ( 𝐴 ∖ { +∞ } ) ) = 𝐴 )
18 uncom ( { +∞ } ∪ ( 𝐴 ∖ { +∞ } ) ) = ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } )
19 18 eqeq1i ( ( { +∞ } ∪ ( 𝐴 ∖ { +∞ } ) ) = 𝐴 ↔ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 )
20 17 19 bitri ( { +∞ } ⊆ 𝐴 ↔ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 )
21 16 20 bitri ( +∞ ∈ 𝐴 ↔ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 )
22 raleq ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ↔ ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ) )
23 rexeq ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ↔ ∃ 𝑧𝐴 𝑧 < 𝑦 ) )
24 23 imbi2d ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ↔ ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
25 24 ralbidv ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
26 22 25 anbi12d ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ) ↔ ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) ) )
27 21 26 sylbi ( +∞ ∈ 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ) ↔ ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) ) )
28 27 rexbidv ( +∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) ) )
29 15 28 syl5ib ( +∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) ) )
30 14 29 mpan9 ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
31 ssxr ( 𝐴 ⊆ ℝ* → ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) )
32 df-3or ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) )
33 or32 ( ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) )
34 32 33 bitri ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) )
35 31 34 sylib ( 𝐴 ⊆ ℝ* → ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) )
36 1 30 35 mpjaodan ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )