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 
|- ( ph -> N e. NN0_s )
bdayfinbndlem.2 
|- ( 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
Assertion bdayfinbndcbv 
|- ( ph -> A. w e. No ( ( ( bday ` w ) C_ ( bday ` N ) /\ 0s <_s w ) -> ( w = N \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b

Proof

Step Hyp Ref Expression
1 bdayfinbndlem.1 
 |-  ( ph -> N e. NN0_s )
2 bdayfinbndlem.2 
 |-  ( 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
3 fveq2 
 |-  ( z = w -> ( bday ` z ) = ( bday ` w ) )
4 3 sseq1d 
 |-  ( z = w -> ( ( bday ` z ) C_ ( bday ` N ) <-> ( bday ` w ) C_ ( bday ` N ) ) )
5 breq2 
 |-  ( z = w -> ( 0s <_s z <-> 0s <_s w ) )
6 4 5 anbi12d 
 |-  ( z = w -> ( ( ( bday ` z ) C_ ( bday ` N ) /\ 0s <_s z ) <-> ( ( bday ` w ) C_ ( bday ` N ) /\ 0s <_s w ) ) )
7 eqeq1 
 |-  ( z = w -> ( z = N <-> w = N ) )
8 eqeq1 
 |-  ( z = w -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( x +s ( y /su ( 2s ^su p ) ) ) ) )
9 8 3anbi1d 
 |-  ( z = w -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
10 9 rexbidv 
 |-  ( z = w -> ( E. p e. NN0_s ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
11 10 2rexbidv 
 |-  ( z = w -> ( 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 ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
12 oveq1 
 |-  ( x = a -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( y /su ( 2s ^su p ) ) ) )
13 12 eqeq2d 
 |-  ( x = a -> ( w = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( y /su ( 2s ^su p ) ) ) ) )
14 oveq1 
 |-  ( x = a -> ( x +s p ) = ( a +s p ) )
15 14 breq1d 
 |-  ( x = a -> ( ( x +s p )  ( a +s p )
16 13 15 3anbi13d 
 |-  ( x = a -> ( ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y
17 16 rexbidv 
 |-  ( x = a -> ( E. p e. NN0_s ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y
18 oveq1 
 |-  ( y = b -> ( y /su ( 2s ^su p ) ) = ( b /su ( 2s ^su p ) ) )
19 18 oveq2d 
 |-  ( y = b -> ( a +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su p ) ) ) )
20 19 eqeq2d 
 |-  ( y = b -> ( w = ( a +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su p ) ) ) ) )
21 breq1 
 |-  ( y = b -> ( y  b
22 20 21 3anbi12d 
 |-  ( y = b -> ( ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y  ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b
23 22 rexbidv 
 |-  ( y = b -> ( E. p e. NN0_s ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y  E. p e. NN0_s ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b
24 oveq2 
 |-  ( p = q -> ( 2s ^su p ) = ( 2s ^su q ) )
25 oveq2 
 |-  ( ( 2s ^su p ) = ( 2s ^su q ) -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) )
26 24 25 syl 
 |-  ( p = q -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) )
27 26 oveq2d 
 |-  ( p = q -> ( a +s ( b /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su q ) ) ) )
28 27 eqeq2d 
 |-  ( p = q -> ( w = ( a +s ( b /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su q ) ) ) ) )
29 24 breq2d 
 |-  ( p = q -> ( b  b
30 oveq2 
 |-  ( p = q -> ( a +s p ) = ( a +s q ) )
31 30 breq1d 
 |-  ( p = q -> ( ( a +s p )  ( a +s q )
32 28 29 31 3anbi123d 
 |-  ( p = q -> ( ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b  ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
33 32 cbvrexvw 
 |-  ( E. p e. NN0_s ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b  E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
34 23 33 bitrdi 
 |-  ( y = b -> ( E. p e. NN0_s ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y  E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
35 17 34 cbvrex2vw 
 |-  ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y  E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
36 11 35 bitrdi 
 |-  ( z = w -> ( 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. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
37 7 36 orbi12d 
 |-  ( z = w -> ( ( 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  ( w = N \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
38 6 37 imbi12d 
 |-  ( z = w -> ( ( ( ( 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 ` w ) C_ ( bday ` N ) /\ 0s <_s w ) -> ( w = N \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
39 38 cbvralvw 
 |-  ( 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. w e. No ( ( ( bday ` w ) C_ ( bday ` N ) /\ 0s <_s w ) -> ( w = N \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
40 2 39 sylib 
 |-  ( ph -> A. w e. No ( ( ( bday ` w ) C_ ( bday ` N ) /\ 0s <_s w ) -> ( w = N \/ E. a e. NN0_s E. b e. NN0_s E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b