This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid ⊢ ( +∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
30 14 29 mpan9 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
31 ssxr ⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) )
32 df-3or ⊢ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) )
33 or32 ⊢ ( ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) )
34 32 33 bitri ⊢ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) )
35 31 34 sylib ⊢ ( 𝐴 ⊆ ℝ* → ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) )
36 1 30 35 mpjaodan ⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )