funressn

Description: A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	funressn	$⊢ Fun F \to {F ↾}_{\{B\}} \subseteq \{⟨B, F (B)⟩\}$

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2		fnressn	$⊢ (F Fn dom F \land B \in dom F) \to {F ↾}_{\{B\}} = \{⟨B, F (B)⟩\}$
3	1 2	sylanb	$⊢ (Fun F \land B \in dom F) \to {F ↾}_{\{B\}} = \{⟨B, F (B)⟩\}$
4		eqimss	$⊢ {F ↾}_{\{B\}} = \{⟨B, F (B)⟩\} \to {F ↾}_{\{B\}} \subseteq \{⟨B, F (B)⟩\}$
5	3 4	syl	$⊢ (Fun F \land B \in dom F) \to {F ↾}_{\{B\}} \subseteq \{⟨B, F (B)⟩\}$
6		disjsn	$⊢ dom F \cap \{B\} = \emptyset \leftrightarrow \neg B \in dom F$
7		fnresdisj	$⊢ F Fn dom F \to (dom F \cap \{B\} = \emptyset \leftrightarrow {F ↾}_{\{B\}} = \emptyset)$
8	1 7	sylbi	$⊢ Fun F \to (dom F \cap \{B\} = \emptyset \leftrightarrow {F ↾}_{\{B\}} = \emptyset)$
9	6 8	bitr3id	$⊢ Fun F \to (\neg B \in dom F \leftrightarrow {F ↾}_{\{B\}} = \emptyset)$
10	9	biimpa	$⊢ (Fun F \land \neg B \in dom F) \to {F ↾}_{\{B\}} = \emptyset$
11		0ss	$⊢ \emptyset \subseteq \{⟨B, F (B)⟩\}$
12	10 11	eqsstrdi	$⊢ (Fun F \land \neg B \in dom F) \to {F ↾}_{\{B\}} \subseteq \{⟨B, F (B)⟩\}$
13	5 12	pm2.61dan	$⊢ Fun F \to {F ↾}_{\{B\}} \subseteq \{⟨B, F (B)⟩\}$

Metamath Proof Explorer