Metamath Proof Explorer

Theorem ovolfcl

Description: Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014)

		Ref	Expression
	Assertion	ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
2	1	elin2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ℝ × ℝ ) )
3		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑁 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ )
4	2 3	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ )
5	4 1	eqeltrrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
6		ancom	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ) ) ↔ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
7		elin	⊢ ( ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ↔ ( ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ≤ ∧ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ( ℝ × ℝ ) ) )
8		df-br	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ↔ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ≤ )
9	8	bicomi	⊢ ( ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ≤ ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) )
10		opelxp	⊢ ( ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ( ℝ × ℝ ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ) )
11	9 10	anbi12i	⊢ ( ( ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ≤ ∧ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ( ℝ × ℝ ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ) ) )
12	7 11	bitri	⊢ ( ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ) ) )
13		df-3an	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ↔ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
14	6 12 13	3bitr4i	⊢ ( ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
15	5 14	sylib	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )