Metamath Proof Explorer


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 V F Fn A F = A F A

Proof

Step Hyp Ref Expression
1 fnsnr F Fn A x F x = A F A
2 1 adantl A V F Fn A x F x = A F A
3 fnfun F Fn A Fun F
4 snidg A V A A
5 4 adantr A V F Fn A A A
6 fndm F Fn A dom F = A
7 6 adantl A V F Fn A dom F = A
8 5 7 eleqtrrd A V F Fn A A dom F
9 funfvop Fun F A dom F A F A F
10 3 8 9 syl2an2 A V F Fn A A F A F
11 eleq1 x = A F A x F A F A F
12 10 11 syl5ibrcom A V F Fn A x = A F A x F
13 2 12 impbid A V F Fn A x F x = A F A
14 velsn x A F A x = A F A
15 13 14 bitr4di A V F Fn A x F x A F A
16 15 eqrdv A V F Fn A F = A F A
17 16 ex A V F Fn A F = A F A
18 fvex F A V
19 fnsng A V F A V A F A Fn A
20 18 19 mpan2 A 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 V F = A F A F Fn A
23 17 22 impbid A V F Fn A F = A F A