dvcnvrelem1

	Ref	Expression
Hypotheses	dvcnvre.f	$⊢ φ \to F : X \underset{cn}{⟶} ℝ$
	dvcnvre.d	$⊢ φ \to dom F_{ℝ}^{'} = X$
	dvcnvre.z	$⊢ φ \to \neg 0 \in ran F_{ℝ}^{'}$
	dvcnvre.1	$⊢ φ \to F : X \underset{1-1 onto}{⟶} Y$
	dvcnvre.c	$⊢ φ \to C \in X$
	dvcnvre.r	$⊢ φ \to R \in ℝ^{+}$
	dvcnvre.s	$⊢ φ \to [C - R, C + R] \subseteq X$
Assertion	dvcnvrelem1	$⊢ φ \to F (C) \in int (topGen (ran (.))) (F [[C - R, C + R]])$

Proof

Step	Hyp	Ref	Expression
1		dvcnvre.f	$⊢ φ \to F : X \underset{cn}{⟶} ℝ$
2		dvcnvre.d	$⊢ φ \to dom F_{ℝ}^{'} = X$
3		dvcnvre.z	$⊢ φ \to \neg 0 \in ran F_{ℝ}^{'}$
4		dvcnvre.1	$⊢ φ \to F : X \underset{1-1 onto}{⟶} Y$
5		dvcnvre.c	$⊢ φ \to C \in X$
6		dvcnvre.r	$⊢ φ \to R \in ℝ^{+}$
7		dvcnvre.s	$⊢ φ \to [C - R, C + R] \subseteq X$
8		dvbsss	$⊢ dom F_{ℝ}^{'} \subseteq ℝ$
9	2 8	eqsstrrdi	$⊢ φ \to X \subseteq ℝ$
10	9 5	sseldd	$⊢ φ \to C \in ℝ$
11	6	rpred	$⊢ φ \to R \in ℝ$
12	10 11	resubcld	$⊢ φ \to C - R \in ℝ$
13	10 11	readdcld	$⊢ φ \to C + R \in ℝ$
14	10 6	ltsubrpd	$⊢ φ \to C - R < C$
15	10 6	ltaddrpd	$⊢ φ \to C < C + R$
16	12 10 13 14 15	lttrd	$⊢ φ \to C - R < C + R$
17	12 13 16	ltled	$⊢ φ \to C - R \leq C + R$
18		rescncf	$⊢ [C - R, C + R] \subseteq X \to (F : X \underset{cn}{⟶} ℝ \to ({F ↾}_{[C - R, C + R]}) : [C - R, C + R] \underset{cn}{⟶} ℝ)$
19	7 1 18	sylc	$⊢ φ \to ({F ↾}_{[C - R, C + R]}) : [C - R, C + R] \underset{cn}{⟶} ℝ$
20	12 13 17 19	evthicc2	$⊢ φ \to \exists x \in ℝ \exists y \in ℝ ran ({F ↾}_{[C - R, C + R]}) = [x, y]$
21		cncff	$⊢ F : X \underset{cn}{⟶} ℝ \to F : X ⟶ ℝ$
22	1 21	syl	$⊢ φ \to F : X ⟶ ℝ$
23	22 5	ffvelcdmd	$⊢ φ \to F (C) \in ℝ$
24	23	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C) \in ℝ$
25	12	rexrd	$⊢ φ \to C - R \in ℝ^{*}$
26	13	rexrd	$⊢ φ \to C + R \in ℝ^{*}$
27		lbicc2	$⊢ (C - R \in ℝ^{} \land C + R \in ℝ^{} \land C - R \leq C + R) \to C - R \in [C - R, C + R]$
28	25 26 17 27	syl3anc	$⊢ φ \to C - R \in [C - R, C + R]$
29	28	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to C - R \in [C - R, C + R]$
30	12 10 14	ltled	$⊢ φ \to C - R \leq C$
31	10 13 15	ltled	$⊢ φ \to C \leq C + R$
32		elicc2	$⊢ (C - R \in ℝ \land C + R \in ℝ) \to (C \in [C - R, C + R] \leftrightarrow (C \in ℝ \land C - R \leq C \land C \leq C + R))$
33	12 13 32	syl2anc	$⊢ φ \to (C \in [C - R, C + R] \leftrightarrow (C \in ℝ \land C - R \leq C \land C \leq C + R))$
34	10 30 31 33	mpbir3and	$⊢ φ \to C \in [C - R, C + R]$
35	34	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to C \in [C - R, C + R]$
36	14	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to C - R < C$
37		isorel	$⊢ (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \land (C - R \in [C - R, C + R] \land C \in [C - R, C + R])) \to (C - R < C \leftrightarrow ({F ↾}_{[C - R, C + R]}) (C - R) < ({F ↾}_{[C - R, C + R]}) (C))$
38	37	biimpd	$⊢ (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \land (C - R \in [C - R, C + R] \land C \in [C - R, C + R])) \to (C - R < C \to ({F ↾}_{[C - R, C + R]}) (C - R) < ({F ↾}_{[C - R, C + R]}) (C))$
39	38	exp32	$⊢ ({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to (C - R \in [C - R, C + R] \to (C \in [C - R, C + R] \to (C - R < C \to ({F ↾}_{[C - R, C + R]}) (C - R) < ({F ↾}_{[C - R, C + R]}) (C))))$
40	39	com4l	$⊢ C - R \in [C - R, C + R] \to (C \in [C - R, C + R] \to (C - R < C \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to ({F ↾}_{[C - R, C + R]}) (C - R) < ({F ↾}_{[C - R, C + R]}) (C))))$
41	29 35 36 40	syl3c	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to ({F ↾}_{[C - R, C + R]}) (C - R) < ({F ↾}_{[C - R, C + R]}) (C))$
42	29	fvresd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to ({F ↾}_{[C - R, C + R]}) (C - R) = F (C - R)$
43	35	fvresd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to ({F ↾}_{[C - R, C + R]}) (C) = F (C)$
44	42 43	breq12d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) (C - R) < ({F ↾}_{[C - R, C + R]}) (C) \leftrightarrow F (C - R) < F (C))$
45	41 44	sylibd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to F (C - R) < F (C))$
46	22	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F : X ⟶ ℝ$
47	46	ffund	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to Fun F$
48	7	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to [C - R, C + R] \subseteq X$
49	46	fdmd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to dom F = X$
50	48 49	sseqtrrd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to [C - R, C + R] \subseteq dom F$
51		funfvima2	$⊢ (Fun F \land [C - R, C + R] \subseteq dom F) \to (C - R \in [C - R, C + R] \to F (C - R) \in F [[C - R, C + R]])$
52	47 50 51	syl2anc	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (C - R \in [C - R, C + R] \to F (C - R) \in F [[C - R, C + R]])$
53	29 52	mpd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C - R) \in F [[C - R, C + R]]$
54		df-ima	$⊢ F [[C - R, C + R]] = ran ({F ↾}_{[C - R, C + R]})$
55		simprr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to ran ({F ↾}_{[C - R, C + R]}) = [x, y]$
56	54 55	eqtrid	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F [[C - R, C + R]] = [x, y]$
57	53 56	eleqtrd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C - R) \in [x, y]$
58		elicc2	$⊢ (x \in ℝ \land y \in ℝ) \to (F (C - R) \in [x, y] \leftrightarrow (F (C - R) \in ℝ \land x \leq F (C - R) \land F (C - R) \leq y))$
59	58	ad2antrl	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C - R) \in [x, y] \leftrightarrow (F (C - R) \in ℝ \land x \leq F (C - R) \land F (C - R) \leq y))$
60	57 59	mpbid	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C - R) \in ℝ \land x \leq F (C - R) \land F (C - R) \leq y)$
61	60	simp2d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to x \leq F (C - R)$
62		simprll	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to x \in ℝ$
63	7 28	sseldd	$⊢ φ \to C - R \in X$
64	22 63	ffvelcdmd	$⊢ φ \to F (C - R) \in ℝ$
65	64	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C - R) \in ℝ$
66		lelttr	$⊢ (x \in ℝ \land F (C - R) \in ℝ \land F (C) \in ℝ) \to ((x \leq F (C - R) \land F (C - R) < F (C)) \to x < F (C))$
67	62 65 24 66	syl3anc	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to ((x \leq F (C - R) \land F (C - R) < F (C)) \to x < F (C))$
68	61 67	mpand	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C - R) < F (C) \to x < F (C))$
69	45 68	syld	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to x < F (C))$
70		ubicc2	$⊢ (C - R \in ℝ^{} \land C + R \in ℝ^{} \land C - R \leq C + R) \to C + R \in [C - R, C + R]$
71	25 26 17 70	syl3anc	$⊢ φ \to C + R \in [C - R, C + R]$
72	71	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to C + R \in [C - R, C + R]$
73	15	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to C < C + R$
74		isorel	$⊢ (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \land (C \in [C - R, C + R] \land C + R \in [C - R, C + R])) \to (C < C + R \leftrightarrow ({F ↾}_{[C - R, C + R]}) (C) <^{-1} ({F ↾}_{[C - R, C + R]}) (C + R))$
75	74	biimpd	$⊢ (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \land (C \in [C - R, C + R] \land C + R \in [C - R, C + R])) \to (C < C + R \to ({F ↾}_{[C - R, C + R]}) (C) <^{-1} ({F ↾}_{[C - R, C + R]}) (C + R))$
76	75	exp32	$⊢ ({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to (C \in [C - R, C + R] \to (C + R \in [C - R, C + R] \to (C < C + R \to ({F ↾}_{[C - R, C + R]}) (C) <^{-1} ({F ↾}_{[C - R, C + R]}) (C + R))))$
77	76	com4l	$⊢ C \in [C - R, C + R] \to (C + R \in [C - R, C + R] \to (C < C + R \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to ({F ↾}_{[C - R, C + R]}) (C) <^{-1} ({F ↾}_{[C - R, C + R]}) (C + R))))$
78	35 72 73 77	syl3c	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to ({F ↾}_{[C - R, C + R]}) (C) <^{-1} ({F ↾}_{[C - R, C + R]}) (C + R))$
79		fvex	$⊢ ({F ↾}_{[C - R, C + R]}) (C) \in V$
80		fvex	$⊢ ({F ↾}_{[C - R, C + R]}) (C + R) \in V$
81	79 80	brcnv	$⊢ ({F ↾}_{[C - R, C + R]}) (C) <^{-1} ({F ↾}_{[C - R, C + R]}) (C + R) \leftrightarrow ({F ↾}_{[C - R, C + R]}) (C + R) < ({F ↾}_{[C - R, C + R]}) (C)$
82	72	fvresd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to ({F ↾}_{[C - R, C + R]}) (C + R) = F (C + R)$
83	82 43	breq12d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) (C + R) < ({F ↾}_{[C - R, C + R]}) (C) \leftrightarrow F (C + R) < F (C))$
84	81 83	bitrid	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) (C) <^{-1} ({F ↾}_{[C - R, C + R]}) (C + R) \leftrightarrow F (C + R) < F (C))$
85	78 84	sylibd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to F (C + R) < F (C))$
86		funfvima2	$⊢ (Fun F \land [C - R, C + R] \subseteq dom F) \to (C + R \in [C - R, C + R] \to F (C + R) \in F [[C - R, C + R]])$
87	47 50 86	syl2anc	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (C + R \in [C - R, C + R] \to F (C + R) \in F [[C - R, C + R]])$
88	72 87	mpd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C + R) \in F [[C - R, C + R]]$
89	88 56	eleqtrd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C + R) \in [x, y]$
90		elicc2	$⊢ (x \in ℝ \land y \in ℝ) \to (F (C + R) \in [x, y] \leftrightarrow (F (C + R) \in ℝ \land x \leq F (C + R) \land F (C + R) \leq y))$
91	90	ad2antrl	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C + R) \in [x, y] \leftrightarrow (F (C + R) \in ℝ \land x \leq F (C + R) \land F (C + R) \leq y))$
92	89 91	mpbid	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C + R) \in ℝ \land x \leq F (C + R) \land F (C + R) \leq y)$
93	92	simp2d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to x \leq F (C + R)$
94	7 71	sseldd	$⊢ φ \to C + R \in X$
95	22 94	ffvelcdmd	$⊢ φ \to F (C + R) \in ℝ$
96	95	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C + R) \in ℝ$
97		lelttr	$⊢ (x \in ℝ \land F (C + R) \in ℝ \land F (C) \in ℝ) \to ((x \leq F (C + R) \land F (C + R) < F (C)) \to x < F (C))$
98	62 96 24 97	syl3anc	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to ((x \leq F (C + R) \land F (C + R) < F (C)) \to x < F (C))$
99	93 98	mpand	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C + R) < F (C) \to x < F (C))$
100	85 99	syld	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to x < F (C))$
101		ax-resscn	$⊢ ℝ \subseteq ℂ$
102	101	a1i	$⊢ φ \to ℝ \subseteq ℂ$
103		fss	$⊢ (F : X ⟶ ℝ \land ℝ \subseteq ℂ) \to F : X ⟶ ℂ$
104	22 101 103	sylancl	$⊢ φ \to F : X ⟶ ℂ$
105	7 9	sstrd	$⊢ φ \to [C - R, C + R] \subseteq ℝ$
106		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
107		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
108	106 107	dvres	$⊢ ((ℝ \subseteq ℂ \land F : X ⟶ ℂ) \land (X \subseteq ℝ \land [C - R, C + R] \subseteq ℝ)) \to ℝ D ({F ↾}_{[C - R, C + R]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([C - R, C + R])}$
109	102 104 9 105 108	syl22anc	$⊢ φ \to ℝ D ({F ↾}_{[C - R, C + R]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([C - R, C + R])}$
110		iccntr	$⊢ (C - R \in ℝ \land C + R \in ℝ) \to int (topGen (ran (.))) ([C - R, C + R]) = (C - R, C + R)$
111	12 13 110	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([C - R, C + R]) = (C - R, C + R)$
112	111	reseq2d	$⊢ φ \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([C - R, C + R])} = {F_{ℝ}^{'} ↾}_{(C - R, C + R)}$
113	109 112	eqtrd	$⊢ φ \to ℝ D ({F ↾}_{[C - R, C + R]}) = {F_{ℝ}^{'} ↾}_{(C - R, C + R)}$
114	113	dmeqd	$⊢ φ \to dom {({F ↾}_{[C - R, C + R]})}_{ℝ}^{'} = dom ({F_{ℝ}^{'} ↾}_{(C - R, C + R)})$
115		dmres	$⊢ dom ({F_{ℝ}^{'} ↾}_{(C - R, C + R)}) = (C - R, C + R) \cap dom F_{ℝ}^{'}$
116		ioossicc	$⊢ (C - R, C + R) \subseteq [C - R, C + R]$
117	116 7	sstrid	$⊢ φ \to (C - R, C + R) \subseteq X$
118	117 2	sseqtrrd	$⊢ φ \to (C - R, C + R) \subseteq dom F_{ℝ}^{'}$
119		dfss2	$⊢ (C - R, C + R) \subseteq dom F_{ℝ}^{'} \leftrightarrow (C - R, C + R) \cap dom F_{ℝ}^{'} = (C - R, C + R)$
120	118 119	sylib	$⊢ φ \to (C - R, C + R) \cap dom F_{ℝ}^{'} = (C - R, C + R)$
121	115 120	eqtrid	$⊢ φ \to dom ({F_{ℝ}^{'} ↾}_{(C - R, C + R)}) = (C - R, C + R)$
122	114 121	eqtrd	$⊢ φ \to dom {({F ↾}_{[C - R, C + R]})}_{ℝ}^{'} = (C - R, C + R)$
123		resss	$⊢ {F_{ℝ}^{'} ↾}_{(C - R, C + R)} \subseteq ℝ D F$
124	113 123	eqsstrdi	$⊢ φ \to ℝ D ({F ↾}_{[C - R, C + R]}) \subseteq ℝ D F$
125		rnss	$⊢ ℝ D ({F ↾}_{[C - R, C + R]}) \subseteq ℝ D F \to ran {({F ↾}_{[C - R, C + R]})}_{ℝ}^{'} \subseteq ran F_{ℝ}^{'}$
126	124 125	syl	$⊢ φ \to ran {({F ↾}_{[C - R, C + R]})}_{ℝ}^{'} \subseteq ran F_{ℝ}^{'}$
127	126 3	ssneldd	$⊢ φ \to \neg 0 \in ran {({F ↾}_{[C - R, C + R]})}_{ℝ}^{'}$
128	12 13 19 122 127	dvne0	$⊢ φ \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \lor ({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})))$
129	128	adantr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \lor ({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})))$
130	69 100 129	mpjaod	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to x < F (C)$
131		isorel	$⊢ (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \land (C \in [C - R, C + R] \land C + R \in [C - R, C + R])) \to (C < C + R \leftrightarrow ({F ↾}_{[C - R, C + R]}) (C) < ({F ↾}_{[C - R, C + R]}) (C + R))$
132	131	biimpd	$⊢ (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \land (C \in [C - R, C + R] \land C + R \in [C - R, C + R])) \to (C < C + R \to ({F ↾}_{[C - R, C + R]}) (C) < ({F ↾}_{[C - R, C + R]}) (C + R))$
133	132	exp32	$⊢ ({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to (C \in [C - R, C + R] \to (C + R \in [C - R, C + R] \to (C < C + R \to ({F ↾}_{[C - R, C + R]}) (C) < ({F ↾}_{[C - R, C + R]}) (C + R))))$
134	133	com4l	$⊢ C \in [C - R, C + R] \to (C + R \in [C - R, C + R] \to (C < C + R \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to ({F ↾}_{[C - R, C + R]}) (C) < ({F ↾}_{[C - R, C + R]}) (C + R))))$
135	35 72 73 134	syl3c	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to ({F ↾}_{[C - R, C + R]}) (C) < ({F ↾}_{[C - R, C + R]}) (C + R))$
136	43 82	breq12d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) (C) < ({F ↾}_{[C - R, C + R]}) (C + R) \leftrightarrow F (C) < F (C + R))$
137	135 136	sylibd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to F (C) < F (C + R))$
138	92	simp3d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C + R) \leq y$
139		simprlr	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to y \in ℝ$
140		ltletr	$⊢ (F (C) \in ℝ \land F (C + R) \in ℝ \land y \in ℝ) \to ((F (C) < F (C + R) \land F (C + R) \leq y) \to F (C) < y)$
141	24 96 139 140	syl3anc	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to ((F (C) < F (C + R) \land F (C + R) \leq y) \to F (C) < y)$
142	138 141	mpan2d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C) < F (C + R) \to F (C) < y)$
143	137 142	syld	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to F (C) < y)$
144		isorel	$⊢ (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \land (C - R \in [C - R, C + R] \land C \in [C - R, C + R])) \to (C - R < C \leftrightarrow ({F ↾}_{[C - R, C + R]}) (C - R) <^{-1} ({F ↾}_{[C - R, C + R]}) (C))$
145	144	biimpd	$⊢ (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \land (C - R \in [C - R, C + R] \land C \in [C - R, C + R])) \to (C - R < C \to ({F ↾}_{[C - R, C + R]}) (C - R) <^{-1} ({F ↾}_{[C - R, C + R]}) (C))$
146	145	exp32	$⊢ ({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to (C - R \in [C - R, C + R] \to (C \in [C - R, C + R] \to (C - R < C \to ({F ↾}_{[C - R, C + R]}) (C - R) <^{-1} ({F ↾}_{[C - R, C + R]}) (C))))$
147	146	com4l	$⊢ C - R \in [C - R, C + R] \to (C \in [C - R, C + R] \to (C - R < C \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to ({F ↾}_{[C - R, C + R]}) (C - R) <^{-1} ({F ↾}_{[C - R, C + R]}) (C))))$
148	29 35 36 147	syl3c	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to ({F ↾}_{[C - R, C + R]}) (C - R) <^{-1} ({F ↾}_{[C - R, C + R]}) (C))$
149		fvex	$⊢ ({F ↾}_{[C - R, C + R]}) (C - R) \in V$
150	149 79	brcnv	$⊢ ({F ↾}_{[C - R, C + R]}) (C - R) <^{-1} ({F ↾}_{[C - R, C + R]}) (C) \leftrightarrow ({F ↾}_{[C - R, C + R]}) (C) < ({F ↾}_{[C - R, C + R]}) (C - R)$
151	43 42	breq12d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) (C) < ({F ↾}_{[C - R, C + R]}) (C - R) \leftrightarrow F (C) < F (C - R))$
152	150 151	bitrid	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) (C - R) <^{-1} ({F ↾}_{[C - R, C + R]}) (C) \leftrightarrow F (C) < F (C - R))$
153	148 152	sylibd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to F (C) < F (C - R))$
154	60	simp3d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C - R) \leq y$
155		ltletr	$⊢ (F (C) \in ℝ \land F (C - R) \in ℝ \land y \in ℝ) \to ((F (C) < F (C - R) \land F (C - R) \leq y) \to F (C) < y)$
156	24 65 139 155	syl3anc	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to ((F (C) < F (C - R) \land F (C - R) \leq y) \to F (C) < y)$
157	154 156	mpan2d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C) < F (C - R) \to F (C) < y)$
158	153 157	syld	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (({F ↾}_{[C - R, C + R]}) {Isom}_{<, <^{-1}} ([C - R, C + R], ran ({F ↾}_{[C - R, C + R]})) \to F (C) < y)$
159	143 158 129	mpjaod	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C) < y$
160	62	rexrd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to x \in ℝ^{*}$
161	139	rexrd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to y \in ℝ^{*}$
162		elioo2	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (F (C) \in (x, y) \leftrightarrow (F (C) \in ℝ \land x < F (C) \land F (C) < y))$
163	160 161 162	syl2anc	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to (F (C) \in (x, y) \leftrightarrow (F (C) \in ℝ \land x < F (C) \land F (C) < y))$
164	24 130 159 163	mpbir3and	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C) \in (x, y)$
165	56	fveq2d	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to int (topGen (ran (.))) (F [[C - R, C + R]]) = int (topGen (ran (.))) ([x, y])$
166		iccntr	$⊢ (x \in ℝ \land y \in ℝ) \to int (topGen (ran (.))) ([x, y]) = (x, y)$
167	166	ad2antrl	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to int (topGen (ran (.))) ([x, y]) = (x, y)$
168	165 167	eqtrd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to int (topGen (ran (.))) (F [[C - R, C + R]]) = (x, y)$
169	164 168	eleqtrrd	$⊢ (φ \land ((x \in ℝ \land y \in ℝ) \land ran ({F ↾}_{[C - R, C + R]}) = [x, y])) \to F (C) \in int (topGen (ran (.))) (F [[C - R, C + R]])$
170	169	expr	$⊢ (φ \land (x \in ℝ \land y \in ℝ)) \to (ran ({F ↾}_{[C - R, C + R]}) = [x, y] \to F (C) \in int (topGen (ran (.))) (F [[C - R, C + R]]))$
171	170	rexlimdvva	$⊢ φ \to (\exists x \in ℝ \exists y \in ℝ ran ({F ↾}_{[C - R, C + R]}) = [x, y] \to F (C) \in int (topGen (ran (.))) (F [[C - R, C + R]]))$
172	20 171	mpd	$⊢ φ \to F (C) \in int (topGen (ran (.))) (F [[C - R, C + R]])$

Metamath Proof Explorer

Theorem dvcnvrelem1

Proof