Theorem 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 e. _V -> ( F Fn { A } <-> F = { <. A , ( F ` A ) >. } ) )

Proof

Step	Hyp	Ref	Expression
1		fnsnr	|- ( F Fn { A } -> ( x e. F -> x = <. A , ( F ` A ) >. ) )
2	1	adantl	|- ( ( A e. _V /\ F Fn { A } ) -> ( x e. F -> x = <. A , ( F ` A ) >. ) )
3		fnfun	|- ( F Fn { A } -> Fun F )
4		snidg	|- ( A e. _V -> A e. { A } )
5	4	adantr	|- ( ( A e. _V /\ F Fn { A } ) -> A e. { A } )
6		fndm	|- ( F Fn { A } -> dom F = { A } )
7	6	adantl	|- ( ( A e. _V /\ F Fn { A } ) -> dom F = { A } )
8	5 7	eleqtrrd	|- ( ( A e. _V /\ F Fn { A } ) -> A e. dom F )
9		funfvop	|- ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
10	3 8 9	syl2an2	|- ( ( A e. _V /\ F Fn { A } ) -> <. A , ( F ` A ) >. e. F )
11		eleq1	|- ( x = <. A , ( F ` A ) >. -> ( x e. F <-> <. A , ( F ` A ) >. e. F ) )
12	10 11	syl5ibrcom	|- ( ( A e. _V /\ F Fn { A } ) -> ( x = <. A , ( F ` A ) >. -> x e. F ) )
13	2 12	impbid	|- ( ( A e. _V /\ F Fn { A } ) -> ( x e. F <-> x = <. A , ( F ` A ) >. ) )
14		velsn	|- ( x e. { <. A , ( F ` A ) >. } <-> x = <. A , ( F ` A ) >. )
15	13 14	bitr4di	|- ( ( A e. _V /\ F Fn { A } ) -> ( x e. F <-> x e. { <. A , ( F ` A ) >. } ) )
16	15	eqrdv	|- ( ( A e. _V /\ F Fn { A } ) -> F = { <. A , ( F ` A ) >. } )
17	16	ex	|- ( A e. _V -> ( F Fn { A } -> F = { <. A , ( F ` A ) >. } ) )
18		fvex	|- ( F ` A ) e. _V
19		fnsng	|- ( ( A e. _V /\ ( F ` A ) e. _V ) -> { <. A , ( F ` A ) >. } Fn { A } )
20	18 19	mpan2	|- ( A e. _V -> { <. A , ( F ` A ) >. } Fn { A } )
21		fneq1	|- ( F = { <. A , ( F ` A ) >. } -> ( F Fn { A } <-> { <. A , ( F ` A ) >. } Fn { A } ) )
22	20 21	syl5ibrcom	|- ( A e. _V -> ( F = { <. A , ( F ` A ) >. } -> F Fn { A } ) )
23	17 22	impbid	|- ( A e. _V -> ( F Fn { A } <-> F = { <. A , ( F ` A ) >. } ) )