Theorem infxrpnf

Description: Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	infxrpnf	⊢ ( 𝐴 ⊆ ℝ* → inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) = inf ( 𝐴 , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ⊆ ℝ* → 𝐴 ⊆ ℝ* )
2		pnfxr	⊢ +∞ ∈ ℝ*
3		snssi	⊢ ( +∞ ∈ ℝ* → { +∞ } ⊆ ℝ* )
4	2 3	ax-mp	⊢ { +∞ } ⊆ ℝ*
5	4	a1i	⊢ ( 𝐴 ⊆ ℝ* → { +∞ } ⊆ ℝ* )
6	1 5	unssd	⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ∪ { +∞ } ) ⊆ ℝ* )
7	6	infxrcld	⊢ ( 𝐴 ⊆ ℝ* → inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) ∈ ℝ* )
8		infxrcl	⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
9		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ { +∞ } )
10	9	a1i	⊢ ( 𝐴 ⊆ ℝ* → 𝐴 ⊆ ( 𝐴 ∪ { +∞ } ) )
11		infxrss	⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ { +∞ } ) ∧ ( 𝐴 ∪ { +∞ } ) ⊆ ℝ* ) → inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) ≤ inf ( 𝐴 , ℝ* , < ) )
12	10 6 11	syl2anc	⊢ ( 𝐴 ⊆ ℝ* → inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) ≤ inf ( 𝐴 , ℝ* , < ) )
13		infeq1	⊢ ( 𝐴 = ∅ → inf ( 𝐴 , ℝ* , < ) = inf ( ∅ , ℝ* , < ) )
14		xrinf0	⊢ inf ( ∅ , ℝ* , < ) = +∞
15	14 2	eqeltri	⊢ inf ( ∅ , ℝ* , < ) ∈ ℝ*
16	15	a1i	⊢ ( 𝐴 = ∅ → inf ( ∅ , ℝ* , < ) ∈ ℝ* )
17	13 16	eqeltrd	⊢ ( 𝐴 = ∅ → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
18		xrltso	⊢ < Or ℝ*
19		infsn	⊢ ( ( < Or ℝ* ∧ +∞ ∈ ℝ* ) → inf ( { +∞ } , ℝ* , < ) = +∞ )
20	18 2 19	mp2an	⊢ inf ( { +∞ } , ℝ* , < ) = +∞
21	20	eqcomi	⊢ +∞ = inf ( { +∞ } , ℝ* , < )
22	21	a1i	⊢ ( 𝐴 = ∅ → +∞ = inf ( { +∞ } , ℝ* , < ) )
23	13 14	eqtrdi	⊢ ( 𝐴 = ∅ → inf ( 𝐴 , ℝ* , < ) = +∞ )
24		uneq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ∪ { +∞ } ) = ( ∅ ∪ { +∞ } ) )
25		0un	⊢ ( ∅ ∪ { +∞ } ) = { +∞ }
26	25	a1i	⊢ ( 𝐴 = ∅ → ( ∅ ∪ { +∞ } ) = { +∞ } )
27	24 26	eqtrd	⊢ ( 𝐴 = ∅ → ( 𝐴 ∪ { +∞ } ) = { +∞ } )
28	27	infeq1d	⊢ ( 𝐴 = ∅ → inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) = inf ( { +∞ } , ℝ* , < ) )
29	22 23 28	3eqtr4d	⊢ ( 𝐴 = ∅ → inf ( 𝐴 , ℝ* , < ) = inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) )
30	17 29	xreqled	⊢ ( 𝐴 = ∅ → inf ( 𝐴 , ℝ* , < ) ≤ inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) )
31	30	adantl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 = ∅ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) )
32		neqne	⊢ ( ¬ 𝐴 = ∅ → 𝐴 ≠ ∅ )
33		nfv	⊢ Ⅎ 𝑥 ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ )
34		nfv	⊢ Ⅎ 𝑦 ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ )
35		simpl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ ℝ* )
36	35 6	syl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ∪ { +∞ } ) ⊆ ℝ* )
37		simpr	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
38		ssel2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
39	38	xrleidd	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ 𝑥 )
40		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ 𝑥 ↔ 𝑥 ≤ 𝑥 ) )
41	40	rspcev	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
42	37 39 41	syl2anc	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
43	42	ad4ant14	⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∪ { +∞ } ) ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
44		simpll	⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∪ { +∞ } ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) )
45		elunnel1	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ { +∞ } ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ { +∞ } )
46		elsni	⊢ ( 𝑥 ∈ { +∞ } → 𝑥 = +∞ )
47	45 46	syl	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ { +∞ } ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑥 = +∞ )
48	47	adantll	⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∪ { +∞ } ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑥 = +∞ )
49		simplr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 = +∞ ) → 𝐴 ≠ ∅ )
50		ssel2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
51		pnfge	⊢ ( 𝑦 ∈ ℝ* → 𝑦 ≤ +∞ )
52	50 51	syl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ≤ +∞ )
53	52	adantlr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 = +∞ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ≤ +∞ )
54		simplr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 = +∞ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = +∞ )
55	53 54	breqtrrd	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 = +∞ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ≤ 𝑥 )
56	55	ralrimiva	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 = +∞ ) → ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
57	56	adantlr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 = +∞ ) → ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
58		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
59	49 57 58	syl2anc	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 = +∞ ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
60	44 48 59	syl2anc	⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∪ { +∞ } ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
61	43 60	pm2.61dan	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∪ { +∞ } ) ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
62	33 34 35 36 61	infleinf2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) )
63	32 62	sylan2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ¬ 𝐴 = ∅ ) → inf ( 𝐴 , ℝ* , < ) ≤ inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) )
64	31 63	pm2.61dan	⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ≤ inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) )
65	7 8 12 64	xrletrid	⊢ ( 𝐴 ⊆ ℝ* → inf ( ( 𝐴 ∪ { +∞ } ) , ℝ* , < ) = inf ( 𝐴 , ℝ* , < ) )