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

Metamath Proof Explorer

Theorem mofsn

Description: There is at most one function into a singleton, with fewer axioms than eufsn and eufsn2 . See also mofsn2 . (Contributed by Zhi Wang, 19-Sep-2024)

		Ref	Expression
	Assertion	mofsn	$⊢ B \in V \to \exists^{*} f f : A ⟶ \{B\}$

Proof

Step	Hyp	Ref	Expression
1		fconst2g	$⊢ B \in V \to (f : A ⟶ \{B\} \leftrightarrow f = A \times \{B\})$
2	1	biimpd	$⊢ B \in V \to (f : A ⟶ \{B\} \to f = A \times \{B\})$
3		fconst2g	$⊢ B \in V \to (g : A ⟶ \{B\} \leftrightarrow g = A \times \{B\})$
4	3	biimpd	$⊢ B \in V \to (g : A ⟶ \{B\} \to g = A \times \{B\})$
5		eqtr3	$⊢ (f = A \times \{B\} \land g = A \times \{B\}) \to f = g$
6	5	a1i	$⊢ B \in V \to ((f = A \times \{B\} \land g = A \times \{B\}) \to f = g)$
7	2 4 6	syl2and	$⊢ B \in V \to ((f : A ⟶ \{B\} \land g : A ⟶ \{B\}) \to f = g)$
8	7	alrimivv	$⊢ B \in V \to \forall f \forall g ((f : A ⟶ \{B\} \land g : A ⟶ \{B\}) \to f = g)$
9		feq1	$⊢ f = g \to (f : A ⟶ \{B\} \leftrightarrow g : A ⟶ \{B\})$
10	9	mo4	$⊢ \exists^{*} f f : A ⟶ \{B\} \leftrightarrow \forall f \forall g ((f : A ⟶ \{B\} \land g : A ⟶ \{B\}) \to f = g)$
11	8 10	sylibr	$⊢ B \in V \to \exists^{*} f f : A ⟶ \{B\}$