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