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

Metamath Proof Explorer

Theorem dvgt0lem2

Description: Lemma for dvgt0 and dvlt0 . (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses dvgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvgt0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
dvgt0lem.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ 𝑆 )
dvgt0lem.o ⊢ 𝑂 Or ℝ
dvgt0lem.i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) )
Assertion dvgt0lem2 ( 𝜑 → 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 dvgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dvgt0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
4 dvgt0lem.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ 𝑆 )
5 dvgt0lem.o ⊢ 𝑂 Or ℝ
6 dvgt0lem.i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) )
7 6 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) )
8 7 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) )
9 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
10 1 2 9 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
11 ltso ⊢ < Or ℝ
12 soss ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( < Or ℝ → < Or ( 𝐴 [,] 𝐵 ) ) )
13 10 11 12 mpisyl ⊢ ( 𝜑 → < Or ( 𝐴 [,] 𝐵 ) )
14 5 a1i ⊢ ( 𝜑 → 𝑂 Or ℝ )
15 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
16 3 15 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
17 ssidd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
18 soisores ⊢ ( ( ( < Or ( 𝐴 [,] 𝐵 ) ∧ 𝑂 Or ℝ ) ∧ ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) ) )
19 13 14 16 17 18 syl22anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐹 ‘ 𝑦 ) ) ) )
20 8 19 mpbird ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
21 ffn ⊢ ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ → 𝐹 Fn ( 𝐴 [,] 𝐵 ) )
22 3 15 21 3syl ⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 [,] 𝐵 ) )
23 fnresdm ⊢ ( 𝐹 Fn ( 𝐴 [,] 𝐵 ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) = 𝐹 )
24 isoeq1 ⊢ ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) = 𝐹 → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ↔ 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) )
25 22 23 24 3syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ↔ 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) )
26 20 25 mpbid ⊢ ( 𝜑 → 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
27 fnima ⊢ ( 𝐹 Fn ( 𝐴 [,] 𝐵 ) → ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) = ran 𝐹 )
28 isoeq5 ⊢ ( ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) = ran 𝐹 → ( 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ↔ 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )
29 22 27 28 3syl ⊢ ( 𝜑 → ( 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ↔ 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )
30 26 29 mpbid ⊢ ( 𝜑 → 𝐹 Isom < , 𝑂 ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) )