Theorem mofsn2

Description: There is at most one function into a singleton. An unconditional variant of mofsn , i.e., the singleton could be empty if Y is a proper class. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mofsn2	⊢ ( 𝐵 = { 𝑌 } → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mofsn	⊢ ( 𝑌 ∈ V → ∃* 𝑓 𝑓 : 𝐴 ⟶ { 𝑌 } )
2	1	adantl	⊢ ( ( 𝐵 = { 𝑌 } ∧ 𝑌 ∈ V ) → ∃* 𝑓 𝑓 : 𝐴 ⟶ { 𝑌 } )
3		feq3	⊢ ( 𝐵 = { 𝑌 } → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑓 : 𝐴 ⟶ { 𝑌 } ) )
4	3	mobidv	⊢ ( 𝐵 = { 𝑌 } → ( ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 ↔ ∃* 𝑓 𝑓 : 𝐴 ⟶ { 𝑌 } ) )
5	4	adantr	⊢ ( ( 𝐵 = { 𝑌 } ∧ 𝑌 ∈ V ) → ( ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 ↔ ∃* 𝑓 𝑓 : 𝐴 ⟶ { 𝑌 } ) )
6	2 5	mpbird	⊢ ( ( 𝐵 = { 𝑌 } ∧ 𝑌 ∈ V ) → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
7		simpl	⊢ ( ( 𝐵 = { 𝑌 } ∧ ¬ 𝑌 ∈ V ) → 𝐵 = { 𝑌 } )
8		snprc	⊢ ( ¬ 𝑌 ∈ V ↔ { 𝑌 } = ∅ )
9	8	biimpi	⊢ ( ¬ 𝑌 ∈ V → { 𝑌 } = ∅ )
10	9	adantl	⊢ ( ( 𝐵 = { 𝑌 } ∧ ¬ 𝑌 ∈ V ) → { 𝑌 } = ∅ )
11	7 10	eqtrd	⊢ ( ( 𝐵 = { 𝑌 } ∧ ¬ 𝑌 ∈ V ) → 𝐵 = ∅ )
12		mof02	⊢ ( 𝐵 = ∅ → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
13	11 12	syl	⊢ ( ( 𝐵 = { 𝑌 } ∧ ¬ 𝑌 ∈ V ) → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
14	6 13	pm2.61dan	⊢ ( 𝐵 = { 𝑌 } → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )