Metamath Proof Explorer

Theorem ovolfcl

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

Ref Expression
Assertion ovolfcl ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ N ∈ ℕ → 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ ∧ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N

Proof

Step Hyp Ref Expression
1 ffvelcdm ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ N ∈ ℕ → F ⁡ N ∈ ≤ ∩ ℝ 2
2 1 elin2d ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ N ∈ ℕ → F ⁡ N ∈ ℝ 2
3 1st2nd2 ⊢ F ⁡ N ∈ ℝ 2 → F ⁡ N = 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N
4 2 3 syl ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ N ∈ ℕ → F ⁡ N = 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N
5 4 1 eqeltrrd ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ N ∈ ℕ → 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ≤ ∩ ℝ 2
6 ancom ⊢ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N ∧ 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ ↔ 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ ∧ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N
7 elin ⊢ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ≤ ∩ ℝ 2 ↔ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ≤ ∧ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ℝ 2
8 df-br ⊢ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N ↔ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ≤
9 8 bicomi ⊢ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ≤ ↔ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N
10 opelxp ⊢ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ℝ 2 ↔ 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ
11 9 10 anbi12i ⊢ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ≤ ∧ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ℝ 2 ↔ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N ∧ 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ
12 7 11 bitri ⊢ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ≤ ∩ ℝ 2 ↔ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N ∧ 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ
13 df-3an ⊢ 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ ∧ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N ↔ 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ ∧ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N
14 6 12 13 3bitr4i ⊢ 1 st ⁡ F ⁡ N 2 nd ⁡ F ⁡ N ∈ ≤ ∩ ℝ 2 ↔ 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ ∧ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N
15 5 14 sylib ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ N ∈ ℕ → 1 st ⁡ F ⁡ N ∈ ℝ ∧ 2 nd ⁡ F ⁡ N ∈ ℝ ∧ 1 st ⁡ F ⁡ N ≤ 2 nd ⁡ F ⁡ N