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	⊢ ( 𝐵 ∈ 𝑉 → ∃* 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } )