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

Metamath Proof Explorer

Theorem leisorel

Description: Version of isorel for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015) (Revised by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion leisorel ⊢ F Isom < , < A B ∧ A ⊆ ℝ * ∧ B ⊆ ℝ * ∧ C ∈ A ∧ D ∈ A → C ≤ D ↔ F ⁡ C ≤ F ⁡ D

Proof

Step Hyp Ref Expression
1 leiso ⊢ A ⊆ ℝ * ∧ B ⊆ ℝ * → F Isom < , < A B ↔ F Isom ≤ , ≤ A B
2 1 biimpcd ⊢ F Isom < , < A B → A ⊆ ℝ * ∧ B ⊆ ℝ * → F Isom ≤ , ≤ A B
3 isorel ⊢ F Isom ≤ , ≤ A B ∧ C ∈ A ∧ D ∈ A → C ≤ D ↔ F ⁡ C ≤ F ⁡ D
4 3 ex ⊢ F Isom ≤ , ≤ A B → C ∈ A ∧ D ∈ A → C ≤ D ↔ F ⁡ C ≤ F ⁡ D
5 2 4 syl6 ⊢ F Isom < , < A B → A ⊆ ℝ * ∧ B ⊆ ℝ * → C ∈ A ∧ D ∈ A → C ≤ D ↔ F ⁡ C ≤ F ⁡ D
6 5 3imp ⊢ F Isom < , < A B ∧ A ⊆ ℝ * ∧ B ⊆ ℝ * ∧ C ∈ A ∧ D ∈ A → C ≤ D ↔ F ⁡ C ≤ F ⁡ D