dvcnvre

Description: The derivative rule for inverse functions. If F is a continuous and differentiable bijective function from X to Y which never has derivative 0 , then ` ``' F is also differentiable, and its derivative is the reciprocal of the derivative of F ` . (Contributed by Mario Carneiro, 24-Feb-2015)

	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$
Assertion	dvcnvre	$⊢ φ \to ℝ D F^{-1} = (x \in Y ⟼ \frac{1}{F_{ℝ}^{'} (F^{-1} (x))})$

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		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
6	5	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
7		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
8	7	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
9		retop	$⊢ topGen (ran (.)) \in Top$
10		f1ofo	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{onto}{⟶} Y$
11		forn	$⊢ F : X \underset{onto}{⟶} Y \to ran F = Y$
12	4 10 11	3syl	$⊢ φ \to ran F = Y$
13		cncff	$⊢ F : X \underset{cn}{⟶} ℝ \to F : X ⟶ ℝ$
14		frn	$⊢ F : X ⟶ ℝ \to ran F \subseteq ℝ$
15	1 13 14	3syl	$⊢ φ \to ran F \subseteq ℝ$
16	12 15	eqsstrrd	$⊢ φ \to Y \subseteq ℝ$
17		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
18	17	ntrss2	$⊢ (topGen (ran (.)) \in Top \land Y \subseteq ℝ) \to int (topGen (ran (.))) (Y) \subseteq Y$
19	9 16 18	sylancr	$⊢ φ \to int (topGen (ran (.))) (Y) \subseteq Y$
20		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land x \in Y) \to F (F^{-1} (x)) = x$
21	4 20	sylan	$⊢ (φ \land x \in Y) \to F (F^{-1} (x)) = x$
22		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
23	22	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
24		dvbsss	$⊢ dom F_{ℝ}^{'} \subseteq ℝ$
25	24	a1i	$⊢ φ \to dom F_{ℝ}^{'} \subseteq ℝ$
26	2 25	eqsstrrd	$⊢ φ \to X \subseteq ℝ$
27	17	ntrss2	$⊢ (topGen (ran (.)) \in Top \land X \subseteq ℝ) \to int (topGen (ran (.))) (X) \subseteq X$
28	9 26 27	sylancr	$⊢ φ \to int (topGen (ran (.))) (X) \subseteq X$
29		ax-resscn	$⊢ ℝ \subseteq ℂ$
30	29	a1i	$⊢ φ \to ℝ \subseteq ℂ$
31	1 13	syl	$⊢ φ \to F : X ⟶ ℝ$
32		fss	$⊢ (F : X ⟶ ℝ \land ℝ \subseteq ℂ) \to F : X ⟶ ℂ$
33	31 29 32	sylancl	$⊢ φ \to F : X ⟶ ℂ$
34	30 33 26 6 5	dvbssntr	$⊢ φ \to dom F_{ℝ}^{'} \subseteq int (topGen (ran (.))) (X)$
35	2 34	eqsstrrd	$⊢ φ \to X \subseteq int (topGen (ran (.))) (X)$
36	28 35	eqssd	$⊢ φ \to int (topGen (ran (.))) (X) = X$
37	17	isopn3	$⊢ (topGen (ran (.)) \in Top \land X \subseteq ℝ) \to (X \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (X) = X)$
38	9 26 37	sylancr	$⊢ φ \to (X \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (X) = X)$
39	36 38	mpbird	$⊢ φ \to X \in topGen (ran (.))$
40		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
41		f1of	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} : Y ⟶ X$
42	4 40 41	3syl	$⊢ φ \to F^{-1} : Y ⟶ X$
43	42	ffvelrnda	$⊢ (φ \land x \in Y) \to F^{-1} (x) \in X$
44		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
45	22 44	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
46	45	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land X \in topGen (ran (.)) \land F^{-1} (x) \in X) \to \exists r \in ℝ^{+} F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X$
47	23 39 43 46	mp3an2ani	$⊢ (φ \land x \in Y) \to \exists r \in ℝ^{+} F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X$
48	1	ad2antrr	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to F : X \underset{cn}{⟶} ℝ$
49	2	ad2antrr	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to dom F_{ℝ}^{'} = X$
50	3	ad2antrr	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to \neg 0 \in ran F_{ℝ}^{'}$
51	4	ad2antrr	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to F : X \underset{1-1 onto}{⟶} Y$
52	43	adantr	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to F^{-1} (x) \in X$
53		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
54	53	ad2antrl	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to \frac{r}{2} \in ℝ^{+}$
55	26	ad2antrr	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to X \subseteq ℝ$
56	55 52	sseldd	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to F^{-1} (x) \in ℝ$
57	54	rpred	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to \frac{r}{2} \in ℝ$
58	56 57	resubcld	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to F^{-1} (x) - (\frac{r}{2}) \in ℝ$
59	56 57	readdcld	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to F^{-1} (x) + (\frac{r}{2}) \in ℝ$
60		elicc2	$⊢ (F^{-1} (x) - (\frac{r}{2}) \in ℝ \land F^{-1} (x) + (\frac{r}{2}) \in ℝ) \to (y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})] \leftrightarrow (y \in ℝ \land F^{-1} (x) - (\frac{r}{2}) \leq y \land y \leq F^{-1} (x) + (\frac{r}{2})))$
61	58 59 60	syl2anc	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to (y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})] \leftrightarrow (y \in ℝ \land F^{-1} (x) - (\frac{r}{2}) \leq y \land y \leq F^{-1} (x) + (\frac{r}{2})))$
62	61	biimpa	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to (y \in ℝ \land F^{-1} (x) - (\frac{r}{2}) \leq y \land y \leq F^{-1} (x) + (\frac{r}{2}))$
63	62	simp1d	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to y \in ℝ$
64	56	adantr	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) \in ℝ$
65		simplrl	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to r \in ℝ^{+}$
66	65	rpred	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to r \in ℝ$
67	64 66	resubcld	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) - r \in ℝ$
68	58	adantr	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) - (\frac{r}{2}) \in ℝ$
69	65 53	syl	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to \frac{r}{2} \in ℝ^{+}$
70	69	rpred	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to \frac{r}{2} \in ℝ$
71		rphalflt	$⊢ r \in ℝ^{+} \to \frac{r}{2} < r$
72	65 71	syl	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to \frac{r}{2} < r$
73	70 66 64 72	ltsub2dd	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) - r < F^{-1} (x) - (\frac{r}{2})$
74	62	simp2d	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) - (\frac{r}{2}) \leq y$
75	67 68 63 73 74	ltletrd	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) - r < y$
76	59	adantr	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) + (\frac{r}{2}) \in ℝ$
77	64 66	readdcld	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) + r \in ℝ$
78	62	simp3d	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to y \leq F^{-1} (x) + (\frac{r}{2})$
79	70 66 64 72	ltadd2dd	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) + (\frac{r}{2}) < F^{-1} (x) + r$
80	63 76 77 78 79	lelttrd	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to y < F^{-1} (x) + r$
81	67	rexrd	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) - r \in ℝ^{*}$
82	77	rexrd	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to F^{-1} (x) + r \in ℝ^{*}$
83		elioo2	$⊢ (F^{-1} (x) - r \in ℝ^{} \land F^{-1} (x) + r \in ℝ^{}) \to (y \in (F^{-1} (x) - r, F^{-1} (x) + r) \leftrightarrow (y \in ℝ \land F^{-1} (x) - r < y \land y < F^{-1} (x) + r))$
84	81 82 83	syl2anc	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to (y \in (F^{-1} (x) - r, F^{-1} (x) + r) \leftrightarrow (y \in ℝ \land F^{-1} (x) - r < y \land y < F^{-1} (x) + r))$
85	63 75 80 84	mpbir3and	$⊢ (((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \land y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})]) \to y \in (F^{-1} (x) - r, F^{-1} (x) + r)$
86	85	ex	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to (y \in [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})] \to y \in (F^{-1} (x) - r, F^{-1} (x) + r))$
87	86	ssrdv	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})] \subseteq (F^{-1} (x) - r, F^{-1} (x) + r)$
88		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
89	88	ad2antrl	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to r \in ℝ$
90	22	bl2ioo	$⊢ (F^{-1} (x) \in ℝ \land r \in ℝ) \to F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (F^{-1} (x) - r, F^{-1} (x) + r)$
91	56 89 90	syl2anc	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (F^{-1} (x) - r, F^{-1} (x) + r)$
92	87 91	sseqtrrd	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})] \subseteq F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r$
93		simprr	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X$
94	92 93	sstrd	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to [F^{-1} (x) - (\frac{r}{2}), F^{-1} (x) + (\frac{r}{2})] \subseteq X$
95		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
96		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} X = TopOpen (ℂ_{fld}) ↾_{𝑡} X$
97		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} Y = TopOpen (ℂ_{fld}) ↾_{𝑡} Y$
98	48 49 50 51 52 54 94 95 5 96 97	dvcnvrelem2	$⊢ ((φ \land x \in Y) \land (r \in ℝ^{+} \land F^{-1} (x) ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq X)) \to (F (F^{-1} (x)) \in int (topGen (ran (.))) (Y) \land F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (F (F^{-1} (x))))$
99	47 98	rexlimddv	$⊢ (φ \land x \in Y) \to (F (F^{-1} (x)) \in int (topGen (ran (.))) (Y) \land F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (F (F^{-1} (x))))$
100	99	simpld	$⊢ (φ \land x \in Y) \to F (F^{-1} (x)) \in int (topGen (ran (.))) (Y)$
101	21 100	eqeltrrd	$⊢ (φ \land x \in Y) \to x \in int (topGen (ran (.))) (Y)$
102	19 101	eqelssd	$⊢ φ \to int (topGen (ran (.))) (Y) = Y$
103	17	isopn3	$⊢ (topGen (ran (.)) \in Top \land Y \subseteq ℝ) \to (Y \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (Y) = Y)$
104	9 16 103	sylancr	$⊢ φ \to (Y \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (Y) = Y)$
105	102 104	mpbird	$⊢ φ \to Y \in topGen (ran (.))$
106	99	simprd	$⊢ (φ \land x \in Y) \to F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (F (F^{-1} (x)))$
107	21	fveq2d	$⊢ (φ \land x \in Y) \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (F (F^{-1} (x))) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (x)$
108	106 107	eleqtrd	$⊢ (φ \land x \in Y) \to F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (x)$
109	108	ralrimiva	$⊢ φ \to \forall x \in Y F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (x)$
110	5	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
111	16 29	sstrdi	$⊢ φ \to Y \subseteq ℂ$
112		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land Y \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} Y \in TopOn (Y)$
113	110 111 112	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} Y \in TopOn (Y)$
114	26 29	sstrdi	$⊢ φ \to X \subseteq ℂ$
115		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land X \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} X \in TopOn (X)$
116	110 114 115	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} X \in TopOn (X)$
117		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} Y \in TopOn (Y) \land TopOpen (ℂ_{fld}) ↾_{𝑡} X \in TopOn (X)) \to (F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) \leftrightarrow (F^{-1} : Y ⟶ X \land \forall x \in Y F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (x)))$
118	113 116 117	syl2anc	$⊢ φ \to (F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) \leftrightarrow (F^{-1} : Y ⟶ X \land \forall x \in Y F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} X)) (x)))$
119	42 109 118	mpbir2and	$⊢ φ \to F^{-1} \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} Y) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} X))$
120	5 97 96	cncfcn	$⊢ (Y \subseteq ℂ \land X \subseteq ℂ) \to Y \underset{cn}{⟶} X = (TopOpen (ℂ_{fld}) ↾_{𝑡} Y) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} X)$
121	111 114 120	syl2anc	$⊢ φ \to Y \underset{cn}{⟶} X = (TopOpen (ℂ_{fld}) ↾_{𝑡} Y) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} X)$
122	119 121	eleqtrrd	$⊢ φ \to F^{-1} : Y \underset{cn}{⟶} X$
123	5 6 8 105 4 122 2 3	dvcnv	$⊢ φ \to ℝ D F^{-1} = (x \in Y ⟼ \frac{1}{F_{ℝ}^{'} (F^{-1} (x))})$

Metamath Proof Explorer

Theorem dvcnvre

Proof