fnsnbt

Description: A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023)

		Ref	Expression
	Assertion	fnsnbt	$⊢ A \in V \to (F Fn \{A\} \leftrightarrow F = \{⟨A, F (A)⟩\})$

Proof

Step	Hyp	Ref	Expression
1		fnsnr	$⊢ F Fn \{A\} \to (x \in F \to x = ⟨A, F (A)⟩)$
2	1	adantl	$⊢ (A \in V \land F Fn \{A\}) \to (x \in F \to x = ⟨A, F (A)⟩)$
3		fnfun	$⊢ F Fn \{A\} \to Fun F$
4		snidg	$⊢ A \in V \to A \in \{A\}$
5	4	adantr	$⊢ (A \in V \land F Fn \{A\}) \to A \in \{A\}$
6		fndm	$⊢ F Fn \{A\} \to dom F = \{A\}$
7	6	adantl	$⊢ (A \in V \land F Fn \{A\}) \to dom F = \{A\}$
8	5 7	eleqtrrd	$⊢ (A \in V \land F Fn \{A\}) \to A \in dom F$
9		funfvop	$⊢ (Fun F \land A \in dom F) \to ⟨A, F (A)⟩ \in F$
10	3 8 9	syl2an2	$⊢ (A \in V \land F Fn \{A\}) \to ⟨A, F (A)⟩ \in F$
11		eleq1	$⊢ x = ⟨A, F (A)⟩ \to (x \in F \leftrightarrow ⟨A, F (A)⟩ \in F)$
12	10 11	syl5ibrcom	$⊢ (A \in V \land F Fn \{A\}) \to (x = ⟨A, F (A)⟩ \to x \in F)$
13	2 12	impbid	$⊢ (A \in V \land F Fn \{A\}) \to (x \in F \leftrightarrow x = ⟨A, F (A)⟩)$
14		velsn	$⊢ x \in \{⟨A, F (A)⟩\} \leftrightarrow x = ⟨A, F (A)⟩$
15	13 14	bitr4di	$⊢ (A \in V \land F Fn \{A\}) \to (x \in F \leftrightarrow x \in \{⟨A, F (A)⟩\})$
16	15	eqrdv	$⊢ (A \in V \land F Fn \{A\}) \to F = \{⟨A, F (A)⟩\}$
17	16	ex	$⊢ A \in V \to (F Fn \{A\} \to F = \{⟨A, F (A)⟩\})$
18		fvex	$⊢ F (A) \in V$
19		fnsng	$⊢ (A \in V \land F (A) \in V) \to \{⟨A, F (A)⟩\} Fn \{A\}$
20	18 19	mpan2	$⊢ A \in V \to \{⟨A, F (A)⟩\} Fn \{A\}$
21		fneq1	$⊢ F = \{⟨A, F (A)⟩\} \to (F Fn \{A\} \leftrightarrow \{⟨A, F (A)⟩\} Fn \{A\})$
22	20 21	syl5ibrcom	$⊢ A \in V \to (F = \{⟨A, F (A)⟩\} \to F Fn \{A\})$
23	17 22	impbid	$⊢ A \in V \to (F Fn \{A\} \leftrightarrow F = \{⟨A, F (A)⟩\})$

Metamath Proof Explorer

Theorem fnsnbt

Proof