Metamath Proof Explorer

Theorem dvnbss

Description: The set of N-times differentiable points is a subset of the domain of the function. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to dom (S D^{n} F) (N) \subseteq dom F$

Proof

Step	Hyp	Ref	Expression
1		dvnff	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) : ℕ_{0} ⟶ ℂ ↑_{𝑝𝑚} dom F$
2	1	ffvelrnda	$⊢ ((S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S)) \land N \in ℕ_{0}) \to (S D^{n} F) (N) \in (ℂ ↑_{𝑝𝑚} dom F)$
3	2	3impa	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to (S D^{n} F) (N) \in (ℂ ↑_{𝑝𝑚} dom F)$
4		cnex	$⊢ ℂ \in V$
5		simp2	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to F \in (ℂ ↑_{𝑝𝑚} S)$
6	5	dmexd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to dom F \in V$
7		elpm2g	$⊢ (ℂ \in V \land dom F \in V) \to ((S D^{n} F) (N) \in (ℂ ↑_{𝑝𝑚} dom F) \leftrightarrow ((S D^{n} F) (N) : dom (S D^{n} F) (N) ⟶ ℂ \land dom (S D^{n} F) (N) \subseteq dom F))$
8	4 6 7	sylancr	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to ((S D^{n} F) (N) \in (ℂ ↑_{𝑝𝑚} dom F) \leftrightarrow ((S D^{n} F) (N) : dom (S D^{n} F) (N) ⟶ ℂ \land dom (S D^{n} F) (N) \subseteq dom F))$
9	3 8	mpbid	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to ((S D^{n} F) (N) : dom (S D^{n} F) (N) ⟶ ℂ \land dom (S D^{n} F) (N) \subseteq dom F)$
10	9	simprd	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to dom (S D^{n} F) (N) \subseteq dom F$