Metamath Proof Explorer

Theorem xrinfmss

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

Ref Expression
Assertion xrinfmss ⊢A⊆ℝ*→∃x∈ℝ*∀y∈A¬y<x∧∀y∈ℝ*x<y→∃z∈Az<y

Proof

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