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