Theorem mofeu

Description: The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	mofeu.1	$$⊢G=A\times B$$
	mofeu.2	$$⊢\phi \to \left(B=\varnothing \to A=\varnothing \right)$$
	mofeu.3	$$⊢\phi \to {\exists }^{*}xx\in B$$
Assertion	mofeu	$$⊢\phi \to \left(F:A⟶B\leftrightarrow F=G\right)$$

Proof

Step	Hyp	Ref	Expression
1		mofeu.1	$$⊢G=A\times B$$
2		mofeu.2	$$⊢\phi \to \left(B=\varnothing \to A=\varnothing \right)$$
3		mofeu.3	$$⊢\phi \to {\exists }^{*}xx\in B$$
4	2	imp	$$⊢\left(\phi \wedge B=\varnothing \right)\to A=\varnothing$$
5		f00	$$⊢F:A⟶\varnothing \leftrightarrow \left(F=\varnothing \wedge A=\varnothing \right)$$
6	5	rbaib	$$⊢A=\varnothing \to \left(F:A⟶\varnothing \leftrightarrow F=\varnothing \right)$$
7	4 6	syl	$$⊢\left(\phi \wedge B=\varnothing \right)\to \left(F:A⟶\varnothing \leftrightarrow F=\varnothing \right)$$
8		feq3	$$⊢B=\varnothing \to \left(F:A⟶B\leftrightarrow F:A⟶\varnothing \right)$$
9	8	adantl	$$⊢\left(\phi \wedge B=\varnothing \right)\to \left(F:A⟶B\leftrightarrow F:A⟶\varnothing \right)$$
10		xpeq2	$$⊢B=\varnothing \to A\times B=A\times \varnothing$$
11		xp0	$$⊢A\times \varnothing =\varnothing$$
12	10 11	eqtrdi	$$⊢B=\varnothing \to A\times B=\varnothing$$
13	1 12	syl5eq	$$⊢B=\varnothing \to G=\varnothing$$
14	13	adantl	$$⊢\left(\phi \wedge B=\varnothing \right)\to G=\varnothing$$
15	14	eqeq2d	$$⊢\left(\phi \wedge B=\varnothing \right)\to \left(F=G\leftrightarrow F=\varnothing \right)$$
16	7 9 15	3bitr4d	$$⊢\left(\phi \wedge B=\varnothing \right)\to \left(F:A⟶B\leftrightarrow F=G\right)$$
17		19.42v	$$⊢\exists y\left(\phi \wedge B=\left\{y\right\}\right)\leftrightarrow \left(\phi \wedge \exists yB=\left\{y\right\}\right)$$
18		fconst2g	$$⊢y\in \mathrm{V}\to \left(F:A⟶\left\{y\right\}\leftrightarrow F=A\times \left\{y\right\}\right)$$
19	18	elv	$$⊢F:A⟶\left\{y\right\}\leftrightarrow F=A\times \left\{y\right\}$$
20		feq3	$$⊢B=\left\{y\right\}\to \left(F:A⟶B\leftrightarrow F:A⟶\left\{y\right\}\right)$$
21		xpeq2	$$⊢B=\left\{y\right\}\to A\times B=A\times \left\{y\right\}$$
22	21	eqeq2d	$$⊢B=\left\{y\right\}\to \left(F=A\times B\leftrightarrow F=A\times \left\{y\right\}\right)$$
23	20 22	bibi12d	$$⊢B=\left\{y\right\}\to \left(\left(F:A⟶B\leftrightarrow F=A\times B\right)\leftrightarrow \left(F:A⟶\left\{y\right\}\leftrightarrow F=A\times \left\{y\right\}\right)\right)$$
24	19 23	mpbiri	$$⊢B=\left\{y\right\}\to \left(F:A⟶B\leftrightarrow F=A\times B\right)$$
25	1	eqeq2i	$$⊢F=G\leftrightarrow F=A\times B$$
26	24 25	bitr4di	$$⊢B=\left\{y\right\}\to \left(F:A⟶B\leftrightarrow F=G\right)$$
27	26	adantl	$$⊢\left(\phi \wedge B=\left\{y\right\}\right)\to \left(F:A⟶B\leftrightarrow F=G\right)$$
28	27	exlimiv	$$⊢\exists y\left(\phi \wedge B=\left\{y\right\}\right)\to \left(F:A⟶B\leftrightarrow F=G\right)$$
29	17 28	sylbir	$$⊢\left(\phi \wedge \exists yB=\left\{y\right\}\right)\to \left(F:A⟶B\leftrightarrow F=G\right)$$
30		mo0sn	$$⊢{\exists }^{*}xx\in B\leftrightarrow \left(B=\varnothing \vee \exists yB=\left\{y\right\}\right)$$
31	3 30	sylib	$$⊢\phi \to \left(B=\varnothing \vee \exists yB=\left\{y\right\}\right)$$
32	16 29 31	mpjaodan	$$⊢\phi \to \left(F:A⟶B\leftrightarrow F=G\right)$$