fconst2g

Description: A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007)

		Ref	Expression
	Assertion	fconst2g	$⊢ B \in C \to (F : A ⟶ \{B\} \leftrightarrow F = A \times \{B\})$

Step	Hyp	Ref	Expression
1		fvconst	$⊢ (F : A ⟶ \{B\} \land x \in A) \to F (x) = B$
2	1	adantlr	$⊢ ((F : A ⟶ \{B\} \land B \in C) \land x \in A) \to F (x) = B$
3		fvconst2g	$⊢ (B \in C \land x \in A) \to (A \times \{B\}) (x) = B$
4	3	adantll	$⊢ ((F : A ⟶ \{B\} \land B \in C) \land x \in A) \to (A \times \{B\}) (x) = B$
5	2 4	eqtr4d	$⊢ ((F : A ⟶ \{B\} \land B \in C) \land x \in A) \to F (x) = (A \times \{B\}) (x)$
6	5	ralrimiva	$⊢ (F : A ⟶ \{B\} \land B \in C) \to \forall x \in A F (x) = (A \times \{B\}) (x)$
7		ffn	$⊢ F : A ⟶ \{B\} \to F Fn A$
8		fnconstg	$⊢ B \in C \to (A \times \{B\}) Fn A$
9		eqfnfv	$⊢ (F Fn A \land (A \times \{B\}) Fn A) \to (F = A \times \{B\} \leftrightarrow \forall x \in A F (x) = (A \times \{B\}) (x))$
10	7 8 9	syl2an	$⊢ (F : A ⟶ \{B\} \land B \in C) \to (F = A \times \{B\} \leftrightarrow \forall x \in A F (x) = (A \times \{B\}) (x))$
11	6 10	mpbird	$⊢ (F : A ⟶ \{B\} \land B \in C) \to F = A \times \{B\}$
12	11	expcom	$⊢ B \in C \to (F : A ⟶ \{B\} \to F = A \times \{B\})$
13		fconstg	$⊢ B \in C \to (A \times \{B\}) : A ⟶ \{B\}$
14		feq1	$⊢ F = A \times \{B\} \to (F : A ⟶ \{B\} \leftrightarrow (A \times \{B\}) : A ⟶ \{B\})$
15	13 14	syl5ibrcom	$⊢ B \in C \to (F = A \times \{B\} \to F : A ⟶ \{B\})$
16	12 15	impbid	$⊢ B \in C \to (F : A ⟶ \{B\} \leftrightarrow F = A \times \{B\})$

Metamath Proof Explorer