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	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
	bdayfinbnd.2	$$⊢\phi \to Z\in \mathrm{No}$$
	bdayfinbnd.3	$$⊢\phi \to \mathrm{bday}\left(Z\right)\subseteq \mathrm{bday}\left(N\right)$$
	bdayfinbnd.4	$$⊢\phi \to 0_s{\le }_{s}Z$$
Assertion	bdayfinbnd	Could not format assertion : No typesetting found for |- ( 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	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
2		bdayfinbnd.2	$$⊢\phi \to Z\in \mathrm{No}$$
3		bdayfinbnd.3	$$⊢\phi \to \mathrm{bday}\left(Z\right)\subseteq \mathrm{bday}\left(N\right)$$
4		bdayfinbnd.4	$$⊢\phi \to 0_s{\le }_{s}Z$$
5		fveq2	$$⊢z=Z\to \mathrm{bday}\left(z\right)=\mathrm{bday}\left(Z\right)$$
6	5	sseq1d	$$⊢z=Z\to \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(N\right)\leftrightarrow \mathrm{bday}\left(Z\right)\subseteq \mathrm{bday}\left(N\right)\right)$$
7		breq2	$$⊢z=Z\to \left(0_s{\le }_{s}z\leftrightarrow 0_s{\le }_{s}Z\right)$$
8	6 7	anbi12d	$$⊢z=Z\to \left(\left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(N\right)\wedge 0_s{\le }_{s}z\right)\leftrightarrow \left(\mathrm{bday}\left(Z\right)\subseteq \mathrm{bday}\left(N\right)\wedge 0_s{\le }_{s}Z\right)\right)$$
9		eqeq1	$$⊢z=Z\to \left(z=N\leftrightarrow Z=N\right)$$
10		eqeq1	Could not format ( z = Z -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> Z = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( z = Z -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> Z = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
11	10	3anbi1d	Could not format ( z = Z -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( Z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
12	11	rexbidv	Could not format ( 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 ( 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	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( ( ( ( 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	Could not format ( 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 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	Could not format ( 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 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	Could not format ( 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 ( ( ( 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	Could not format ( 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 ( 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