fconstg

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

		Ref	Expression
	Assertion	fconstg	$⊢ B \in V \to (A \times \{B\}) : A ⟶ \{B\}$

Step	Hyp	Ref	Expression
1		sneq	$⊢ x = B \to \{x\} = \{B\}$
2	1	xpeq2d	$⊢ x = B \to A \times \{x\} = A \times \{B\}$
3		feq1	$⊢ A \times \{x\} = A \times \{B\} \to ((A \times \{x\}) : A ⟶ \{x\} \leftrightarrow (A \times \{B\}) : A ⟶ \{x\})$
4		feq3	$⊢ \{x\} = \{B\} \to ((A \times \{B\}) : A ⟶ \{x\} \leftrightarrow (A \times \{B\}) : A ⟶ \{B\})$
5	3 4	sylan9bb	$⊢ (A \times \{x\} = A \times \{B\} \land \{x\} = \{B\}) \to ((A \times \{x\}) : A ⟶ \{x\} \leftrightarrow (A \times \{B\}) : A ⟶ \{B\})$
6	2 1 5	syl2anc	$⊢ x = B \to ((A \times \{x\}) : A ⟶ \{x\} \leftrightarrow (A \times \{B\}) : A ⟶ \{B\})$
7		vex	$⊢ x \in V$
8	7	fconst	$⊢ (A \times \{x\}) : A ⟶ \{x\}$
9	6 8	vtoclg	$⊢ B \in V \to (A \times \{B\}) : A ⟶ \{B\}$

Metamath Proof Explorer