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

Metamath Proof Explorer

Theorem fnsnbOLD

Description: Obsolete version of fnsnb as of 21-Oct-2025. A function whose domain is a singleton can be represented as a singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) Revised to add reverse implication. (Revised by NM, 29-Dec-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis fnsnb.1 ⊢ 𝐴 ∈ V
Assertion fnsnbOLD ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 fnsnb.1 ⊢ 𝐴 ∈ V
2 fnsnr ⊢ ( 𝐹 Fn { 𝐴 } → ( 𝑥 ∈ 𝐹 → 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) )
3 df-fn ⊢ ( 𝐹 Fn { 𝐴 } ↔ ( Fun 𝐹 ∧ dom 𝐹 = { 𝐴 } ) )
4 1 snid ⊢ 𝐴 ∈ { 𝐴 }
5 eleq2 ⊢ ( dom 𝐹 = { 𝐴 } → ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ { 𝐴 } ) )
6 4 5 mpbiri ⊢ ( dom 𝐹 = { 𝐴 } → 𝐴 ∈ dom 𝐹 )
7 6 anim2i ⊢ ( ( Fun 𝐹 ∧ dom 𝐹 = { 𝐴 } ) → ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) )
8 3 7 sylbi ⊢ ( 𝐹 Fn { 𝐴 } → ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) )
9 funfvop ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
10 8 9 syl ⊢ ( 𝐹 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 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
18 1 17 fnsn ⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 }
19 fneq1 ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → ( 𝐹 Fn { 𝐴 } ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 } ) )
20 18 19 mpbiri ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → 𝐹 Fn { 𝐴 } )
21 16 20 impbii ⊢ ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )