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 ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) |