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) (Proof shortened by SN, 24-Nov-2025)

	Ref	Expression
Hypothesis	f1omo.1	|- ( ph -> F = ( A X. { 1o } ) )
Assertion	f1omo	|- ( ph -> E* y y e. ( F ` X ) )

Proof

Step	Hyp	Ref	Expression
1		f1omo.1	|- ( ph -> F = ( A X. { 1o } ) )
2		1oex	|- 1o e. _V
3		eqid	|- ( ( A X. { 1o } ) ` X ) = ( ( A X. { 1o } ) ` X )
4	2 3	fvconst0ci	|- ( ( ( A X. { 1o } ) ` X ) = (/) \/ ( ( A X. { 1o } ) ` X ) = 1o )
5		mo0	|- ( ( ( A X. { 1o } ) ` X ) = (/) -> E* y y e. ( ( A X. { 1o } ) ` X ) )
6		df1o2	|- 1o = { (/) }
7	6	eqeq2i	|- ( ( ( A X. { 1o } ) ` X ) = 1o <-> ( ( A X. { 1o } ) ` X ) = { (/) } )
8		mosn	|- ( ( ( A X. { 1o } ) ` X ) = { (/) } -> E* y y e. ( ( A X. { 1o } ) ` X ) )
9	7 8	sylbi	|- ( ( ( A X. { 1o } ) ` X ) = 1o -> E* y y e. ( ( A X. { 1o } ) ` X ) )
10	5 9	jaoi	|- ( ( ( ( A X. { 1o } ) ` X ) = (/) \/ ( ( A X. { 1o } ) ` X ) = 1o ) -> E* y y e. ( ( A X. { 1o } ) ` X ) )
11	4 10	ax-mp	|- E* y y e. ( ( A X. { 1o } ) ` X )
12	1	fveq1d	|- ( ph -> ( F ` X ) = ( ( A X. { 1o } ) ` X ) )
13	12	eleq2d	|- ( ph -> ( y e. ( F ` X ) <-> y e. ( ( A X. { 1o } ) ` X ) ) )
14	13	mobidv	|- ( ph -> ( E* y y e. ( F ` X ) <-> E* y y e. ( ( A X. { 1o } ) ` X ) ) )
15	11 14	mpbiri	|- ( ph -> E* y y e. ( F ` X ) )