Theorem fconstg

Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004)

	Ref	Expression
Assertion	fconstg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑥 = 𝐵 → { 𝑥 } = { 𝐵 } )
2	1	xpeq2d	⊢ ( 𝑥 = 𝐵 → ( 𝐴 × { 𝑥 } ) = ( 𝐴 × { 𝐵 } ) )
3		feq1	⊢ ( ( 𝐴 × { 𝑥 } ) = ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } ↔ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝑥 } ) )
4		feq3	⊢ ( { 𝑥 } = { 𝐵 } → ( ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝑥 } ↔ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } ) )
5	3 4	sylan9bb	⊢ ( ( ( 𝐴 × { 𝑥 } ) = ( 𝐴 × { 𝐵 } ) ∧ { 𝑥 } = { 𝐵 } ) → ( ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } ↔ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } ) )
6	2 1 5	syl2anc	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } ↔ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } ) )
7		vex	⊢ 𝑥 ∈ V
8	7	fconst	⊢ ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 }
9	6 8	vtoclg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } )