ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dvfgg GIF version

Theorem dvfgg 12606
Description: Explicitly write out the functionality condition on derivative for 𝑆 = ℝ and . (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jun-2023.)
Assertion
Ref Expression
dvfgg ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)

Proof of Theorem dvfgg
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 recnprss 12605 . . . . 5 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
2 reldvg 12597 . . . . 5 ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → Rel (𝑆 D 𝐹))
31, 2sylan 279 . . . 4 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → Rel (𝑆 D 𝐹))
4 elpmi 6513 . . . . . . . . . . . . . 14 (𝐹 ∈ (ℂ ↑pm 𝑆) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹𝑆))
54simpld 111 . . . . . . . . . . . . 13 (𝐹 ∈ (ℂ ↑pm 𝑆) → 𝐹:dom 𝐹⟶ℂ)
65adantl 273 . . . . . . . . . . . 12 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → 𝐹:dom 𝐹⟶ℂ)
76adantr 272 . . . . . . . . . . 11 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → 𝐹:dom 𝐹⟶ℂ)
84simprd 113 . . . . . . . . . . . . . 14 (𝐹 ∈ (ℂ ↑pm 𝑆) → dom 𝐹𝑆)
98adantl 273 . . . . . . . . . . . . 13 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → dom 𝐹𝑆)
101adantr 272 . . . . . . . . . . . . 13 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → 𝑆 ⊆ ℂ)
119, 10sstrd 3071 . . . . . . . . . . . 12 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → dom 𝐹 ⊆ ℂ)
1211adantr 272 . . . . . . . . . . 11 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → dom 𝐹 ⊆ ℂ)
13 eqid 2113 . . . . . . . . . . . . . . . . 17 (MetOpen‘(abs ∘ − )) = (MetOpen‘(abs ∘ − ))
1413cntoptopon 12515 . . . . . . . . . . . . . . . 16 (MetOpen‘(abs ∘ − )) ∈ (TopOn‘ℂ)
15 resttopon 12177 . . . . . . . . . . . . . . . 16 (((MetOpen‘(abs ∘ − )) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ (TopOn‘𝑆))
1614, 15mpan 418 . . . . . . . . . . . . . . 15 (𝑆 ⊆ ℂ → ((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ (TopOn‘𝑆))
17 topontop 12018 . . . . . . . . . . . . . . 15 (((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ (TopOn‘𝑆) → ((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ Top)
1816, 17syl 14 . . . . . . . . . . . . . 14 (𝑆 ⊆ ℂ → ((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ Top)
1910, 18syl 14 . . . . . . . . . . . . 13 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ Top)
20 toponuni 12019 . . . . . . . . . . . . . . . . 17 (((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ((MetOpen‘(abs ∘ − )) ↾t 𝑆))
2116, 20syl 14 . . . . . . . . . . . . . . . 16 (𝑆 ⊆ ℂ → 𝑆 = ((MetOpen‘(abs ∘ − )) ↾t 𝑆))
2221sseq2d 3091 . . . . . . . . . . . . . . 15 (𝑆 ⊆ ℂ → (dom 𝐹𝑆 ↔ dom 𝐹 ((MetOpen‘(abs ∘ − )) ↾t 𝑆)))
2310, 22syl 14 . . . . . . . . . . . . . 14 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (dom 𝐹𝑆 ↔ dom 𝐹 ((MetOpen‘(abs ∘ − )) ↾t 𝑆)))
249, 23mpbid 146 . . . . . . . . . . . . 13 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → dom 𝐹 ((MetOpen‘(abs ∘ − )) ↾t 𝑆))
25 eqid 2113 . . . . . . . . . . . . . 14 ((MetOpen‘(abs ∘ − )) ↾t 𝑆) = ((MetOpen‘(abs ∘ − )) ↾t 𝑆)
2625ntrss2 12127 . . . . . . . . . . . . 13 ((((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ Top ∧ dom 𝐹 ((MetOpen‘(abs ∘ − )) ↾t 𝑆)) → ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹)
2719, 24, 26syl2anc 406 . . . . . . . . . . . 12 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹)
2827sselda 3061 . . . . . . . . . . 11 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ dom 𝐹)
297, 12, 28dvlemap 12598 . . . . . . . . . 10 ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) ∧ 𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥}) → (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥)) ∈ ℂ)
3029fmpttd 5527 . . . . . . . . 9 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → (𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))):{𝑤 ∈ dom 𝐹𝑤 # 𝑥}⟶ℂ)
31 ssrab2 3146 . . . . . . . . . 10 {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ⊆ dom 𝐹
3231, 12syl5ss 3072 . . . . . . . . 9 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ⊆ ℂ)
3312, 28sseldd 3062 . . . . . . . . 9 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ ℂ)
34 simpr 109 . . . . . . . . 9 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹))
3527, 9sstrd 3071 . . . . . . . . . 10 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ⊆ 𝑆)
3635sselda 3061 . . . . . . . . 9 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → 𝑥𝑆)
3719adantr 272 . . . . . . . . . 10 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → ((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ Top)
3824adantr 272 . . . . . . . . . 10 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → dom 𝐹 ((MetOpen‘(abs ∘ − )) ↾t 𝑆))
3925ntropn 12123 . . . . . . . . . 10 ((((MetOpen‘(abs ∘ − )) ↾t 𝑆) ∈ Top ∧ dom 𝐹 ((MetOpen‘(abs ∘ − )) ↾t 𝑆)) → ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∈ ((MetOpen‘(abs ∘ − )) ↾t 𝑆))
4037, 38, 39syl2anc 406 . . . . . . . . 9 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∈ ((MetOpen‘(abs ∘ − )) ↾t 𝑆))
41 simpll 501 . . . . . . . . 9 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → 𝑆 ∈ {ℝ, ℂ})
42 rabss2 3144 . . . . . . . . . . 11 (((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ⊆ dom 𝐹 → {𝑤 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∣ 𝑤 # 𝑥} ⊆ {𝑤 ∈ dom 𝐹𝑤 # 𝑥})
4327, 42syl 14 . . . . . . . . . 10 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → {𝑤 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∣ 𝑤 # 𝑥} ⊆ {𝑤 ∈ dom 𝐹𝑤 # 𝑥})
4443adantr 272 . . . . . . . . 9 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → {𝑤 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∣ 𝑤 # 𝑥} ⊆ {𝑤 ∈ dom 𝐹𝑤 # 𝑥})
4530, 32, 33, 34, 36, 40, 41, 44, 13limcimo 12584 . . . . . . . 8 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹)) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))) lim 𝑥))
4645ex 114 . . . . . . 7 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))) lim 𝑥)))
47 moanimv 2048 . . . . . . 7 (∃*𝑦(𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))) lim 𝑥)) ↔ (𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) → ∃*𝑦 𝑦 ∈ ((𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))) lim 𝑥)))
4846, 47sylibr 133 . . . . . 6 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ∃*𝑦(𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))) lim 𝑥)))
49 eqid 2113 . . . . . . . 8 ((MetOpen‘(abs ∘ − )) ↾t 𝑆) = ((MetOpen‘(abs ∘ − )) ↾t 𝑆)
50 eqid 2113 . . . . . . . 8 (𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))) = (𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥)))
5149, 13, 50, 10, 6, 9eldvap 12600 . . . . . . 7 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑥(𝑆 D 𝐹)𝑦 ↔ (𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))) lim 𝑥))))
5251mobidv 2009 . . . . . 6 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (∃*𝑦 𝑥(𝑆 D 𝐹)𝑦 ↔ ∃*𝑦(𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑆))‘dom 𝐹) ∧ 𝑦 ∈ ((𝑧 ∈ {𝑤 ∈ dom 𝐹𝑤 # 𝑥} ↦ (((𝐹𝑧) − (𝐹𝑥)) / (𝑧𝑥))) lim 𝑥))))
5348, 52mpbird 166 . . . . 5 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ∃*𝑦 𝑥(𝑆 D 𝐹)𝑦)
5453alrimiv 1826 . . . 4 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ∀𝑥∃*𝑦 𝑥(𝑆 D 𝐹)𝑦)
55 dffun6 5093 . . . 4 (Fun (𝑆 D 𝐹) ↔ (Rel (𝑆 D 𝐹) ∧ ∀𝑥∃*𝑦 𝑥(𝑆 D 𝐹)𝑦))
563, 54, 55sylanbrc 411 . . 3 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → Fun (𝑆 D 𝐹))
5756funfnd 5110 . 2 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D 𝐹) Fn dom (𝑆 D 𝐹))
58 vex 2658 . . . . 5 𝑦 ∈ V
5958elrn 4740 . . . 4 (𝑦 ∈ ran (𝑆 D 𝐹) ↔ ∃𝑥 𝑥(𝑆 D 𝐹)𝑦)
6010, 6, 9dvcl 12601 . . . . . 6 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ 𝑥(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ)
6160ex 114 . . . . 5 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑥(𝑆 D 𝐹)𝑦𝑦 ∈ ℂ))
6261exlimdv 1771 . . . 4 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (∃𝑥 𝑥(𝑆 D 𝐹)𝑦𝑦 ∈ ℂ))
6359, 62syl5bi 151 . . 3 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑦 ∈ ran (𝑆 D 𝐹) → 𝑦 ∈ ℂ))
6463ssrdv 3067 . 2 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ran (𝑆 D 𝐹) ⊆ ℂ)
65 df-f 5083 . 2 ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ ((𝑆 D 𝐹) Fn dom (𝑆 D 𝐹) ∧ ran (𝑆 D 𝐹) ⊆ ℂ))
6657, 64, 65sylanbrc 411 1 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1310   = wceq 1312  wex 1449  wcel 1461  ∃*wmo 1974  {crab 2392  wss 3035  {cpr 3492   cuni 3700   class class class wbr 3893  cmpt 3947  dom cdm 4497  ran crn 4498  ccom 4501  Rel wrel 4502  Fun wfun 5073   Fn wfn 5074  wf 5075  cfv 5079  (class class class)co 5726  pm cpm 6495  cc 7539  cr 7540  cmin 7850   # cap 8255   / cdiv 8339  abscabs 10655  t crest 11957  MetOpencmopn 11991  Topctop 12001  TopOnctopon 12014  intcnt 12099   lim climc 12573   D cdv 12574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-iinf 4460  ax-cnex 7630  ax-resscn 7631  ax-1cn 7632  ax-1re 7633  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-mulrcl 7638  ax-addcom 7639  ax-mulcom 7640  ax-addass 7641  ax-mulass 7642  ax-distr 7643  ax-i2m1 7644  ax-0lt1 7645  ax-1rid 7646  ax-0id 7647  ax-rnegex 7648  ax-precex 7649  ax-cnre 7650  ax-pre-ltirr 7651  ax-pre-ltwlin 7652  ax-pre-lttrn 7653  ax-pre-apti 7654  ax-pre-ltadd 7655  ax-pre-mulgt0 7656  ax-pre-mulext 7657  ax-arch 7658  ax-caucvg 7659
This theorem depends on definitions:  df-bi 116  df-stab 799  df-dc 803  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-reu 2395  df-rmo 2396  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-if 3439  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-po 4176  df-iso 4177  df-iord 4246  df-on 4248  df-ilim 4249  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-isom 5088  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-1st 5990  df-2nd 5991  df-recs 6154  df-frec 6240  df-map 6496  df-pm 6497  df-sup 6821  df-inf 6822  df-pnf 7720  df-mnf 7721  df-xr 7722  df-ltxr 7723  df-le 7724  df-sub 7852  df-neg 7853  df-reap 8249  df-ap 8256  df-div 8340  df-inn 8625  df-2 8683  df-3 8684  df-4 8685  df-n0 8876  df-z 8953  df-uz 9223  df-q 9308  df-rp 9338  df-xneg 9446  df-xadd 9447  df-seqfrec 10106  df-exp 10180  df-cj 10501  df-re 10502  df-im 10503  df-rsqrt 10656  df-abs 10657  df-rest 11959  df-topgen 11978  df-psmet 11993  df-xmet 11994  df-met 11995  df-bl 11996  df-mopn 11997  df-top 12002  df-topon 12015  df-bases 12047  df-ntr 12102  df-limced 12575  df-dvap 12576
This theorem is referenced by:  dvfpm  12607  dvfcnpm  12608  dvaddxx  12615  dviaddf  12616
  Copyright terms: Public domain W3C validator