infxrpnf2

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

		Ref	Expression
	Assertion	infxrpnf2	$⊢ A \subseteq ℝ^{} \to inf (A ∖ \{+∞\} ℝ^{} <) = inf (A ℝ^{*} <)$

Step	Hyp	Ref	Expression
1		ssdifss	$⊢ A \subseteq ℝ^{} \to A ∖ \{+∞\} \subseteq ℝ^{}$
2		infxrpnf	$⊢ A ∖ \{+∞\} \subseteq ℝ^{} \to inf ((A ∖ \{+∞\}) \cup \{+∞\} ℝ^{} <) = inf (A ∖ \{+∞\} ℝ^{*} <)$
3	1 2	syl	$⊢ A \subseteq ℝ^{} \to inf ((A ∖ \{+∞\}) \cup \{+∞\} ℝ^{} <) = inf (A ∖ \{+∞\} ℝ^{*} <)$
4	3	adantr	$⊢ (A \subseteq ℝ^{} \land +∞ \in A) \to inf ((A ∖ \{+∞\}) \cup \{+∞\} ℝ^{} <) = inf (A ∖ \{+∞\} ℝ^{*} <)$
5		difsnid	$⊢ +∞ \in A \to (A ∖ \{+∞\}) \cup \{+∞\} = A$
6	5	infeq1d	$⊢ +∞ \in A \to inf ((A ∖ \{+∞\}) \cup \{+∞\} ℝ^{} <) = inf (A ℝ^{} <)$
7	6	adantl	$⊢ (A \subseteq ℝ^{} \land +∞ \in A) \to inf ((A ∖ \{+∞\}) \cup \{+∞\} ℝ^{} <) = inf (A ℝ^{*} <)$
8	4 7	eqtr3d	$⊢ (A \subseteq ℝ^{} \land +∞ \in A) \to inf (A ∖ \{+∞\} ℝ^{} <) = inf (A ℝ^{*} <)$
9		difsn	$⊢ \neg +∞ \in A \to A ∖ \{+∞\} = A$
10	9	infeq1d	$⊢ \neg +∞ \in A \to inf (A ∖ \{+∞\} ℝ^{} <) = inf (A ℝ^{} <)$
11	10	adantl	$⊢ (A \subseteq ℝ^{} \land \neg +∞ \in A) \to inf (A ∖ \{+∞\} ℝ^{} <) = inf (A ℝ^{*} <)$
12	8 11	pm2.61dan	$⊢ A \subseteq ℝ^{} \to inf (A ∖ \{+∞\} ℝ^{} <) = inf (A ℝ^{*} <)$

Metamath Proof Explorer