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

Metamath Proof Explorer

Theorem f1omoOLD

Description: Obsolete version of f1omo as of 24-Nov-2025. (Contributed by Zhi Wang, 19-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis f1omo.1 
|- ( ph -> F = ( A X. { 1o } ) )
Assertion f1omoOLD 
|- ( 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 ) )