Theorem reldv

Description: The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	reldv	⊢ Rel ( 𝑆 D 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		relxp	⊢ Rel ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
2	1	rgenw	⊢ ∀ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) Rel ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
3		reliun	⊢ ( Rel ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) Rel ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
4	2 3	mpbir	⊢ Rel ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
5		df-rel	⊢ ( Rel ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ↔ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( V × V ) )
6	4 5	mpbi	⊢ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( V × V )
7	6	rgenw	⊢ ∀ 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( V × V )
8	7	rgenw	⊢ ∀ 𝑠 ∈ 𝒫 ℂ ∀ 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( V × V )
9		df-dv	⊢ D = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
10	9	ovmptss	⊢ ( ∀ 𝑠 ∈ 𝒫 ℂ ∀ 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ⊆ ( V × V ) → ( 𝑆 D 𝐹 ) ⊆ ( V × V ) )
11	8 10	ax-mp	⊢ ( 𝑆 D 𝐹 ) ⊆ ( V × V )
12		df-rel	⊢ ( Rel ( 𝑆 D 𝐹 ) ↔ ( 𝑆 D 𝐹 ) ⊆ ( V × V ) )
13	11 12	mpbir	⊢ Rel ( 𝑆 D 𝐹 )