Metamath Proof Explorer

Theorem nobdaymin

Description: Any non-empty class of surreals has a birthday-minimal element. (Contributed by Scott Fenton, 11-Dec-2025)

Ref Expression
Assertion nobdaymin 
|- ( ( A C_ No /\ A =/= (/) ) -> E. x e. A ( bday ` x ) = |^| ( bday " A ) )

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( bday " A ) C_ ran bday
2 bdayrn 
 |-  ran bday = On
3 1 2 sseqtri 
 |-  ( bday " A ) C_ On
4 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
5 bdaydm 
 |-  dom bday = No
6 5 sseq2i 
 |-  ( A C_ dom bday <-> A C_ No )
7 bdayfun 
 |-  Fun bday
8 funfvima2 
 |-  ( ( Fun bday /\ A C_ dom bday ) -> ( x e. A -> ( bday ` x ) e. ( bday " A ) ) )
9 7 8 mpan 
 |-  ( A C_ dom bday -> ( x e. A -> ( bday ` x ) e. ( bday " A ) ) )
10 6 9 sylbir 
 |-  ( A C_ No -> ( x e. A -> ( bday ` x ) e. ( bday " A ) ) )
11 ne0i 
 |-  ( ( bday ` x ) e. ( bday " A ) -> ( bday " A ) =/= (/) )
12 10 11 syl6 
 |-  ( A C_ No -> ( x e. A -> ( bday " A ) =/= (/) ) )
13 12 exlimdv 
 |-  ( A C_ No -> ( E. x x e. A -> ( bday " A ) =/= (/) ) )
14 4 13 biimtrid 
 |-  ( A C_ No -> ( A =/= (/) -> ( bday " A ) =/= (/) ) )
15 14 imp 
 |-  ( ( A C_ No /\ A =/= (/) ) -> ( bday " A ) =/= (/) )
16 onint 
 |-  ( ( ( bday " A ) C_ On /\ ( bday " A ) =/= (/) ) -> |^| ( bday " A ) e. ( bday " A ) )
17 3 15 16 sylancr 
 |-  ( ( A C_ No /\ A =/= (/) ) -> |^| ( bday " A ) e. ( bday " A ) )
18 bdayfn 
 |-  bday Fn No
19 fvelimab 
 |-  ( ( bday Fn No /\ A C_ No ) -> ( |^| ( bday " A ) e. ( bday " A ) <-> E. x e. A ( bday ` x ) = |^| ( bday " A ) ) )
20 18 19 mpan 
 |-  ( A C_ No -> ( |^| ( bday " A ) e. ( bday " A ) <-> E. x e. A ( bday ` x ) = |^| ( bday " A ) ) )
21 20 adantr 
 |-  ( ( A C_ No /\ A =/= (/) ) -> ( |^| ( bday " A ) e. ( bday " A ) <-> E. x e. A ( bday ` x ) = |^| ( bday " A ) ) )
22 17 21 mpbid 
 |-  ( ( A C_ No /\ A =/= (/) ) -> E. x e. A ( bday ` x ) = |^| ( bday " A ) )