Theorem f1omoALT

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.) Use f1omo without assuming ax-un . (Contributed by Zhi Wang, 18-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		f1omoALT.1	$$⊢\phi \to F=A\times \left\{1_{𝑜}\right\}$$
2	1	fveq1d	$$⊢\phi \to F\left(X\right)=\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)$$
3		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
4	3	fvconstdomi	$$⊢\left(A\times \left\{1_{𝑜}\right\}\right)\left(X\right)\preccurlyeq 1_{𝑜}$$
5	2 4	eqbrtrdi	$$⊢\phi \to F\left(X\right)\preccurlyeq 1_{𝑜}$$
6		modom2	$$⊢{\exists }^{*}yy\in F\left(X\right)\leftrightarrow F\left(X\right)\preccurlyeq 1_{𝑜}$$
7	5 6	sylibr	$$⊢\phi \to {\exists }^{*}yy\in F\left(X\right)$$