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

Metamath Proof Explorer

Theorem eufsnlem

Description: There is exactly one function into a singleton. For a simpler hypothesis, see eufsn assuming ax-rep , or eufsn2 assuming ax-pow and ax-un . (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Hypotheses eufsn.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
eufsnlem.2 ⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) ∈ 𝑉 )
Assertion eufsnlem ( 𝜑 → ∃! 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } )

Proof

Step Hyp Ref Expression
1 eufsn.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
2 eufsnlem.2 ⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) ∈ 𝑉 )
3 fconst2g ⊢ ( 𝐵 ∈ 𝑊 → ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = ( 𝐴 × { 𝐵 } ) ) )
4 1 3 syl ⊢ ( 𝜑 → ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = ( 𝐴 × { 𝐵 } ) ) )
5 4 alrimiv ⊢ ( 𝜑 → ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = ( 𝐴 × { 𝐵 } ) ) )
6 eqeq2 ⊢ ( 𝑔 = ( 𝐴 × { 𝐵 } ) → ( 𝑓 = 𝑔 ↔ 𝑓 = ( 𝐴 × { 𝐵 } ) ) )
7 6 bibi2d ⊢ ( 𝑔 = ( 𝐴 × { 𝐵 } ) → ( ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = 𝑔 ) ↔ ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = ( 𝐴 × { 𝐵 } ) ) ) )
8 7 albidv ⊢ ( 𝑔 = ( 𝐴 × { 𝐵 } ) → ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = 𝑔 ) ↔ ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = ( 𝐴 × { 𝐵 } ) ) ) )
9 2 5 8 spcedv ⊢ ( 𝜑 → ∃ 𝑔 ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = 𝑔 ) )
10 eu6im ⊢ ( ∃ 𝑔 ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ { 𝐵 } ↔ 𝑓 = 𝑔 ) → ∃! 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } )
11 9 10 syl ⊢ ( 𝜑 → ∃! 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } )