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

Metamath Proof Explorer

Theorem f1cdmsn

Description: If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton. (Contributed by BTernaryTau, 1-Dec-2024)

		Ref	Expression
	Assertion	f1cdmsn	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land A \neq \emptyset) \to \exists x A = \{x\}$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} \{B\} \to F : A ⟶ \{B\}$
2		fvconst	$⊢ (F : A ⟶ \{B\} \land y \in A) \to F (y) = B$
3	2	3adant3	$⊢ (F : A ⟶ \{B\} \land y \in A \land z \in A) \to F (y) = B$
4		fvconst	$⊢ (F : A ⟶ \{B\} \land z \in A) \to F (z) = B$
5	4	3adant2	$⊢ (F : A ⟶ \{B\} \land y \in A \land z \in A) \to F (z) = B$
6	3 5	eqtr4d	$⊢ (F : A ⟶ \{B\} \land y \in A \land z \in A) \to F (y) = F (z)$
7	1 6	syl3an1	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land y \in A \land z \in A) \to F (y) = F (z)$
8		f1veqaeq	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land (y \in A \land z \in A)) \to (F (y) = F (z) \to y = z)$
9	8	3impb	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land y \in A \land z \in A) \to (F (y) = F (z) \to y = z)$
10	7 9	mpd	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land y \in A \land z \in A) \to y = z$
11	10	3expia	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land y \in A) \to (z \in A \to y = z)$
12	11	ralrimiv	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land y \in A) \to \forall z \in A y = z$
13	12	reximdva0	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land A \neq \emptyset) \to \exists y \in A \forall z \in A y = z$
14		issn	$⊢ \exists y \in A \forall z \in A y = z \to \exists x A = \{x\}$
15	13 14	syl	$⊢ (F : A \underset{1-1}{⟶} \{B\} \land A \neq \emptyset) \to \exists x A = \{x\}$