Metamath Proof Explorer

Theorem bdayfinbndcbv

Description: Lemma for bdayfinbnd . Change some bound variables. (Contributed by Scott Fenton, 25-Feb-2026)

Ref Expression
Hypotheses bdayfinbndlem.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
bdayfinbndlem.2 ⊢ ( 𝜑 → ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) )
Assertion bdayfinbndcbv ( 𝜑 → ∀ 𝑤 ∈ No ( ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑤 ) → ( 𝑤 = 𝑁 ∨ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 bdayfinbndlem.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
2 bdayfinbndlem.2 ⊢ ( 𝜑 → ∀ 𝑧 ∈ No ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) → ( 𝑧 = 𝑁 ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) ) )
3 fveq2 ⊢ ( 𝑧 = 𝑤 → ( bday ‘ 𝑧 ) = ( bday ‘ 𝑤 ) )
4 3 sseq1d ⊢ ( 𝑧 = 𝑤 → ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ↔ ( bday ‘ 𝑤 ) ⊆ ( bday ‘ 𝑁 ) ) )
5 breq2 ⊢ ( 𝑧 = 𝑤 → ( 0s ≤s 𝑧 ↔ 0s ≤s 𝑤 ) )
6 4 5 anbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ( bday ‘ 𝑧 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑧 ) ↔ ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑤 ) ) )
7 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = 𝑁 ↔ 𝑤 = 𝑁 ) )
8 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
9 8 3anbi1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )
10 9 rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ) )
11 10 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 𝑁 ) ) )
12 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) )
13 12 eqeq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
14 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 +s 𝑝 ) = ( 𝑎 +s 𝑝 ) )
15 14 breq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 +s 𝑝 ) <s 𝑁 ↔ ( 𝑎 +s 𝑝 ) <s 𝑁 ) )
16 13 15 3anbi13d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ) )
17 16 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ) )
18 oveq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 /su ( 2s ↑s 𝑝 ) ) = ( 𝑏 /su ( 2s ↑s 𝑝 ) ) )
19 18 oveq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) )
20 19 eqeq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ) )
21 breq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 <s ( 2s ↑s 𝑝 ) ↔ 𝑏 <s ( 2s ↑s 𝑝 ) ) )
22 20 21 3anbi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ↔ ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ) )
23 22 rexbidv ⊢ ( 𝑦 = 𝑏 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ) )
24 oveq2 ⊢ ( 𝑝 = 𝑞 → ( 2s ↑s 𝑝 ) = ( 2s ↑s 𝑞 ) )
25 oveq2 ⊢ ( ( 2s ↑s 𝑝 ) = ( 2s ↑s 𝑞 ) → ( 𝑏 /su ( 2s ↑s 𝑝 ) ) = ( 𝑏 /su ( 2s ↑s 𝑞 ) ) )
26 24 25 syl ⊢ ( 𝑝 = 𝑞 → ( 𝑏 /su ( 2s ↑s 𝑝 ) ) = ( 𝑏 /su ( 2s ↑s 𝑞 ) ) )
27 26 oveq2d ⊢ ( 𝑝 = 𝑞 → ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) )
28 27 eqeq2d ⊢ ( 𝑝 = 𝑞 → ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ↔ 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ) )
29 24 breq2d ⊢ ( 𝑝 = 𝑞 → ( 𝑏 <s ( 2s ↑s 𝑝 ) ↔ 𝑏 <s ( 2s ↑s 𝑞 ) ) )
30 oveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝑎 +s 𝑝 ) = ( 𝑎 +s 𝑞 ) )
31 30 breq1d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑎 +s 𝑝 ) <s 𝑁 ↔ ( 𝑎 +s 𝑞 ) <s 𝑁 ) )
32 28 29 31 3anbi123d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ↔ ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s 𝑁 ) ) )
33 32 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s 𝑁 ) )
34 23 33 bitrdi ⊢ ( 𝑦 = 𝑏 → ( ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑎 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s 𝑁 ) ) )
35 17 34 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑤 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s 𝑁 ) )
36 11 35 bitrdi ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝑧 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ∧ ( 𝑥 +s 𝑝 ) <s 𝑁 ) ↔ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s 𝑁 ) ) )
37 7 36 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 𝑁 ) ) ) )
38 6 37 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 𝑁 ) ) ) ) )
39 38 cbvralvw ⊢ ( ∀ 𝑧 ∈ 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 𝑁 ) ) ) )
40 2 39 sylib ⊢ ( 𝜑 → ∀ 𝑤 ∈ No ( ( ( bday ‘ 𝑤 ) ⊆ ( bday ‘ 𝑁 ) ∧ 0s ≤s 𝑤 ) → ( 𝑤 = 𝑁 ∨ ∃ 𝑎 ∈ ℕ0s ∃ 𝑏 ∈ ℕ0s ∃ 𝑞 ∈ ℕ0s ( 𝑤 = ( 𝑎 +s ( 𝑏 /su ( 2s ↑s 𝑞 ) ) ) ∧ 𝑏 <s ( 2s ↑s 𝑞 ) ∧ ( 𝑎 +s 𝑞 ) <s 𝑁 ) ) ) )