Theorem fconst7

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	fconst7.p	$$⊢Ⅎx\phi$$
	fconst7.x	$$⊢\underset{\_}{Ⅎ}xF$$
	fconst7.f	$$⊢\phi \to FFnA$$
	fconst7.b	$$⊢\phi \to B\in V$$
	fconst7.e	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=B$$
Assertion	fconst7	$$⊢\phi \to F=A\times \left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fconst7.p	$$⊢Ⅎx\phi$$
2		fconst7.x	$$⊢\underset{\_}{Ⅎ}xF$$
3		fconst7.f	$$⊢\phi \to FFnA$$
4		fconst7.b	$$⊢\phi \to B\in V$$
5		fconst7.e	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=B$$
6		fvexd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in \mathrm{V}$$
7	5 6	eqeltrrd	$$⊢\left(\phi \wedge x\in A\right)\to B\in \mathrm{V}$$
8		snidg	$$⊢B\in \mathrm{V}\to B\in \left\{B\right\}$$
9	7 8	syl	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left\{B\right\}$$
10	5 9	eqeltrd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in \left\{B\right\}$$
11	1 10	ralrimia	$$⊢\phi \to \forall x\in AF\left(x\right)\in \left\{B\right\}$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{B\right\}$$
14	12 13 2	ffnfvf	$$⊢F:A⟶\left\{B\right\}\leftrightarrow \left(FFnA\wedge \forall x\in AF\left(x\right)\in \left\{B\right\}\right)$$
15	3 11 14	sylanbrc	$$⊢\phi \to F:A⟶\left\{B\right\}$$
16		fconst2g	$$⊢B\in V\to \left(F:A⟶\left\{B\right\}\leftrightarrow F=A\times \left\{B\right\}\right)$$
17	4 16	syl	$$⊢\phi \to \left(F:A⟶\left\{B\right\}\leftrightarrow F=A\times \left\{B\right\}\right)$$
18	15 17	mpbid	$$⊢\phi \to F=A\times \left\{B\right\}$$