dvne0

Description: A function on a closed interval with nonzero derivative is either monotone increasing or monotone decreasing. (Contributed by Mario Carneiro, 19-Feb-2015)

	Ref	Expression
Hypotheses	dvne0.a	$⊢ φ \to A \in ℝ$
	dvne0.b	$⊢ φ \to B \in ℝ$
	dvne0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	dvne0.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	dvne0.z	$⊢ φ \to \neg 0 \in ran F_{ℝ}^{'}$
Assertion	dvne0	$⊢ φ \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))$

Proof

Step	Hyp	Ref	Expression
1		dvne0.a	$⊢ φ \to A \in ℝ$
2		dvne0.b	$⊢ φ \to B \in ℝ$
3		dvne0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
4		dvne0.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
5		dvne0.z	$⊢ φ \to \neg 0 \in ran F_{ℝ}^{'}$
6		eleq1	$⊢ x = 0 \to (x \in ran F_{ℝ}^{'} \leftrightarrow 0 \in ran F_{ℝ}^{'})$
7	6	notbid	$⊢ x = 0 \to (\neg x \in ran F_{ℝ}^{'} \leftrightarrow \neg 0 \in ran F_{ℝ}^{'})$
8	5 7	syl5ibrcom	$⊢ φ \to (x = 0 \to \neg x \in ran F_{ℝ}^{'})$
9	8	necon2ad	$⊢ φ \to (x \in ran F_{ℝ}^{'} \to x \neq 0)$
10	9	imp	$⊢ (φ \land x \in ran F_{ℝ}^{'}) \to x \neq 0$
11		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
12	3 11	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
13		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
14	1 2 13	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
15		dvfre	$⊢ (F : [A, B] ⟶ ℝ \land [A, B] \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
16	12 14 15	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
17	16	frnd	$⊢ φ \to ran F_{ℝ}^{'} \subseteq ℝ$
18	17	sselda	$⊢ (φ \land x \in ran F_{ℝ}^{'}) \to x \in ℝ$
19		0re	$⊢ 0 \in ℝ$
20		lttri2	$⊢ (x \in ℝ \land 0 \in ℝ) \to (x \neq 0 \leftrightarrow (x < 0 \lor 0 < x))$
21	18 19 20	sylancl	$⊢ (φ \land x \in ran F_{ℝ}^{'}) \to (x \neq 0 \leftrightarrow (x < 0 \lor 0 < x))$
22		0xr	$⊢ 0 \in ℝ^{*}$
23		elioomnf	$⊢ 0 \in ℝ^{*} \to (x \in (−∞, 0) \leftrightarrow (x \in ℝ \land x < 0))$
24	22 23	ax-mp	$⊢ x \in (−∞, 0) \leftrightarrow (x \in ℝ \land x < 0)$
25	24	baib	$⊢ x \in ℝ \to (x \in (−∞, 0) \leftrightarrow x < 0)$
26		elrp	$⊢ x \in ℝ^{+} \leftrightarrow (x \in ℝ \land 0 < x)$
27	26	baib	$⊢ x \in ℝ \to (x \in ℝ^{+} \leftrightarrow 0 < x)$
28	25 27	orbi12d	$⊢ x \in ℝ \to ((x \in (−∞, 0) \lor x \in ℝ^{+}) \leftrightarrow (x < 0 \lor 0 < x))$
29	18 28	syl	$⊢ (φ \land x \in ran F_{ℝ}^{'}) \to ((x \in (−∞, 0) \lor x \in ℝ^{+}) \leftrightarrow (x < 0 \lor 0 < x))$
30	21 29	bitr4d	$⊢ (φ \land x \in ran F_{ℝ}^{'}) \to (x \neq 0 \leftrightarrow (x \in (−∞, 0) \lor x \in ℝ^{+}))$
31	10 30	mpbid	$⊢ (φ \land x \in ran F_{ℝ}^{'}) \to (x \in (−∞, 0) \lor x \in ℝ^{+})$
32		elun	$⊢ x \in ((−∞, 0) \cup ℝ^{+}) \leftrightarrow (x \in (−∞, 0) \lor x \in ℝ^{+})$
33	31 32	sylibr	$⊢ (φ \land x \in ran F_{ℝ}^{'}) \to x \in ((−∞, 0) \cup ℝ^{+})$
34	33	ex	$⊢ φ \to (x \in ran F_{ℝ}^{'} \to x \in ((−∞, 0) \cup ℝ^{+}))$
35	34	ssrdv	$⊢ φ \to ran F_{ℝ}^{'} \subseteq (−∞, 0) \cup ℝ^{+}$
36		disjssun	$⊢ ran F_{ℝ}^{'} \cap (−∞, 0) = \emptyset \to (ran F_{ℝ}^{'} \subseteq (−∞, 0) \cup ℝ^{+} \leftrightarrow ran F_{ℝ}^{'} \subseteq ℝ^{+})$
37	35 36	syl5ibcom	$⊢ φ \to (ran F_{ℝ}^{'} \cap (−∞, 0) = \emptyset \to ran F_{ℝ}^{'} \subseteq ℝ^{+})$
38	37	imp	$⊢ (φ \land ran F_{ℝ}^{'} \cap (−∞, 0) = \emptyset) \to ran F_{ℝ}^{'} \subseteq ℝ^{+}$
39	1	adantr	$⊢ (φ \land ran F_{ℝ}^{'} \subseteq ℝ^{+}) \to A \in ℝ$
40	2	adantr	$⊢ (φ \land ran F_{ℝ}^{'} \subseteq ℝ^{+}) \to B \in ℝ$
41	3	adantr	$⊢ (φ \land ran F_{ℝ}^{'} \subseteq ℝ^{+}) \to F : [A, B] \underset{cn}{⟶} ℝ$
42	4	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℝ)$
43	16 42	mpbid	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℝ$
44	43	ffnd	$⊢ φ \to F_{ℝ}^{'} Fn (A, B)$
45	44	anim1i	$⊢ (φ \land ran F_{ℝ}^{'} \subseteq ℝ^{+}) \to (F_{ℝ}^{'} Fn (A, B) \land ran F_{ℝ}^{'} \subseteq ℝ^{+})$
46		df-f	$⊢ F_{ℝ}^{'} : (A, B) ⟶ ℝ^{+} \leftrightarrow (F_{ℝ}^{'} Fn (A, B) \land ran F_{ℝ}^{'} \subseteq ℝ^{+})$
47	45 46	sylibr	$⊢ (φ \land ran F_{ℝ}^{'} \subseteq ℝ^{+}) \to F_{ℝ}^{'} : (A, B) ⟶ ℝ^{+}$
48	39 40 41 47	dvgt0	$⊢ (φ \land ran F_{ℝ}^{'} \subseteq ℝ^{+}) \to F {Isom}_{<, <} ([A, B], ran F)$
49	48	orcd	$⊢ (φ \land ran F_{ℝ}^{'} \subseteq ℝ^{+}) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))$
50	38 49	syldan	$⊢ (φ \land ran F_{ℝ}^{'} \cap (−∞, 0) = \emptyset) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))$
51		n0	$⊢ ran F_{ℝ}^{'} \cap (−∞, 0) \neq \emptyset \leftrightarrow \exists x x \in (ran F_{ℝ}^{'} \cap (−∞, 0))$
52		elin	$⊢ x \in (ran F_{ℝ}^{'} \cap (−∞, 0)) \leftrightarrow (x \in ran F_{ℝ}^{'} \land x \in (−∞, 0))$
53		fvelrnb	$⊢ F_{ℝ}^{'} Fn (A, B) \to (x \in ran F_{ℝ}^{'} \leftrightarrow \exists y \in (A, B) F_{ℝ}^{'} (y) = x)$
54	44 53	syl	$⊢ φ \to (x \in ran F_{ℝ}^{'} \leftrightarrow \exists y \in (A, B) F_{ℝ}^{'} (y) = x)$
55	1	adantr	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to A \in ℝ$
56	2	adantr	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to B \in ℝ$
57	3	adantr	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to F : [A, B] \underset{cn}{⟶} ℝ$
58	44	adantr	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to F_{ℝ}^{'} Fn (A, B)$
59	43	adantr	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to F_{ℝ}^{'} : (A, B) ⟶ ℝ$
60	59	ffvelrnda	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land z \in (A, B)) \to F_{ℝ}^{'} (z) \in ℝ$
61	5	ad2antrr	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land z \in (A, B)) \to \neg 0 \in ran F_{ℝ}^{'}$
62		simplrl	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to y \in (A, B)$
63		simprl	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to z \in (A, B)$
64		ioossicc	$⊢ (A, B) \subseteq [A, B]$
65		rescncf	$⊢ (A, B) \subseteq [A, B] \to (F : [A, B] \underset{cn}{⟶} ℝ \to ({F ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℝ)$
66	64 3 65	mpsyl	$⊢ φ \to ({F ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℝ$
67	66	ad2antrr	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to ({F ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℝ$
68		ax-resscn	$⊢ ℝ \subseteq ℂ$
69	68	a1i	$⊢ φ \to ℝ \subseteq ℂ$
70		fss	$⊢ (F : [A, B] ⟶ ℝ \land ℝ \subseteq ℂ) \to F : [A, B] ⟶ ℂ$
71	12 68 70	sylancl	$⊢ φ \to F : [A, B] ⟶ ℂ$
72	64 14	sstrid	$⊢ φ \to (A, B) \subseteq ℝ$
73		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
74	73	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
75	73 74	dvres	$⊢ ((ℝ \subseteq ℂ \land F : [A, B] ⟶ ℂ) \land ([A, B] \subseteq ℝ \land (A, B) \subseteq ℝ)) \to ℝ D ({F ↾}_{(A, B)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((A, B))}$
76	69 71 14 72 75	syl22anc	$⊢ φ \to ℝ D ({F ↾}_{(A, B)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((A, B))}$
77		retop	$⊢ topGen (ran (.)) \in Top$
78		iooretop	$⊢ (A, B) \in topGen (ran (.))$
79		isopn3i	$⊢ (topGen (ran (.)) \in Top \land (A, B) \in topGen (ran (.))) \to int (topGen (ran (.))) ((A, B)) = (A, B)$
80	77 78 79	mp2an	$⊢ int (topGen (ran (.))) ((A, B)) = (A, B)$
81	80	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((A, B))} = {F_{ℝ}^{'} ↾}_{(A, B)}$
82		fnresdm	$⊢ F_{ℝ}^{'} Fn (A, B) \to {F_{ℝ}^{'} ↾}_{(A, B)} = ℝ D F$
83	44 82	syl	$⊢ φ \to {F_{ℝ}^{'} ↾}_{(A, B)} = ℝ D F$
84	81 83	syl5eq	$⊢ φ \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((A, B))} = ℝ D F$
85	76 84	eqtrd	$⊢ φ \to ℝ D ({F ↾}_{(A, B)}) = ℝ D F$
86	85	dmeqd	$⊢ φ \to dom {({F ↾}_{(A, B)})}_{ℝ}^{'} = dom F_{ℝ}^{'}$
87	86 4	eqtrd	$⊢ φ \to dom {({F ↾}_{(A, B)})}_{ℝ}^{'} = (A, B)$
88	87	ad2antrr	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to dom {({F ↾}_{(A, B)})}_{ℝ}^{'} = (A, B)$
89	62 63 67 88	dvivth	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to [{({F ↾}_{(A, B)})}_{ℝ}^{'} (y), {({F ↾}_{(A, B)})}_{ℝ}^{'} (z)] \subseteq ran {({F ↾}_{(A, B)})}_{ℝ}^{'}$
90	85	ad2antrr	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to ℝ D ({F ↾}_{(A, B)}) = ℝ D F$
91	90	fveq1d	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to {({F ↾}_{(A, B)})}_{ℝ}^{'} (y) = F_{ℝ}^{'} (y)$
92	90	fveq1d	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to {({F ↾}_{(A, B)})}_{ℝ}^{'} (z) = F_{ℝ}^{'} (z)$
93	91 92	oveq12d	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to [{({F ↾}_{(A, B)})}_{ℝ}^{'} (y), {({F ↾}_{(A, B)})}_{ℝ}^{'} (z)] = [F_{ℝ}^{'} (y), F_{ℝ}^{'} (z)]$
94	90	rneqd	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to ran {({F ↾}_{(A, B)})}_{ℝ}^{'} = ran F_{ℝ}^{'}$
95	89 93 94	3sstr3d	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to [F_{ℝ}^{'} (y), F_{ℝ}^{'} (z)] \subseteq ran F_{ℝ}^{'}$
96	19	a1i	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to 0 \in ℝ$
97		simplrr	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to F_{ℝ}^{'} (y) \in (−∞, 0)$
98		elioomnf	$⊢ 0 \in ℝ^{*} \to (F_{ℝ}^{'} (y) \in (−∞, 0) \leftrightarrow (F_{ℝ}^{'} (y) \in ℝ \land F_{ℝ}^{'} (y) < 0))$
99	22 98	ax-mp	$⊢ F_{ℝ}^{'} (y) \in (−∞, 0) \leftrightarrow (F_{ℝ}^{'} (y) \in ℝ \land F_{ℝ}^{'} (y) < 0)$
100	97 99	sylib	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to (F_{ℝ}^{'} (y) \in ℝ \land F_{ℝ}^{'} (y) < 0)$
101	100	simprd	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to F_{ℝ}^{'} (y) < 0$
102	100	simpld	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to F_{ℝ}^{'} (y) \in ℝ$
103		ltle	$⊢ (F_{ℝ}^{'} (y) \in ℝ \land 0 \in ℝ) \to (F_{ℝ}^{'} (y) < 0 \to F_{ℝ}^{'} (y) \leq 0)$
104	102 19 103	sylancl	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to (F_{ℝ}^{'} (y) < 0 \to F_{ℝ}^{'} (y) \leq 0)$
105	101 104	mpd	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to F_{ℝ}^{'} (y) \leq 0$
106		simprr	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to 0 \leq F_{ℝ}^{'} (z)$
107	63 60	syldan	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to F_{ℝ}^{'} (z) \in ℝ$
108		elicc2	$⊢ (F_{ℝ}^{'} (y) \in ℝ \land F_{ℝ}^{'} (z) \in ℝ) \to (0 \in [F_{ℝ}^{'} (y), F_{ℝ}^{'} (z)] \leftrightarrow (0 \in ℝ \land F_{ℝ}^{'} (y) \leq 0 \land 0 \leq F_{ℝ}^{'} (z)))$
109	102 107 108	syl2anc	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to (0 \in [F_{ℝ}^{'} (y), F_{ℝ}^{'} (z)] \leftrightarrow (0 \in ℝ \land F_{ℝ}^{'} (y) \leq 0 \land 0 \leq F_{ℝ}^{'} (z)))$
110	96 105 106 109	mpbir3and	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to 0 \in [F_{ℝ}^{'} (y), F_{ℝ}^{'} (z)]$
111	95 110	sseldd	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land (z \in (A, B) \land 0 \leq F_{ℝ}^{'} (z))) \to 0 \in ran F_{ℝ}^{'}$
112	111	expr	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land z \in (A, B)) \to (0 \leq F_{ℝ}^{'} (z) \to 0 \in ran F_{ℝ}^{'})$
113	61 112	mtod	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land z \in (A, B)) \to \neg 0 \leq F_{ℝ}^{'} (z)$
114		ltnle	$⊢ (F_{ℝ}^{'} (z) \in ℝ \land 0 \in ℝ) \to (F_{ℝ}^{'} (z) < 0 \leftrightarrow \neg 0 \leq F_{ℝ}^{'} (z))$
115	60 19 114	sylancl	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land z \in (A, B)) \to (F_{ℝ}^{'} (z) < 0 \leftrightarrow \neg 0 \leq F_{ℝ}^{'} (z))$
116	113 115	mpbird	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land z \in (A, B)) \to F_{ℝ}^{'} (z) < 0$
117		elioomnf	$⊢ 0 \in ℝ^{*} \to (F_{ℝ}^{'} (z) \in (−∞, 0) \leftrightarrow (F_{ℝ}^{'} (z) \in ℝ \land F_{ℝ}^{'} (z) < 0))$
118	22 117	ax-mp	$⊢ F_{ℝ}^{'} (z) \in (−∞, 0) \leftrightarrow (F_{ℝ}^{'} (z) \in ℝ \land F_{ℝ}^{'} (z) < 0)$
119	60 116 118	sylanbrc	$⊢ ((φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \land z \in (A, B)) \to F_{ℝ}^{'} (z) \in (−∞, 0)$
120	119	ralrimiva	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to \forall z \in (A, B) F_{ℝ}^{'} (z) \in (−∞, 0)$
121		ffnfv	$⊢ F_{ℝ}^{'} : (A, B) ⟶ (−∞, 0) \leftrightarrow (F_{ℝ}^{'} Fn (A, B) \land \forall z \in (A, B) F_{ℝ}^{'} (z) \in (−∞, 0))$
122	58 120 121	sylanbrc	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to F_{ℝ}^{'} : (A, B) ⟶ (−∞, 0)$
123	55 56 57 122	dvlt0	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to F {Isom}_{<, <^{-1}} ([A, B], ran F)$
124	123	olcd	$⊢ (φ \land (y \in (A, B) \land F_{ℝ}^{'} (y) \in (−∞, 0))) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))$
125	124	expr	$⊢ (φ \land y \in (A, B)) \to (F_{ℝ}^{'} (y) \in (−∞, 0) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F)))$
126		eleq1	$⊢ F_{ℝ}^{'} (y) = x \to (F_{ℝ}^{'} (y) \in (−∞, 0) \leftrightarrow x \in (−∞, 0))$
127	126	imbi1d	$⊢ F_{ℝ}^{'} (y) = x \to ((F_{ℝ}^{'} (y) \in (−∞, 0) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))) \leftrightarrow (x \in (−∞, 0) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))))$
128	125 127	syl5ibcom	$⊢ (φ \land y \in (A, B)) \to (F_{ℝ}^{'} (y) = x \to (x \in (−∞, 0) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))))$
129	128	rexlimdva	$⊢ φ \to (\exists y \in (A, B) F_{ℝ}^{'} (y) = x \to (x \in (−∞, 0) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))))$
130	54 129	sylbid	$⊢ φ \to (x \in ran F_{ℝ}^{'} \to (x \in (−∞, 0) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))))$
131	130	impd	$⊢ φ \to ((x \in ran F_{ℝ}^{'} \land x \in (−∞, 0)) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F)))$
132	52 131	syl5bi	$⊢ φ \to (x \in (ran F_{ℝ}^{'} \cap (−∞, 0)) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F)))$
133	132	exlimdv	$⊢ φ \to (\exists x x \in (ran F_{ℝ}^{'} \cap (−∞, 0)) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F)))$
134	51 133	syl5bi	$⊢ φ \to (ran F_{ℝ}^{'} \cap (−∞, 0) \neq \emptyset \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F)))$
135	134	imp	$⊢ (φ \land ran F_{ℝ}^{'} \cap (−∞, 0) \neq \emptyset) \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))$
136	50 135	pm2.61dane	$⊢ φ \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))$

Metamath Proof Explorer

Theorem dvne0

Proof