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	|- ( 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		el1o	|- ( y e. 1o <-> y = (/) )
7		el1o	|- ( x e. 1o <-> x = (/) )
8		eqtr3	|- ( ( y = (/) /\ x = (/) ) -> y = x )
9	6 7 8	syl2anb	|- ( ( y e. 1o /\ x e. 1o ) -> y = x )
10	9	gen2	|- A. y A. x ( ( y e. 1o /\ x e. 1o ) -> y = x )
11		eleq1w	|- ( y = x -> ( y e. 1o <-> x e. 1o ) )
12	11	mo4	|- ( E* y y e. 1o <-> A. y A. x ( ( y e. 1o /\ x e. 1o ) -> y = x ) )
13	10 12	mpbir	|- E* y y e. 1o
14		eleq2w2	|- ( ( ( A X. { 1o } ) ` X ) = 1o -> ( y e. ( ( A X. { 1o } ) ` X ) <-> y e. 1o ) )
15	14	mobidv	|- ( ( ( A X. { 1o } ) ` X ) = 1o -> ( E* y y e. ( ( A X. { 1o } ) ` X ) <-> E* y y e. 1o ) )
16	13 15	mpbiri	|- ( ( ( A X. { 1o } ) ` X ) = 1o -> E* y y e. ( ( A X. { 1o } ) ` X ) )
17	5 16	jaoi	|- ( ( ( ( A X. { 1o } ) ` X ) = (/) \/ ( ( A X. { 1o } ) ` X ) = 1o ) -> E* y y e. ( ( A X. { 1o } ) ` X ) )
18	4 17	ax-mp	|- E* y y e. ( ( A X. { 1o } ) ` X )
19	1	fveq1d	|- ( ph -> ( F ` X ) = ( ( A X. { 1o } ) ` X ) )
20	19	eleq2d	|- ( ph -> ( y e. ( F ` X ) <-> y e. ( ( A X. { 1o } ) ` X ) ) )
21	20	mobidv	|- ( ph -> ( E* y y e. ( F ` X ) <-> E* y y e. ( ( A X. { 1o } ) ` X ) ) )
22	18 21	mpbiri	|- ( ph -> E* y y e. ( F ` X ) )