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	⊢ ( ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) ∧ ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 ≤ 𝐷 ↔ ( 𝐹 ‘ 𝐶 ) ≤ ( 𝐹 ‘ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		leiso	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) → ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ≤ , ≤ ( 𝐴 , 𝐵 ) ) )
2	1	biimpcd	⊢ ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) → ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) → 𝐹 Isom ≤ , ≤ ( 𝐴 , 𝐵 ) ) )
3		isorel	⊢ ( ( 𝐹 Isom ≤ , ≤ ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 ≤ 𝐷 ↔ ( 𝐹 ‘ 𝐶 ) ≤ ( 𝐹 ‘ 𝐷 ) ) )
4	3	ex	⊢ ( 𝐹 Isom ≤ , ≤ ( 𝐴 , 𝐵 ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐶 ≤ 𝐷 ↔ ( 𝐹 ‘ 𝐶 ) ≤ ( 𝐹 ‘ 𝐷 ) ) ) )
5	2 4	syl6	⊢ ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) → ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐶 ≤ 𝐷 ↔ ( 𝐹 ‘ 𝐶 ) ≤ ( 𝐹 ‘ 𝐷 ) ) ) ) )
6	5	3imp	⊢ ( ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) ∧ ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 ≤ 𝐷 ↔ ( 𝐹 ‘ 𝐶 ) ≤ ( 𝐹 ‘ 𝐷 ) ) )