Theorem bdayfinbnd

Description: Given a non-negative integer and a non-negative surreal of lesser or equal birthday, show that the surreal can be expressed as a dyadic fraction with an upper bound on the integer and exponent. This proof follows the proof from Mizar at https://mizar.uwb.edu.pl/version/current/html/surrealn.html . (Contributed by Scott Fenton, 26-Feb-2026)

	Ref	Expression
Hypotheses	bdayfinbnd.1	|- ( ph -> N e. NN0_s )
	bdayfinbnd.2	|- ( ph -> Z e. No )
	bdayfinbnd.3	|- ( ph -> ( bday ` Z ) C_ ( bday ` N ) )
	bdayfinbnd.4	|- ( ph -> 0s <_s Z )
Assertion	bdayfinbnd	|- ( ph -> ( Z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y

Proof

Step	Hyp	Ref	Expression
1		bdayfinbnd.1	|- ( ph -> N e. NN0_s )
2		bdayfinbnd.2	|- ( ph -> Z e. No )
3		bdayfinbnd.3	|- ( ph -> ( bday ` Z ) C_ ( bday ` N ) )
4		bdayfinbnd.4	|- ( ph -> 0s <_s Z )
5		fveq2	|- ( z = Z -> ( bday ` z ) = ( bday ` Z ) )
6	5	sseq1d	|- ( z = Z -> ( ( bday ` z ) C_ ( bday ` N ) <-> ( bday ` Z ) C_ ( bday ` N ) ) )
7		breq2	|- ( z = Z -> ( 0s <_s z <-> 0s <_s Z ) )
8	6 7	anbi12d	|- ( z = Z -> ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) <-> ( ( bday ` Z ) C_ ( bday ` N ) /\ 0s <_s Z ) ) )
9		eqeq1	|- ( z = Z -> ( z = N <-> Z = N ) )
10		eqeq1	|- ( z = Z -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> Z = ( x +s ( y /su ( 2s ^su p ) ) ) ) )
11	10	3anbi1d	|- ( z = Z -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
12	11	rexbidv	|- ( z = Z -> ( E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. p e. NN0_s ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
13	12	2rexbidv	|- ( z = Z -> ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
14	9 13	orbi12d	|- ( z = Z -> ( ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( Z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
15	8 14	imbi12d	|- ( z = Z -> ( ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) -> ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( ( bday ` Z ) C_ ( bday ` N ) /\ 0s <_s Z ) -> ( Z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
16		bdayfinbndlem2	|- ( N e. NN0_s -> A. z e. No ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) -> ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
17	1 16	syl	|- ( ph -> A. z e. No ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) -> ( z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
18	15 17 2	rspcdva	|- ( ph -> ( ( ( bday ` Z ) C_ ( bday ` N ) /\ 0s <_s Z ) -> ( Z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
19	3 4 18	mp2and	|- ( ph -> ( Z = N \/ E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y