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 | |- ( ph -> F = ( A X. { 1o } ) ) |
|
| Assertion | f1omoALT | |- ( ph -> E* y y e. ( F ` X ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1omoALT.1 | |- ( ph -> F = ( A X. { 1o } ) ) |
|
| 2 | 1 | fveq1d | |- ( ph -> ( F ` X ) = ( ( A X. { 1o } ) ` X ) ) |
| 3 | 1oex | |- 1o e. _V |
|
| 4 | 3 | fvconstdomi | |- ( ( A X. { 1o } ) ` X ) ~<_ 1o |
| 5 | 2 4 | eqbrtrdi | |- ( ph -> ( F ` X ) ~<_ 1o ) |
| 6 | modom2 | |- ( E* y y e. ( F ` X ) <-> ( F ` X ) ~<_ 1o ) |
|
| 7 | 5 6 | sylibr | |- ( ph -> E* y y e. ( F ` X ) ) |