Theorem xrinfmss2

Description: Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014)

	Ref	Expression
Assertion	xrinfmss2	$$⊢A\subseteq {ℝ}^{*}\to \exists x\in {ℝ}^{*}\left(\forall y\in A\neg x{<}^{-1}y\wedge \forall y\in {ℝ}^{*}\left(y{<}^{-1}x\to \exists z\in Ay{<}^{-1}z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrinfmss	$$⊢A\subseteq {ℝ}^{*}\to \exists x\in {ℝ}^{*}\left(\forall y\in A\neg y<x\wedge \forall y\in {ℝ}^{*}\left(x<y\to \exists z\in Az<y\right)\right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	brcnv	$$⊢x{<}^{-1}y\leftrightarrow y<x$$
5	4	notbii	$$⊢\neg x{<}^{-1}y\leftrightarrow \neg y<x$$
6	5	ralbii	$$⊢\forall y\in A\neg x{<}^{-1}y\leftrightarrow \forall y\in A\neg y<x$$
7	3 2	brcnv	$$⊢y{<}^{-1}x\leftrightarrow x<y$$
8		vex	$$⊢z\in \mathrm{V}$$
9	3 8	brcnv	$$⊢y{<}^{-1}z\leftrightarrow z<y$$
10	9	rexbii	$$⊢\exists z\in Ay{<}^{-1}z\leftrightarrow \exists z\in Az<y$$
11	7 10	imbi12i	$$⊢\left(y{<}^{-1}x\to \exists z\in Ay{<}^{-1}z\right)\leftrightarrow \left(x<y\to \exists z\in Az<y\right)$$
12	11	ralbii	$$⊢\forall y\in {ℝ}^{*}\left(y{<}^{-1}x\to \exists z\in Ay{<}^{-1}z\right)\leftrightarrow \forall y\in {ℝ}^{*}\left(x<y\to \exists z\in Az<y\right)$$
13	6 12	anbi12i	$$⊢\left(\forall y\in A\neg x{<}^{-1}y\wedge \forall y\in {ℝ}^{*}\left(y{<}^{-1}x\to \exists z\in Ay{<}^{-1}z\right)\right)\leftrightarrow \left(\forall y\in A\neg y<x\wedge \forall y\in {ℝ}^{*}\left(x<y\to \exists z\in Az<y\right)\right)$$
14	13	rexbii	$$⊢\exists x\in {ℝ}^{*}\left(\forall y\in A\neg x{<}^{-1}y\wedge \forall y\in {ℝ}^{*}\left(y{<}^{-1}x\to \exists z\in Ay{<}^{-1}z\right)\right)\leftrightarrow \exists x\in {ℝ}^{*}\left(\forall y\in A\neg y<x\wedge \forall y\in {ℝ}^{*}\left(x<y\to \exists z\in Az<y\right)\right)$$
15	1 14	sylibr	$$⊢A\subseteq {ℝ}^{*}\to \exists x\in {ℝ}^{*}\left(\forall y\in A\neg x{<}^{-1}y\wedge \forall y\in {ℝ}^{*}\left(y{<}^{-1}x\to \exists z\in Ay{<}^{-1}z\right)\right)$$