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

Metamath Proof Explorer

Theorem mofsn

Description: There is at most one function into a singleton, with fewer axioms than eufsn and eufsn2 . See also mofsn2 . (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion mofsn ( 𝐵 ∈ 𝑉 → ∃* 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } )

Proof

Step Hyp Ref Expression
1 fconst2g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = ( 𝐴 × { 𝐵 } ) ) )
2 1 biimpd ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑓 : 𝐴 ⟶ { 𝐵 } → 𝑓 = ( 𝐴 × { 𝐵 } ) ) )
3 fconst2g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑔 : 𝐴 ⟶ { 𝐵 } ↔ 𝑔 = ( 𝐴 × { 𝐵 } ) ) )
4 3 biimpd ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑔 : 𝐴 ⟶ { 𝐵 } → 𝑔 = ( 𝐴 × { 𝐵 } ) ) )
5 eqtr3 ⊢ ( ( 𝑓 = ( 𝐴 × { 𝐵 } ) ∧ 𝑔 = ( 𝐴 × { 𝐵 } ) ) → 𝑓 = 𝑔 )
6 5 a1i ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑓 = ( 𝐴 × { 𝐵 } ) ∧ 𝑔 = ( 𝐴 × { 𝐵 } ) ) → 𝑓 = 𝑔 ) )
7 2 4 6 syl2and ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑓 : 𝐴 ⟶ { 𝐵 } ∧ 𝑔 : 𝐴 ⟶ { 𝐵 } ) → 𝑓 = 𝑔 ) )
8 7 alrimivv ⊢ ( 𝐵 ∈ 𝑉 → ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 : 𝐴 ⟶ { 𝐵 } ∧ 𝑔 : 𝐴 ⟶ { 𝐵 } ) → 𝑓 = 𝑔 ) )
9 feq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑔 : 𝐴 ⟶ { 𝐵 } ) )
10 9 mo4 ⊢ ( ∃* 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 : 𝐴 ⟶ { 𝐵 } ∧ 𝑔 : 𝐴 ⟶ { 𝐵 } ) → 𝑓 = 𝑔 ) )
11 8 10 sylibr ⊢ ( 𝐵 ∈ 𝑉 → ∃* 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } )