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

Metamath Proof Explorer

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