This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsnunf

Description: Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015)

		Ref	Expression
	Assertion	fsnunf	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to (F \cup \{⟨X, Y⟩\}) : S \cup \{X\} ⟶ T$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to F : S ⟶ T$
2		simp2l	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to X \in V$
3		simp3	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to Y \in T$
4		f1osng	$⊢ (X \in V \land Y \in T) \to \{⟨X, Y⟩\} : \{X\} \underset{1-1 onto}{⟶} \{Y\}$
5	2 3 4	syl2anc	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to \{⟨X, Y⟩\} : \{X\} \underset{1-1 onto}{⟶} \{Y\}$
6		f1of	$⊢ \{⟨X, Y⟩\} : \{X\} \underset{1-1 onto}{⟶} \{Y\} \to \{⟨X, Y⟩\} : \{X\} ⟶ \{Y\}$
7	5 6	syl	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to \{⟨X, Y⟩\} : \{X\} ⟶ \{Y\}$
8		simp2r	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to \neg X \in S$
9		disjsn	$⊢ S \cap \{X\} = \emptyset \leftrightarrow \neg X \in S$
10	8 9	sylibr	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to S \cap \{X\} = \emptyset$
11		fun	$⊢ ((F : S ⟶ T \land \{⟨X, Y⟩\} : \{X\} ⟶ \{Y\}) \land S \cap \{X\} = \emptyset) \to (F \cup \{⟨X, Y⟩\}) : S \cup \{X\} ⟶ T \cup \{Y\}$
12	1 7 10 11	syl21anc	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to (F \cup \{⟨X, Y⟩\}) : S \cup \{X\} ⟶ T \cup \{Y\}$
13		snssi	$⊢ Y \in T \to \{Y\} \subseteq T$
14	13	3ad2ant3	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to \{Y\} \subseteq T$
15		ssequn2	$⊢ \{Y\} \subseteq T \leftrightarrow T \cup \{Y\} = T$
16	14 15	sylib	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to T \cup \{Y\} = T$
17	16	feq3d	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to ((F \cup \{⟨X, Y⟩\}) : S \cup \{X\} ⟶ T \cup \{Y\} \leftrightarrow (F \cup \{⟨X, Y⟩\}) : S \cup \{X\} ⟶ T)$
18	12 17	mpbid	$⊢ (F : S ⟶ T \land (X \in V \land \neg X \in S) \land Y \in T) \to (F \cup \{⟨X, Y⟩\}) : S \cup \{X\} ⟶ T$