Theorem fconst7v

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022) Removed hyphotheses as suggested by SN (Revised by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypotheses	fconst7v.f	$$⊢\phi \to FFnA$$
	fconst7v.e	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=B$$
Assertion	fconst7v	$$⊢\phi \to F=A\times \left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fconst7v.f	$$⊢\phi \to FFnA$$
2		fconst7v.e	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=B$$
3		0xp	$$⊢\varnothing \times \left\{B\right\}=\varnothing$$
4	3	a1i	$$⊢\left(\phi \wedge A=\varnothing \right)\to \varnothing \times \left\{B\right\}=\varnothing$$
5		simpr	$$⊢\left(\phi \wedge A=\varnothing \right)\to A=\varnothing$$
6	5	xpeq1d	$$⊢\left(\phi \wedge A=\varnothing \right)\to A\times \left\{B\right\}=\varnothing \times \left\{B\right\}$$
7	1	adantr	$$⊢\left(\phi \wedge A=\varnothing \right)\to FFnA$$
8		fneq2	$$⊢A=\varnothing \to \left(FFnA\leftrightarrow FFn\varnothing \right)$$
9	8	adantl	$$⊢\left(\phi \wedge A=\varnothing \right)\to \left(FFnA\leftrightarrow FFn\varnothing \right)$$
10	7 9	mpbid	$$⊢\left(\phi \wedge A=\varnothing \right)\to FFn\varnothing$$
11		fn0	$$⊢FFn\varnothing \leftrightarrow F=\varnothing$$
12	10 11	sylib	$$⊢\left(\phi \wedge A=\varnothing \right)\to F=\varnothing$$
13	4 6 12	3eqtr4rd	$$⊢\left(\phi \wedge A=\varnothing \right)\to F=A\times \left\{B\right\}$$
14		fvexd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in \mathrm{V}$$
15	2 14	eqeltrrd	$$⊢\left(\phi \wedge x\in A\right)\to B\in \mathrm{V}$$
16		snidg	$$⊢B\in \mathrm{V}\to B\in \left\{B\right\}$$
17	15 16	syl	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left\{B\right\}$$
18	2 17	eqeltrd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in \left\{B\right\}$$
19	18	ralrimiva	$$⊢\phi \to \forall x\in AF\left(x\right)\in \left\{B\right\}$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{B\right\}$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}xF$$
23	20 21 22	ffnfvf	$$⊢F:A⟶\left\{B\right\}\leftrightarrow \left(FFnA\wedge \forall x\in AF\left(x\right)\in \left\{B\right\}\right)$$
24	1 19 23	sylanbrc	$$⊢\phi \to F:A⟶\left\{B\right\}$$
25	24	adantr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to F:A⟶\left\{B\right\}$$
26		simpr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to A\ne \varnothing$$
27	15	adantlr	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge x\in A\right)\to B\in \mathrm{V}$$
28	26 27	n0limd	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to B\in \mathrm{V}$$
29		fconst2g	$$⊢B\in \mathrm{V}\to \left(F:A⟶\left\{B\right\}\leftrightarrow F=A\times \left\{B\right\}\right)$$
30	28 29	syl	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to \left(F:A⟶\left\{B\right\}\leftrightarrow F=A\times \left\{B\right\}\right)$$
31	25 30	mpbid	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to F=A\times \left\{B\right\}$$
32		exmidne	$$⊢\left(A=\varnothing \vee A\ne \varnothing \right)$$
33	32	a1i	$$⊢\phi \to \left(A=\varnothing \vee A\ne \varnothing \right)$$
34	13 31 33	mpjaodan	$$⊢\phi \to F=A\times \left\{B\right\}$$