Theorem f1omo

Description: There is at most one element in the function value of a constant function whose output is 1o . (An artifact of our function value definition.) Proof could be significantly shortened by fvconstdomi assuming ax-un (see f1omoALT ). (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Hypothesis	f1omo.1	$$⊢\phi \to F=A\times \left\{1_{𝑜}\right\}$$
Assertion	f1omo	$$⊢\phi \to {\exists }^{*}yy\in F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1omo.1	$$⊢\phi \to F=A\times \left\{1_{𝑜}\right\}$$
2		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
3		eqid	$$⊢\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)$$
4	2 3	fvconst0ci	$$⊢\left(\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=\varnothing \vee \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=1_{𝑜}\right)$$
5		mo0	$$⊢\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=\varnothing \to {\exists }^{*}yy\in \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)$$
6		el1o	$$⊢y\in 1_{𝑜}\leftrightarrow y=\varnothing$$
7		el1o	$$⊢x\in 1_{𝑜}\leftrightarrow x=\varnothing$$
8		eqtr3	$$⊢\left(y=\varnothing \wedge x=\varnothing \right)\to y=x$$
9	6 7 8	syl2anb	$$⊢\left(y\in 1_{𝑜}\wedge x\in 1_{𝑜}\right)\to y=x$$
10	9	gen2	$$⊢\forall y\forall x\left(\left(y\in 1_{𝑜}\wedge x\in 1_{𝑜}\right)\to y=x\right)$$
11		eleq1w	$$⊢y=x\to \left(y\in 1_{𝑜}\leftrightarrow x\in 1_{𝑜}\right)$$
12	11	mo4	$$⊢{\exists }^{*}yy\in 1_{𝑜}\leftrightarrow \forall y\forall x\left(\left(y\in 1_{𝑜}\wedge x\in 1_{𝑜}\right)\to y=x\right)$$
13	10 12	mpbir	$$⊢{\exists }^{*}yy\in 1_{𝑜}$$
14		eleq2w2	$$⊢\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=1_{𝑜}\to \left(y\in \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)\leftrightarrow y\in 1_{𝑜}\right)$$
15	14	mobidv	$$⊢\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=1_{𝑜}\to \left({\exists }^{*}yy\in \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)\leftrightarrow {\exists }^{*}yy\in 1_{𝑜}\right)$$
16	13 15	mpbiri	$$⊢\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=1_{𝑜}\to {\exists }^{*}yy\in \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)$$
17	5 16	jaoi	$$⊢\left(\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=\varnothing \vee \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)=1_{𝑜}\right)\to {\exists }^{*}yy\in \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)$$
18	4 17	ax-mp	$$⊢{\exists }^{*}yy\in \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)$$
19	1	fveq1d	$$⊢\phi \to F\left(X\right)=\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)$$
20	19	eleq2d	$$⊢\phi \to \left(y\in F\left(X\right)\leftrightarrow y\in \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)\right)$$
21	20	mobidv	$$⊢\phi \to \left({\exists }^{*}yy\in F\left(X\right)\leftrightarrow {\exists }^{*}yy\in \left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)\right)$$
22	18 21	mpbiri	$$⊢\phi \to {\exists }^{*}yy\in F\left(X\right)$$