dvgt0lem2

	Ref	Expression
Hypotheses	dvgt0.a	$⊢ φ \to A \in ℝ$
	dvgt0.b	$⊢ φ \to B \in ℝ$
	dvgt0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	dvgt0lem.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ S$
	dvgt0lem.o	$⊢ O Or ℝ$
	dvgt0lem.i	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (x) O F (y)$
Assertion	dvgt0lem2	$⊢ φ \to F {Isom}_{<, O} ([A, B], ran F)$

Proof

Step	Hyp	Ref	Expression
1		dvgt0.a	$⊢ φ \to A \in ℝ$
2		dvgt0.b	$⊢ φ \to B \in ℝ$
3		dvgt0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
4		dvgt0lem.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ S$
5		dvgt0lem.o	$⊢ O Or ℝ$
6		dvgt0lem.i	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (x) O F (y)$
7	6	ex	$⊢ (φ \land (x \in [A, B] \land y \in [A, B])) \to (x < y \to F (x) O F (y))$
8	7	ralrimivva	$⊢ φ \to \forall x \in [A, B] \forall y \in [A, B] (x < y \to F (x) O F (y))$
9		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
10	1 2 9	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
11		ltso	$⊢ < Or ℝ$
12		soss	$⊢ [A, B] \subseteq ℝ \to (< Or ℝ \to < Or [A, B])$
13	10 11 12	mpisyl	$⊢ φ \to < Or [A, B]$
14	5	a1i	$⊢ φ \to O Or ℝ$
15		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
16	3 15	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
17		ssidd	$⊢ φ \to [A, B] \subseteq [A, B]$
18		soisores	$⊢ ((< Or [A, B] \land O Or ℝ) \land (F : [A, B] ⟶ ℝ \land [A, B] \subseteq [A, B])) \to (({F ↾}_{[A, B]}) {Isom}_{<, O} ([A, B], F [[A, B]]) \leftrightarrow \forall x \in [A, B] \forall y \in [A, B] (x < y \to F (x) O F (y)))$
19	13 14 16 17 18	syl22anc	$⊢ φ \to (({F ↾}_{[A, B]}) {Isom}_{<, O} ([A, B], F [[A, B]]) \leftrightarrow \forall x \in [A, B] \forall y \in [A, B] (x < y \to F (x) O F (y)))$
20	8 19	mpbird	$⊢ φ \to ({F ↾}_{[A, B]}) {Isom}_{<, O} ([A, B], F [[A, B]])$
21		ffn	$⊢ F : [A, B] ⟶ ℝ \to F Fn [A, B]$
22	3 15 21	3syl	$⊢ φ \to F Fn [A, B]$
23		fnresdm	$⊢ F Fn [A, B] \to {F ↾}_{[A, B]} = F$
24		isoeq1	$⊢ {F ↾}_{[A, B]} = F \to (({F ↾}_{[A, B]}) {Isom}_{<, O} ([A, B], F [[A, B]]) \leftrightarrow F {Isom}_{<, O} ([A, B], F [[A, B]]))$
25	22 23 24	3syl	$⊢ φ \to (({F ↾}_{[A, B]}) {Isom}_{<, O} ([A, B], F [[A, B]]) \leftrightarrow F {Isom}_{<, O} ([A, B], F [[A, B]]))$
26	20 25	mpbid	$⊢ φ \to F {Isom}_{<, O} ([A, B], F [[A, B]])$
27		fnima	$⊢ F Fn [A, B] \to F [[A, B]] = ran F$
28		isoeq5	$⊢ F [[A, B]] = ran F \to (F {Isom}_{<, O} ([A, B], F [[A, B]]) \leftrightarrow F {Isom}_{<, O} ([A, B], ran F))$
29	22 27 28	3syl	$⊢ φ \to (F {Isom}_{<, O} ([A, B], F [[A, B]]) \leftrightarrow F {Isom}_{<, O} ([A, B], ran F))$
30	26 29	mpbid	$⊢ φ \to F {Isom}_{<, O} ([A, B], ran F)$

Metamath Proof Explorer

Theorem dvgt0lem2

Proof