Metamath Proof Explorer

Theorem onsfi

Description: A surreal ordinal with a finite birthday is a non-negative surreal integer. (Contributed by Scott Fenton, 4-Nov-2025)

Ref Expression
Assertion onsfi 
|- ( ( A e. On_s /\ ( bday ` A ) e. _om ) -> A e. NN0_s )

Proof

Step Hyp Ref Expression
1 risset 
 |-  ( ( bday ` A ) e. _om <-> E. x e. _om x = ( bday ` A ) )
2 eqeq1 
 |-  ( y = z -> ( y = ( bday ` a ) <-> z = ( bday ` a ) ) )
3 2 imbi1d 
 |-  ( y = z -> ( ( y = ( bday ` a ) -> a e. NN0_s ) <-> ( z = ( bday ` a ) -> a e. NN0_s ) ) )
4 3 ralbidv 
 |-  ( y = z -> ( A. a e. On_s ( y = ( bday ` a ) -> a e. NN0_s ) <-> A. a e. On_s ( z = ( bday ` a ) -> a e. NN0_s ) ) )
5 fveq2 
 |-  ( a = b -> ( bday ` a ) = ( bday ` b ) )
6 5 eqeq2d 
 |-  ( a = b -> ( z = ( bday ` a ) <-> z = ( bday ` b ) ) )
7 eleq1 
 |-  ( a = b -> ( a e. NN0_s <-> b e. NN0_s ) )
8 6 7 imbi12d 
 |-  ( a = b -> ( ( z = ( bday ` a ) -> a e. NN0_s ) <-> ( z = ( bday ` b ) -> b e. NN0_s ) ) )
9 8 cbvralvw 
 |-  ( A. a e. On_s ( z = ( bday ` a ) -> a e. NN0_s ) <-> A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) )
10 4 9 bitrdi 
 |-  ( y = z -> ( A. a e. On_s ( y = ( bday ` a ) -> a e. NN0_s ) <-> A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) ) )
11 eqeq1 
 |-  ( y = x -> ( y = ( bday ` a ) <-> x = ( bday ` a ) ) )
12 11 imbi1d 
 |-  ( y = x -> ( ( y = ( bday ` a ) -> a e. NN0_s ) <-> ( x = ( bday ` a ) -> a e. NN0_s ) ) )
13 12 ralbidv 
 |-  ( y = x -> ( A. a e. On_s ( y = ( bday ` a ) -> a e. NN0_s ) <-> A. a e. On_s ( x = ( bday ` a ) -> a e. NN0_s ) ) )
14 onscutlt 
 |-  ( a e. On_s -> a = ( { x e. On_s | x
15 14 3ad2ant3 
 |-  ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) -> a = ( { x e. On_s | x
16 onssno 
 |-  On_s C_ No
17 simp13 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  a e. On_s )
18 16 17 sselid 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  a e. No )
19 sltonold 
 |-  ( a e. No -> { b e. On_s | b
20 18 19 syl 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  { b e. On_s | b
21 breq1 
 |-  ( b = x -> ( b  x
22 simp2 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  x e. On_s )
23 simp3 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  x
24 21 22 23 elrabd 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  x e. { b e. On_s | b
25 20 24 sseldd 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  x e. ( _Old ` ( bday ` a ) ) )
26 bdayelon 
 |-  ( bday ` a ) e. On
27 16 22 sselid 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  x e. No )
28 oldbday 
 |-  ( ( ( bday ` a ) e. On /\ x e. No ) -> ( x e. ( _Old ` ( bday ` a ) ) <-> ( bday ` x ) e. ( bday ` a ) ) )
29 26 27 28 sylancr 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  ( x e. ( _Old ` ( bday ` a ) ) <-> ( bday ` x ) e. ( bday ` a ) ) )
30 25 29 mpbid 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  ( bday ` x ) e. ( bday ` a ) )
31 fveq2 
 |-  ( b = x -> ( bday ` b ) = ( bday ` x ) )
32 31 eleq1d 
 |-  ( b = x -> ( ( bday ` b ) e. ( bday ` a ) <-> ( bday ` x ) e. ( bday ` a ) ) )
33 eleq1 
 |-  ( b = x -> ( b e. NN0_s <-> x e. NN0_s ) )
34 32 33 imbi12d 
 |-  ( b = x -> ( ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) <-> ( ( bday ` x ) e. ( bday ` a ) -> x e. NN0_s ) ) )
35 simp12 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) )
36 34 35 22 rspcdva 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  ( ( bday ` x ) e. ( bday ` a ) -> x e. NN0_s ) )
37 30 36 mpd 
 |-  ( ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) /\ x e. On_s /\ x  x e. NN0_s )
38 37 rabssdv 
 |-  ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) -> { x e. On_s | x
39 oldfi 
 |-  ( ( bday ` a ) e. _om -> ( _Old ` ( bday ` a ) ) e. Fin )
40 39 3ad2ant1 
 |-  ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) -> ( _Old ` ( bday ` a ) ) e. Fin )
41 onsno 
 |-  ( a e. On_s -> a e. No )
42 41 3ad2ant3 
 |-  ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) -> a e. No )
43 sltonold 
 |-  ( a e. No -> { x e. On_s | x
44 42 43 syl 
 |-  ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) -> { x e. On_s | x
45 40 44 ssfid 
 |-  ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) -> { x e. On_s | x
46 n0sfincut 
 |-  ( ( { x e. On_s | x  ( { x e. On_s | x
47 38 45 46 syl2anc 
 |-  ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) -> ( { x e. On_s | x
48 15 47 eqeltrd 
 |-  ( ( ( bday ` a ) e. _om /\ A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) /\ a e. On_s ) -> a e. NN0_s )
49 48 3exp 
 |-  ( ( bday ` a ) e. _om -> ( A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) -> ( a e. On_s -> a e. NN0_s ) ) )
50 eleq1 
 |-  ( y = ( bday ` a ) -> ( y e. _om <-> ( bday ` a ) e. _om ) )
51 raleq 
 |-  ( y = ( bday ` a ) -> ( A. z e. y A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) <-> A. z e. ( bday ` a ) A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) ) )
52 ralcom 
 |-  ( A. z e. ( bday ` a ) A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) <-> A. b e. On_s A. z e. ( bday ` a ) ( z = ( bday ` b ) -> b e. NN0_s ) )
53 df-ral 
 |-  ( A. z e. ( bday ` a ) ( z = ( bday ` b ) -> b e. NN0_s ) <-> A. z ( z e. ( bday ` a ) -> ( z = ( bday ` b ) -> b e. NN0_s ) ) )
54 bi2.04 
 |-  ( ( z e. ( bday ` a ) -> ( z = ( bday ` b ) -> b e. NN0_s ) ) <-> ( z = ( bday ` b ) -> ( z e. ( bday ` a ) -> b e. NN0_s ) ) )
55 54 albii 
 |-  ( A. z ( z e. ( bday ` a ) -> ( z = ( bday ` b ) -> b e. NN0_s ) ) <-> A. z ( z = ( bday ` b ) -> ( z e. ( bday ` a ) -> b e. NN0_s ) ) )
56 fvex 
 |-  ( bday ` b ) e. _V
57 eleq1 
 |-  ( z = ( bday ` b ) -> ( z e. ( bday ` a ) <-> ( bday ` b ) e. ( bday ` a ) ) )
58 57 imbi1d 
 |-  ( z = ( bday ` b ) -> ( ( z e. ( bday ` a ) -> b e. NN0_s ) <-> ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) ) )
59 56 58 ceqsalv 
 |-  ( A. z ( z = ( bday ` b ) -> ( z e. ( bday ` a ) -> b e. NN0_s ) ) <-> ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) )
60 53 55 59 3bitri 
 |-  ( A. z e. ( bday ` a ) ( z = ( bday ` b ) -> b e. NN0_s ) <-> ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) )
61 60 ralbii 
 |-  ( A. b e. On_s A. z e. ( bday ` a ) ( z = ( bday ` b ) -> b e. NN0_s ) <-> A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) )
62 52 61 bitri 
 |-  ( A. z e. ( bday ` a ) A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) <-> A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) )
63 51 62 bitrdi 
 |-  ( y = ( bday ` a ) -> ( A. z e. y A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) <-> A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) ) )
64 63 imbi1d 
 |-  ( y = ( bday ` a ) -> ( ( A. z e. y A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) -> ( a e. On_s -> a e. NN0_s ) ) <-> ( A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) -> ( a e. On_s -> a e. NN0_s ) ) ) )
65 50 64 imbi12d 
 |-  ( y = ( bday ` a ) -> ( ( y e. _om -> ( A. z e. y A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) -> ( a e. On_s -> a e. NN0_s ) ) ) <-> ( ( bday ` a ) e. _om -> ( A. b e. On_s ( ( bday ` b ) e. ( bday ` a ) -> b e. NN0_s ) -> ( a e. On_s -> a e. NN0_s ) ) ) ) )
66 49 65 mpbiri 
 |-  ( y = ( bday ` a ) -> ( y e. _om -> ( A. z e. y A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) -> ( a e. On_s -> a e. NN0_s ) ) ) )
67 66 com4l 
 |-  ( y e. _om -> ( A. z e. y A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) -> ( a e. On_s -> ( y = ( bday ` a ) -> a e. NN0_s ) ) ) )
68 67 ralrimdv 
 |-  ( y e. _om -> ( A. z e. y A. b e. On_s ( z = ( bday ` b ) -> b e. NN0_s ) -> A. a e. On_s ( y = ( bday ` a ) -> a e. NN0_s ) ) )
69 10 13 68 omsinds 
 |-  ( x e. _om -> A. a e. On_s ( x = ( bday ` a ) -> a e. NN0_s ) )
70 fveq2 
 |-  ( a = A -> ( bday ` a ) = ( bday ` A ) )
71 70 eqeq2d 
 |-  ( a = A -> ( x = ( bday ` a ) <-> x = ( bday ` A ) ) )
72 eleq1 
 |-  ( a = A -> ( a e. NN0_s <-> A e. NN0_s ) )
73 71 72 imbi12d 
 |-  ( a = A -> ( ( x = ( bday ` a ) -> a e. NN0_s ) <-> ( x = ( bday ` A ) -> A e. NN0_s ) ) )
74 73 rspccv 
 |-  ( A. a e. On_s ( x = ( bday ` a ) -> a e. NN0_s ) -> ( A e. On_s -> ( x = ( bday ` A ) -> A e. NN0_s ) ) )
75 69 74 syl 
 |-  ( x e. _om -> ( A e. On_s -> ( x = ( bday ` A ) -> A e. NN0_s ) ) )
76 75 com23 
 |-  ( x e. _om -> ( x = ( bday ` A ) -> ( A e. On_s -> A e. NN0_s ) ) )
77 76 rexlimiv 
 |-  ( E. x e. _om x = ( bday ` A ) -> ( A e. On_s -> A e. NN0_s ) )
78 1 77 sylbi 
 |-  ( ( bday ` A ) e. _om -> ( A e. On_s -> A e. NN0_s ) )
79 78 impcom 
 |-  ( ( A e. On_s /\ ( bday ` A ) e. _om ) -> A e. NN0_s )