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 𝐹 ) )