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

Metamath Proof Explorer

Theorem fnsnbg

Description: A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023) Relax condition for being in the universal class. (Revised by Zhi Wang, 21-Oct-2025)

Ref Expression
Assertion fnsnbg ( 𝐴 ∈ 𝑉 → ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )

Proof

Step Hyp Ref Expression
1 fnsnr ⊢ ( 𝐹 Fn { 𝐴 } → ( 𝑥 ∈ 𝐹 → 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) )
2 1 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ( 𝑥 ∈ 𝐹 → 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) )
3 fnfun ⊢ ( 𝐹 Fn { 𝐴 } → Fun 𝐹 )
4 snidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
5 4 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → 𝐴 ∈ { 𝐴 } )
6 fndm ⊢ ( 𝐹 Fn { 𝐴 } → dom 𝐹 = { 𝐴 } )
7 6 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → dom 𝐹 = { 𝐴 } )
8 5 7 eleqtrrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → 𝐴 ∈ dom 𝐹 )
9 funfvop ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
10 3 8 9 syl2an2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
11 eleq1 ⊢ ( 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ → ( 𝑥 ∈ 𝐹 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
12 10 11 syl5ibrcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ( 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ → 𝑥 ∈ 𝐹 ) )
13 2 12 impbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ( 𝑥 ∈ 𝐹 ↔ 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) )
14 velsn ⊢ ( 𝑥 ∈ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ↔ 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ )
15 13 14 bitr4di ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ( 𝑥 ∈ 𝐹 ↔ 𝑥 ∈ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
16 15 eqrdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
17 16 ex ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 Fn { 𝐴 } → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
18 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
19 fnsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 } )
20 18 19 mpan2 ⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 } )
21 fneq1 ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → ( 𝐹 Fn { 𝐴 } ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 } ) )
22 20 21 syl5ibrcom ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → 𝐹 Fn { 𝐴 } ) )
23 17 22 impbid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )