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	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
	bdayfinbnd.2	⊢ ( 𝜑 → 𝑍 ∈ No )
	bdayfinbnd.3	⊢ ( 𝜑 → ( bday ‘ 𝑍 ) ⊆ ( bday ‘ 𝑁 ) )
	bdayfinbnd.4	⊢ ( 𝜑 → 0s ≤s 𝑍 )
Assertion	bdayfinbnd	⊢ ( 𝜑 → ( 𝑍 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bdayfinbnd.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
2		bdayfinbnd.2	⊢ ( 𝜑 → 𝑍 ∈ No )
3		bdayfinbnd.3	⊢ ( 𝜑 → ( bday ‘ 𝑍 ) ⊆ ( bday ‘ 𝑁 ) )
4		bdayfinbnd.4	⊢ ( 𝜑 → 0s ≤s 𝑍 )
5		fveq2	⊢ ( 𝑧 = 𝑍 → ( bday ‘ 𝑧 ) = ( bday ‘ 𝑍 ) )
6	5	sseq1d	⊢ ( 𝑧 = 𝑍 → ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ↔ ( bday ‘ 𝑍 ) ⊆ ( bday ‘ 𝑁 ) ) )
7		breq2	⊢ ( 𝑧 = 𝑍 → ( 0s ≤s 𝑧 ↔ 0s ≤s 𝑍 ) )
8	6 7	anbi12d	⊢ ( 𝑧 = 𝑍 → ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) ↔ ( ( bday ‘ 𝑍 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑍 ) ) )
9		eqeq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 = 𝑁 ↔ 𝑍 = 𝑁 ) )
10		eqeq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
11	10	3anbi1d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ( 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )
12	11	rexbidv	⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )
13	12	2rexbidv	⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )
14	9 13	orbi12d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ↔ ( 𝑍 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) )
15	8 14	imbi12d	⊢ ( 𝑧 = 𝑍 → ( ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) ↔ ( ( ( bday ‘ 𝑍 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑍 ) → ( 𝑍 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) ) )
16		bdayfinbndlem2	⊢ ( 𝑁 ∈ ℕ0s → ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) )
17	1 16	syl	⊢ ( 𝜑 → ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) )
18	15 17 2	rspcdva	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑍 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑍 ) → ( 𝑍 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) )
19	3 4 18	mp2and	⊢ ( 𝜑 → ( 𝑍 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑍 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )