This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrinfmss2

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

		Ref	Expression
	Assertion	xrinfmss2	⊢ ( 𝐴 ⊆ ℝ^* → ∃ 𝑥 ∈ ℝ^* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ^◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑦 ^◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ^◡ < 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrinfmss	⊢ ( 𝐴 ⊆ ℝ^* → ∃ 𝑥 ∈ ℝ^* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	brcnv	⊢ ( 𝑥 ^◡ < 𝑦 ↔ 𝑦 < 𝑥 )
5	4	notbii	⊢ ( ¬ 𝑥 ^◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥 )
6	5	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ^◡ < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 )
7	3 2	brcnv	⊢ ( 𝑦 ^◡ < 𝑥 ↔ 𝑥 < 𝑦 )
8		vex	⊢ 𝑧 ∈ V
9	3 8	brcnv	⊢ ( 𝑦 ^◡ < 𝑧 ↔ 𝑧 < 𝑦 )
10	9	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐴 𝑦 ^◡ < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 )
11	7 10	imbi12i	⊢ ( ( 𝑦 ^◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ^◡ < 𝑧 ) ↔ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
12	11	ralbii	⊢ ( ∀ 𝑦 ∈ ℝ^* ( 𝑦 ^◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ^◡ < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ^* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
13	6 12	anbi12i	⊢ ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ^◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑦 ^◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ^◡ < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
14	13	rexbii	⊢ ( ∃ 𝑥 ∈ ℝ^* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ^◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑦 ^◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ^◡ < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ^* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
15	1 14	sylibr	⊢ ( 𝐴 ⊆ ℝ^* → ∃ 𝑥 ∈ ℝ^* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ^◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ^* ( 𝑦 ^◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ^◡ < 𝑧 ) ) )