This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )