Metamath Proof Explorer

Theorem bdayfinbndlem2

Description: Lemma for bdayfinbnd . Conduct the induction. (Contributed by Scott Fenton, 26-Feb-2026)

Ref Expression
Assertion bdayfinbndlem2 ( 𝑁 ∈ ℕ0s → ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑚 = 0s → ( bday ‘ 𝑚 ) = ( bday ‘ 0s ) )
2 bday0s ⊢ ( bday ‘ 0s ) = ∅
3 1 2 eqtrdi ⊢ ( 𝑚 = 0s → ( bday ‘ 𝑚 ) = ∅ )
4 3 sseq2d ⊢ ( 𝑚 = 0s → ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ↔ ( bday ‘ 𝑧 ) ⊆ ∅ ) )
5 ss0b ⊢ ( ( bday ‘ 𝑧 ) ⊆ ∅ ↔ ( bday ‘ 𝑧 ) = ∅ )
6 4 5 bitrdi ⊢ ( 𝑚 = 0s → ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ↔ ( bday ‘ 𝑧 ) = ∅ ) )
7 6 anbi1d ⊢ ( 𝑚 = 0s → ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) ↔ ( ( bday ‘ 𝑧 ) = ∅ ∧ 0s ≤s 𝑧 ) ) )
8 eqeq2 ⊢ ( 𝑚 = 0s → ( 𝑧 = 𝑚 ↔ 𝑧 = 0s ) )
9 breq2 ⊢ ( 𝑚 = 0s → ( ( 𝑥 +s 𝑝 ) <s 𝑚 ↔ ( 𝑥 +s 𝑝 ) <s 0s ) )
10 9 3anbi3d ⊢ ( 𝑚 = 0s → ( ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) )
11 10 rexbidv ⊢ ( 𝑚 = 0s → ( ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) )
12 11 2rexbidv ⊢ ( 𝑚 = 0s → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) )
13 8 12 orbi12d ⊢ ( 𝑚 = 0s → ( ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ↔ ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) ) )
14 7 13 imbi12d ⊢ ( 𝑚 = 0s → ( ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ) ↔ ( ( ( bday ‘ 𝑧 ) = ∅ ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) ) ) )
15 14 ralbidv ⊢ ( 𝑚 = 0s → ( ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ) ↔ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) = ∅ ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) ) ) )
16 fveq2 ⊢ ( 𝑚 = 𝑛 → ( bday ‘ 𝑚 ) = ( bday ‘ 𝑛 ) )
17 16 sseq2d ⊢ ( 𝑚 = 𝑛 → ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ↔ ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ) )
18 17 anbi1d ⊢ ( 𝑚 = 𝑛 → ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) ↔ ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑧 ) ) )
19 eqeq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑧 = 𝑚 ↔ 𝑧 = 𝑛 ) )
20 breq2 ⊢ ( 𝑚 = 𝑛 → ( ( 𝑥 +s 𝑝 ) <s 𝑚 ↔ ( 𝑥 +s 𝑝 ) <s 𝑛 ) )
21 20 3anbi3d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) )
22 21 rexbidv ⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) )
23 22 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 𝑛 ) ) )
24 19 23 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 𝑛 ) ) ) )
25 18 24 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 𝑛 ) ) ) ) )
26 25 ralbidv ⊢ ( 𝑚 = 𝑛 → ( ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ) ↔ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑛 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) ) ) )
27 fveq2 ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( bday ‘ 𝑚 ) = ( bday ‘ ( 𝑛 +s 1s ) ) )
28 27 sseq2d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ↔ ( bday ‘ 𝑧 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ) )
29 28 anbi1d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) ↔ ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑧 ) ) )
30 eqeq2 ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑧 = 𝑚 ↔ 𝑧 = ( 𝑛 +s 1s ) ) )
31 breq2 ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝑥 +s 𝑝 ) <s 𝑚 ↔ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) )
32 31 3anbi3d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
33 32 rexbidv ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
34 33 2rexbidv ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
35 30 34 orbi12d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ↔ ( 𝑧 = ( 𝑛 +s 1s ) ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) ) )
36 29 35 imbi12d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ) ↔ ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = ( 𝑛 +s 1s ) ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) ) ) )
37 36 ralbidv ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ) ↔ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = ( 𝑛 +s 1s ) ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) ) ) )
38 fveq2 ⊢ ( 𝑧 = 𝑤 → ( bday ‘ 𝑧 ) = ( bday ‘ 𝑤 ) )
39 38 sseq1d ⊢ ( 𝑧 = 𝑤 → ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ↔ ( bday ‘ 𝑤 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ) )
40 breq2 ⊢ ( 𝑧 = 𝑤 → ( 0s ≤s 𝑧 ↔ 0s ≤s 𝑤 ) )
41 39 40 anbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑧 ) ↔ ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑤 ) ) )
42 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑛 +s 1s ) ↔ 𝑤 = ( 𝑛 +s 1s ) ) )
43 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
44 43 3anbi1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
45 44 rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
46 45 2rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
47 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) )
48 47 eqeq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
49 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 +s 𝑝 ) = ( 𝑎 +s 𝑝 ) )
50 49 breq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ↔ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) )
51 48 50 3anbi13d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
52 51 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
53 oveq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 /su ( 2s ↑s 𝑝 ) ) = ( 𝑏 /su ( 2s ↑s 𝑝 ) ) )
54 53 oveq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) )
55 54 eqeq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ) )
56 breq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 <s ( 2s ↑s 𝑝 ) ↔ 𝑏 <s ( 2s ↑s 𝑝 ) ) )
57 55 56 3anbi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
58 57 rexbidv ⊢ ( 𝑦 = 𝑏 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) )
59 oveq2 ⊢ ( 𝑝 = 𝑞 → ( 2s ↑s 𝑝 ) = ( 2s ↑s 𝑞 ) )
60 59 oveq2d ⊢ ( 𝑝 = 𝑞 → ( 𝑏 /su ( 2s ↑s 𝑝 ) ) = ( 𝑏 /su ( 2s ↑s 𝑞 ) ) )
61 60 oveq2d ⊢ ( 𝑝 = 𝑞 → ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) )
62 61 eqeq2d ⊢ ( 𝑝 = 𝑞 → ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ) )
63 59 breq2d ⊢ ( 𝑝 = 𝑞 → ( 𝑏 <s ( 2s ↑s 𝑝 ) ↔ 𝑏 <s ( 2s ↑s 𝑞 ) ) )
64 oveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝑎 +s 𝑝 ) = ( 𝑎 +s 𝑞 ) )
65 64 breq1d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ↔ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) )
66 62 63 65 3anbi123d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) )
67 66 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) )
68 58 67 bitrdi ⊢ ( 𝑦 = 𝑏 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) )
69 52 68 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) )
70 46 69 bitrdi ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ↔ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) )
71 42 70 orbi12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 = ( 𝑛 +s 1s ) ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) ↔ ( 𝑤 = ( 𝑛 +s 1s ) ∨ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) ) )
72 41 71 imbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = ( 𝑛 +s 1s ) ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) ) ↔ ( ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑤 ) → ( 𝑤 = ( 𝑛 +s 1s ) ∨ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) ) ) )
73 72 cbvralvw ⊢ ( ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = ( 𝑛 +s 1s ) ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s ( 𝑛 +s 1s ) ) ) ) ↔ ∀ 𝑤 ∈ No ( ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑤 ) → ( 𝑤 = ( 𝑛 +s 1s ) ∨ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) ) )
74 37 73 bitrdi ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ) ↔ ∀ 𝑤 ∈ No ( ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑤 ) → ( 𝑤 = ( 𝑛 +s 1s ) ∨ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) ) ) )
75 fveq2 ⊢ ( 𝑚 = 𝑁 → ( bday ‘ 𝑚 ) = ( bday ‘ 𝑁 ) )
76 75 sseq2d ⊢ ( 𝑚 = 𝑁 → ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ↔ ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ) )
77 76 anbi1d ⊢ ( 𝑚 = 𝑁 → ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) ↔ ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) ) )
78 eqeq2 ⊢ ( 𝑚 = 𝑁 → ( 𝑧 = 𝑚 ↔ 𝑧 = 𝑁 ) )
79 breq2 ⊢ ( 𝑚 = 𝑁 → ( ( 𝑥 +s 𝑝 ) <s 𝑚 ↔ ( 𝑥 +s 𝑝 ) <s 𝑁 ) )
80 79 3anbi3d ⊢ ( 𝑚 = 𝑁 → ( ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )
81 80 rexbidv ⊢ ( 𝑚 = 𝑁 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )
82 81 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 𝑁 ) ) )
83 78 82 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 𝑁 ) ) ) )
84 77 83 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 𝑁 ) ) ) ) )
85 84 ralbidv ⊢ ( 𝑚 = 𝑁 → ( ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑚 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑚 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑚 ) ) ) ↔ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) ) )
86 bday0b ⊢ ( 𝑧 ∈ No → ( ( bday ‘ 𝑧 ) = ∅ ↔ 𝑧 = 0s ) )
87 orc ⊢ ( 𝑧 = 0s → ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) )
88 86 87 biimtrdi ⊢ ( 𝑧 ∈ No → ( ( bday ‘ 𝑧 ) = ∅ → ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) ) )
89 88 adantrd ⊢ ( 𝑧 ∈ No → ( ( ( bday ‘ 𝑧 ) = ∅ ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) ) )
90 89 rgen ⊢ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) = ∅ ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 0s ) ) )
91 simpl ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑛 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) ) ) → 𝑛 ∈ ℕ0s )
92 simpr ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑛 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) ) ) → ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑛 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) ) )
93 91 92 bdayfinbndcbv ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑛 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) ) ) → ∀ 𝑡 ∈ No ( ( ( bday ‘ 𝑡 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑡 ) → ( 𝑡 = 𝑛 ∨ ∃ 𝑐 ∈ ℕ0s ∃ 𝑑 ∈ ℕ0s ∃ 𝑟 ∈ ℕ0s ( 𝑡 = ( 𝑐 +s ( 𝑑 /su ( 2s ↑s 𝑟 ) ) ) ∧ 𝑑 <s ( 2s ↑s 𝑟 ) ∧ ( 𝑐 +s 𝑟 ) <s 𝑛 ) ) ) )
94 91 93 bdayfinbndlem1 ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑛 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) ) ) → ∀ 𝑤 ∈ No ( ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑤 ) → ( 𝑤 = ( 𝑛 +s 1s ) ∨ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) ) )
95 94 ex ⊢ ( 𝑛 ∈ ℕ0s → ( ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑛 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑛 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑛 ) ) ) → ∀ 𝑤 ∈ No ( ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ ( 𝑛 +s 1s ) ) ∧ 0s ≤s 𝑤 ) → ( 𝑤 = ( 𝑛 +s 1s ) ∨ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s ( 𝑛 +s 1s ) ) ) ) ) )
96 15 26 74 85 90 95 n0sind ⊢ ( 𝑁 ∈ ℕ0s → ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) )