dvcnvre - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvcnvre		Structured version Visualization version GIF version

Theorem dvcnvre 24219

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

**Hypotheses**
Ref	Expression
dvcnvre.f	⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ))
dvcnvre.d	⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋)
dvcnvre.z	⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))
dvcnvre.1	⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)

**Assertion**
Ref	Expression
dvcnvre	⊢ (𝜑 → (ℝ D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((ℝ D 𝐹)‘(^◡𝐹‘𝑥)))))

Distinct variable groups: 𝑥,𝐹 𝜑,𝑥 𝑥,𝑋 𝑥,𝑌

Proof of Theorem dvcnvre Dummy variables 𝑦 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2778	. 2 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
2	1	tgioo2 23014	. 2 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
3		reelprrecn 10364	. . 3 ⊢ ℝ ∈ {ℝ, ℂ}
4	3	a1i 11	. 2 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
5		retop 22973	. . . . 5 ⊢ (topGen‘ran (,)) ∈ Top
6		dvcnvre.1	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌)
7		f1ofo 6398	. . . . . . 7 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌)
8		forn 6369	. . . . . . 7 ⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌)
9	6, 7, 8	3syl 18	. . . . . 6 ⊢ (𝜑 → ran 𝐹 = 𝑌)
10		dvcnvre.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ))
11		cncff 23104	. . . . . . 7 ⊢ (𝐹 ∈ (𝑋–cn→ℝ) → 𝐹:𝑋⟶ℝ)
12		frn 6297	. . . . . . 7 ⊢ (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ)
13	10, 11, 12	3syl 18	. . . . . 6 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
14	9, 13	eqsstr3d 3859	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ ℝ)
15		uniretop 22974	. . . . . 6 ⊢ ℝ = ∪ (topGen‘ran (,))
16	15	ntrss2 21269	. . . . 5 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑌 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝑌) ⊆ 𝑌)
17	5, 14, 16	sylancr 581	. . . 4 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝑌) ⊆ 𝑌)
18		f1ocnvfv2 6805	. . . . . 6 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
19	6, 18	sylan 575	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
20		f1ocnv 6403	. . . . . . . . . 10 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
21		f1of 6391	. . . . . . . . . 10 ⊢ (^◡𝐹:𝑌–1-1-onto→𝑋 → ^◡𝐹:𝑌⟶𝑋)
22	6, 20, 21	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹:𝑌⟶𝑋)
23	22	ffvelrnda 6623	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (^◡𝐹‘𝑥) ∈ 𝑋)
24		dvcnvre.d	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋)
25		dvbsss 24103	. . . . . . . . . . . . . 14 ⊢ dom (ℝ D 𝐹) ⊆ ℝ
26	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ℝ)
27	24, 26	eqsstr3d 3859	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ⊆ ℝ)
28	15	ntrss2 21269	. . . . . . . . . . . 12 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑋 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝑋) ⊆ 𝑋)
29	5, 27, 28	sylancr 581	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝑋) ⊆ 𝑋)
30		ax-resscn 10329	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
31	30	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℝ ⊆ ℂ)
32	10, 11	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)
33		fss 6304	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑋⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝑋⟶ℂ)
34	32, 30, 33	sylancl 580	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
35	31, 34, 27, 2, 1	dvbssntr 24101	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ((int‘(topGen‘ran (,)))‘𝑋))
36	24, 35	eqsstr3d 3859	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ⊆ ((int‘(topGen‘ran (,)))‘𝑋))
37	29, 36	eqssd 3838	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝑋) = 𝑋)
38	15	isopn3 21278	. . . . . . . . . . 11 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑋 ⊆ ℝ) → (𝑋 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝑋) = 𝑋))
39	5, 27, 38	sylancr 581	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝑋) = 𝑋))
40	37, 39	mpbird 249	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (topGen‘ran (,)))
41		eqid 2778	. . . . . . . . . . 11 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
42	41	rexmet 23002	. . . . . . . . . 10 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
43		eqid 2778	. . . . . . . . . . . 12 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
44	41, 43	tgioo 23007	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
45	44	mopni2 22706	. . . . . . . . . 10 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝑋 ∈ (topGen‘ran (,)) ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → ∃𝑟 ∈ ℝ⁺ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)
46	42, 45	mp3an1 1521	. . . . . . . . 9 ⊢ ((𝑋 ∈ (topGen‘ran (,)) ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → ∃𝑟 ∈ ℝ⁺ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)
47	40, 46	sylan 575	. . . . . . . 8 ⊢ ((𝜑 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → ∃𝑟 ∈ ℝ⁺ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)
48	23, 47	syldan 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ∃𝑟 ∈ ℝ⁺ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)
49	10	ad2antrr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝐹 ∈ (𝑋–cn→ℝ))
50	24	ad2antrr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → dom (ℝ D 𝐹) = 𝑋)
51		dvcnvre.z	. . . . . . . . 9 ⊢ (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))
52	51	ad2antrr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ¬ 0 ∈ ran (ℝ D 𝐹))
53	6	ad2antrr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝐹:𝑋–1-1-onto→𝑌)
54	23	adantr 474	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (^◡𝐹‘𝑥) ∈ 𝑋)
55		rphalfcl 12166	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) ∈ ℝ⁺)
56	55	ad2antrl 718	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑟 / 2) ∈ ℝ⁺)
57	27	ad2antrr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝑋 ⊆ ℝ)
58	57, 54	sseldd 3822	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (^◡𝐹‘𝑥) ∈ ℝ)
59	56	rpred 12181	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑟 / 2) ∈ ℝ)
60	58, 59	resubcld 10803	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((^◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ)
61	58, 59	readdcld 10406	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((^◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ)
62		elicc2 12550	. . . . . . . . . . . . . . . 16 ⊢ ((((^◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ ∧ ((^◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ) → (𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ↔ (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((^◡𝐹‘𝑥) + (𝑟 / 2)))))
63	60, 61, 62	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ↔ (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((^◡𝐹‘𝑥) + (𝑟 / 2)))))
64	63	biimpa 470	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((^◡𝐹‘𝑥) + (𝑟 / 2))))
65	64	simp1d 1133	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ∈ ℝ)
66	58	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (^◡𝐹‘𝑥) ∈ ℝ)
67		simplrl 767	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑟 ∈ ℝ⁺)
68	67	rpred 12181	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑟 ∈ ℝ)
69	66, 68	resubcld 10803	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − 𝑟) ∈ ℝ)
70	60	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ)
71	67, 55	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ⁺)
72	71	rpred 12181	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ)
73		rphalflt 12168	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ ℝ⁺ → (𝑟 / 2) < 𝑟)
74	67, 73	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) < 𝑟)
75	72, 68, 66, 74	ltsub2dd 10988	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − 𝑟) < ((^◡𝐹‘𝑥) − (𝑟 / 2)))
76	64	simp2d 1134	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦)
77	69, 70, 65, 75, 76	ltletrd 10536	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − 𝑟) < 𝑦)
78	61	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ)
79	66, 68	readdcld 10406	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) + 𝑟) ∈ ℝ)
80	64	simp3d 1135	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ≤ ((^◡𝐹‘𝑥) + (𝑟 / 2)))
81	72, 68, 66, 74	ltadd2dd 10535	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) + (𝑟 / 2)) < ((^◡𝐹‘𝑥) + 𝑟))
82	65, 78, 79, 80, 81	lelttrd 10534	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 < ((^◡𝐹‘𝑥) + 𝑟))
83	69	rexrd 10426	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) − 𝑟) ∈ ℝ^*)
84	79	rexrd 10426	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → ((^◡𝐹‘𝑥) + 𝑟) ∈ ℝ^*)
85		elioo2 12528	. . . . . . . . . . . . . 14 ⊢ ((((^◡𝐹‘𝑥) − 𝑟) ∈ ℝ^* ∧ ((^◡𝐹‘𝑥) + 𝑟) ∈ ℝ^*) → (𝑦 ∈ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)) ↔ (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − 𝑟) < 𝑦 ∧ 𝑦 < ((^◡𝐹‘𝑥) + 𝑟))))
86	83, 84, 85	syl2anc 579	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑦 ∈ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)) ↔ (𝑦 ∈ ℝ ∧ ((^◡𝐹‘𝑥) − 𝑟) < 𝑦 ∧ 𝑦 < ((^◡𝐹‘𝑥) + 𝑟))))
87	65, 77, 82, 86	mpbir3and 1399	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ∈ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)))
88	87	ex 403	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑦 ∈ (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) → 𝑦 ∈ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟))))
89	88	ssrdv 3827	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)))
90		rpre 12145	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
91	90	ad2antrl 718	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝑟 ∈ ℝ)
92	41	bl2ioo 23003	. . . . . . . . . . 11 ⊢ (((^◡𝐹‘𝑥) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)))
93	58, 91, 92	syl2anc 579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (((^◡𝐹‘𝑥) − 𝑟)(,)((^◡𝐹‘𝑥) + 𝑟)))
94	89, 93	sseqtr4d 3861	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟))
95		simprr 763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)
96	94, 95	sstrd 3831	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((^◡𝐹‘𝑥) − (𝑟 / 2))[,]((^◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ 𝑋)
97		eqid 2778	. . . . . . . 8 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
98		eqid 2778	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑋) = ((TopOpen‘ℂ_fld) ↾_t 𝑋)
99		eqid 2778	. . . . . . . 8 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑌) = ((TopOpen‘ℂ_fld) ↾_t 𝑌)
100	49, 50, 52, 53, 54, 56, 96, 97, 1, 98, 99	dvcnvrelem2 24218	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ⁺ ∧ ((^◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((𝐹‘(^◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran (,)))‘𝑌) ∧ ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘(𝐹‘(^◡𝐹‘𝑥)))))
101	48, 100	rexlimddv 3218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝐹‘(^◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran (,)))‘𝑌) ∧ ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘(𝐹‘(^◡𝐹‘𝑥)))))
102	101	simpld 490	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran (,)))‘𝑌))
103	19, 102	eqeltrrd 2860	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ ((int‘(topGen‘ran (,)))‘𝑌))
104	17, 103	eqelssd 3841	. . 3 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝑌) = 𝑌)
105	15	isopn3 21278	. . . 4 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝑌 ⊆ ℝ) → (𝑌 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝑌) = 𝑌))
106	5, 14, 105	sylancr 581	. . 3 ⊢ (𝜑 → (𝑌 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝑌) = 𝑌))
107	104, 106	mpbird 249	. 2 ⊢ (𝜑 → 𝑌 ∈ (topGen‘ran (,)))
108	101	simprd 491	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘(𝐹‘(^◡𝐹‘𝑥))))
109	19	fveq2d 6450	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘(𝐹‘(^◡𝐹‘𝑥))) = ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))
110	108, 109	eleqtrd 2861	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))
111	110	ralrimiva 3148	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑌 ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))
112	1	cnfldtopon 22994	. . . . . 6 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
113	14, 30	syl6ss 3833	. . . . . 6 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
114		resttopon 21373	. . . . . 6 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑌 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑌) ∈ (TopOn‘𝑌))
115	112, 113, 114	sylancr 581	. . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑌) ∈ (TopOn‘𝑌))
116	27, 30	syl6ss 3833	. . . . . 6 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
117		resttopon 21373	. . . . . 6 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑋 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑋) ∈ (TopOn‘𝑋))
118	112, 116, 117	sylancr 581	. . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑋) ∈ (TopOn‘𝑋))
119		cncnp 21492	. . . . 5 ⊢ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) ∈ (TopOn‘𝑌) ∧ ((TopOpen‘ℂ_fld) ↾_t 𝑋) ∈ (TopOn‘𝑋)) → (^◡𝐹 ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)) ↔ (^◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑌 ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))))
120	115, 118, 119	syl2anc 579	. . . 4 ⊢ (𝜑 → (^◡𝐹 ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)) ↔ (^◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑌 ^◡𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑌) CnP ((TopOpen‘ℂ_fld) ↾_t 𝑋))‘𝑥))))
121	22, 111, 120	mpbir2and 703	. . 3 ⊢ (𝜑 → ^◡𝐹 ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)))
122	1, 99, 98	cncfcn 23120	. . . 4 ⊢ ((𝑌 ⊆ ℂ ∧ 𝑋 ⊆ ℂ) → (𝑌–cn→𝑋) = (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)))
123	113, 116, 122	syl2anc 579	. . 3 ⊢ (𝜑 → (𝑌–cn→𝑋) = (((TopOpen‘ℂ_fld) ↾_t 𝑌) Cn ((TopOpen‘ℂ_fld) ↾_t 𝑋)))
124	121, 123	eleqtrrd 2862	. 2 ⊢ (𝜑 → ^◡𝐹 ∈ (𝑌–cn→𝑋))
125	1, 2, 4, 107, 6, 124, 24, 51	dvcnv 24177	1 ⊢ (𝜑 → (ℝ D ^◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((ℝ D 𝐹)‘(^◡𝐹‘𝑥)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 386 ∧ w3a 1071 = wceq 1601 ∈ wcel 2107 ∀wral 3090 ∃wrex 3091 ⊆ wss 3792 {cpr 4400 class class class wbr 4886 ↦ cmpt 4965 × cxp 5353 ^◡ccnv 5354 dom cdm 5355 ran crn 5356 ↾ cres 5357 ∘ ccom 5359 ⟶wf 6131 –onto→wfo 6133 –1-1-onto→wf1o 6134 ‘cfv 6135 (class class class)co 6922 ℂcc 10270 ℝcr 10271 0cc0 10272 1c1 10273 + caddc 10275 ℝ^*cxr 10410 < clt 10411 ≤ cle 10412 − cmin 10606 / cdiv 11032 2c2 11430 ℝ⁺crp 12137 (,)cioo 12487 [,]cicc 12490 abscabs 14381 ↾_t crest 16467 TopOpenctopn 16468 topGenctg 16484 ∞Metcxmet 20127 ballcbl 20129 MetOpencmopn 20132 ℂ_fldccnfld 20142 Topctop 21105 TopOnctopon 21122 intcnt 21229 Cn ccn 21436 CnP ccnp 21437 –cn→ccncf 23087 D cdv 24064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5006 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-inf2 8835 ax-cnex 10328 ax-resscn 10329 ax-1cn 10330 ax-icn 10331 ax-addcl 10332 ax-addrcl 10333 ax-mulcl 10334 ax-mulrcl 10335 ax-mulcom 10336 ax-addass 10337 ax-mulass 10338 ax-distr 10339 ax-i2m1 10340 ax-1ne0 10341 ax-1rid 10342 ax-rnegex 10343 ax-rrecex 10344 ax-cnre 10345 ax-pre-lttri 10346 ax-pre-lttrn 10347 ax-pre-ltadd 10348 ax-pre-mulgt0 10349 ax-pre-sup 10350 ax-addf 10351 ax-mulf 10352

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rmo 3098 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4672 df-int 4711 df-iun 4755 df-iin 4756 df-br 4887 df-opab 4949 df-mpt 4966 df-tr 4988 df-id 5261 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-se 5315 df-we 5316 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-pred 5933 df-ord 5979 df-on 5980 df-lim 5981 df-suc 5982 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-fv 6143 df-isom 6144 df-riota 6883 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-of 7174 df-om 7344 df-1st 7445 df-2nd 7446 df-supp 7577 df-wrecs 7689 df-recs 7751 df-rdg 7789 df-1o 7843 df-2o 7844 df-oadd 7847 df-er 8026 df-map 8142 df-pm 8143 df-ixp 8195 df-en 8242 df-dom 8243 df-sdom 8244 df-fin 8245 df-fsupp 8564 df-fi 8605 df-sup 8636 df-inf 8637 df-oi 8704 df-card 9098 df-cda 9325 df-pnf 10413 df-mnf 10414 df-xr 10415 df-ltxr 10416 df-le 10417 df-sub 10608 df-neg 10609 df-div 11033 df-nn 11375 df-2 11438 df-3 11439 df-4 11440 df-5 11441 df-6 11442 df-7 11443 df-8 11444 df-9 11445 df-n0 11643 df-z 11729 df-dec 11846 df-uz 11993 df-q 12096 df-rp 12138 df-xneg 12257 df-xadd 12258 df-xmul 12259 df-ioo 12491 df-ico 12493 df-icc 12494 df-fz 12644 df-fzo 12785 df-seq 13120 df-exp 13179 df-hash 13436 df-cj 14246 df-re 14247 df-im 14248 df-sqrt 14382 df-abs 14383 df-struct 16257 df-ndx 16258 df-slot 16259 df-base 16261 df-sets 16262 df-ress 16263 df-plusg 16351 df-mulr 16352 df-starv 16353 df-sca 16354 df-vsca 16355 df-ip 16356 df-tset 16357 df-ple 16358 df-ds 16360 df-unif 16361 df-hom 16362 df-cco 16363 df-rest 16469 df-topn 16470 df-0g 16488 df-gsum 16489 df-topgen 16490 df-pt 16491 df-prds 16494 df-xrs 16548 df-qtop 16553 df-imas 16554 df-xps 16556 df-mre 16632 df-mrc 16633 df-acs 16635 df-mgm 17628 df-sgrp 17670 df-mnd 17681 df-submnd 17722 df-mulg 17928 df-cntz 18133 df-cmn 18581 df-psmet 20134 df-xmet 20135 df-met 20136 df-bl 20137 df-mopn 20138 df-fbas 20139 df-fg 20140 df-cnfld 20143 df-top 21106 df-topon 21123 df-topsp 21145 df-bases 21158 df-cld 21231 df-ntr 21232 df-cls 21233 df-nei 21310 df-lp 21348 df-perf 21349 df-cn 21439 df-cnp 21440 df-haus 21527 df-cmp 21599 df-tx 21774 df-hmeo 21967 df-fil 22058 df-fm 22150 df-flim 22151 df-flf 22152 df-xms 22533 df-ms 22534 df-tms 22535 df-cncf 23089 df-limc 24067 df-dv 24068

This theorem is referenced by: dvrelog 24820

W3C validator