Metamath Proof Explorer


Theorem ovolfcl

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

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

Proof

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