Metamath Proof Explorer

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 ⁡ F S ′

Proof

Step Hyp Ref Expression
1 relxp ⊢ Rel ⁡ x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
2 1 rgenw ⊢ ∀ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f Rel ⁡ x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
3 reliun ⊢ Rel ⁡ ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x ↔ ∀ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f Rel ⁡ x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
4 2 3 mpbir ⊢ Rel ⁡ ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
5 df-rel ⊢ Rel ⁡ ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x ↔ ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x ⊆ V × V
6 4 5 mpbi ⊢ ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x ⊆ V × V
7 6 rgenw ⊢ ∀ f ∈ ℂ ↑ 𝑝𝑚 s ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x ⊆ V × V
8 7 rgenw ⊢ ∀ s ∈ 𝒫 ℂ ∀ f ∈ ℂ ↑ 𝑝𝑚 s ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x ⊆ V × V
9 df-dv ⊢ D = s ∈ 𝒫 ℂ , f ∈ ℂ ↑ 𝑝𝑚 s ⟼ ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
10 9 ovmptss ⊢ ∀ s ∈ 𝒫 ℂ ∀ f ∈ ℂ ↑ 𝑝𝑚 s ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x ⊆ V × V → S D F ⊆ V × V
11 8 10 ax-mp ⊢ S D F ⊆ V × V
12 df-rel ⊢ Rel ⁡ F S ′ ↔ S D F ⊆ V × V
13 11 12 mpbir ⊢ Rel ⁡ F S ′