Theorem mofmo

Description: There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mofmo	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mo0sn	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 ↔ ( 𝐵 = ∅ ∨ ∃ 𝑦 𝐵 = { 𝑦 } ) )
2		mof02	⊢ ( 𝐵 = ∅ → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
3		mofsn2	⊢ ( 𝐵 = { 𝑦 } → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
4	3	exlimiv	⊢ ( ∃ 𝑦 𝐵 = { 𝑦 } → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
5	2 4	jaoi	⊢ ( ( 𝐵 = ∅ ∨ ∃ 𝑦 𝐵 = { 𝑦 } ) → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
6	1 5	sylbi	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )