Theorem bdayfinbndcbv

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

	Ref	Expression
Hypotheses	bdayfinbndlem.1	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
	bdayfinbndlem.2	No typesetting found for |- ( 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	Could not format assertion : No typesetting found for |- ( 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	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
2		bdayfinbndlem.2	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
3		fveq2	$$⊢z=w\to \mathrm{bday}\left(z\right)=\mathrm{bday}\left(w\right)$$
4	3	sseq1d	$$⊢z=w\to \left(\mathrm{bday}\left(z\right)\subseteq \mathrm{bday}\left(N\right)\leftrightarrow \mathrm{bday}\left(w\right)\subseteq \mathrm{bday}\left(N\right)\right)$$
5		breq2	$$⊢z=w\to \left(0_s{\le }_{s}z\leftrightarrow 0_s{\le }_{s}w\right)$$
6	4 5	anbi12d	$$⊢z=w\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(w\right)\subseteq \mathrm{bday}\left(N\right)\wedge 0_s{\le }_{s}w\right)\right)$$
7		eqeq1	$$⊢z=w\to \left(z=N\leftrightarrow w=N\right)$$
8		eqeq1	Could not format ( z = w -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( z = w -> ( z = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( x +s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
9	8	3anbi1d	Could not format ( z = w -> ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( z = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
10	9	rexbidv	Could not format ( 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 ( 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	Could not format ( 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 ( 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	Could not format ( x = a -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( y /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( x = a -> ( x +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( y /su ( 2s ^su p ) ) ) ) with typecode |-
13	12	eqeq2d	Could not format ( x = a -> ( w = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( x = a -> ( w = ( x +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
14		oveq1	$$⊢x=a\to x{+}_{s}p=a{+}_{s}p$$
15	14	breq1d	$$⊢x=a\to \left(\left(x{+}_{s}p\right){<}_{s}N\leftrightarrow \left(a{+}_{s}p\right){<}_{s}N\right)$$
16	13 15	3anbi13d	Could not format ( x = a -> ( ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y ( ( w = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y
17	16	rexbidv	Could not format ( 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 ( 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	Could not format ( y = b -> ( y /su ( 2s ^su p ) ) = ( b /su ( 2s ^su p ) ) ) : No typesetting found for |- ( y = b -> ( y /su ( 2s ^su p ) ) = ( b /su ( 2s ^su p ) ) ) with typecode |-
19	18	oveq2d	Could not format ( y = b -> ( a +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( y = b -> ( a +s ( y /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su p ) ) ) ) with typecode |-
20	19	eqeq2d	Could not format ( y = b -> ( w = ( a +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( y = b -> ( w = ( a +s ( y /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su p ) ) ) ) ) with typecode |-
21		breq1	Could not format ( y = b -> ( y b ( y b
22	20 21	3anbi12d	Could not format ( y = b -> ( ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b ( ( w = ( a +s ( y /su ( 2s ^su p ) ) ) /\ y ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b
23	22	rexbidv	Could not format ( 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 ( 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	Could not format ( p = q -> ( 2s ^su p ) = ( 2s ^su q ) ) : No typesetting found for |- ( p = q -> ( 2s ^su p ) = ( 2s ^su q ) ) with typecode |-
25		oveq2	Could not format ( ( 2s ^su p ) = ( 2s ^su q ) -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) ) : No typesetting found for |- ( ( 2s ^su p ) = ( 2s ^su q ) -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) ) with typecode |-
26	24 25	syl	Could not format ( p = q -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) ) : No typesetting found for |- ( p = q -> ( b /su ( 2s ^su p ) ) = ( b /su ( 2s ^su q ) ) ) with typecode |-
27	26	oveq2d	Could not format ( p = q -> ( a +s ( b /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su q ) ) ) ) : No typesetting found for |- ( p = q -> ( a +s ( b /su ( 2s ^su p ) ) ) = ( a +s ( b /su ( 2s ^su q ) ) ) ) with typecode |-
28	27	eqeq2d	Could not format ( p = q -> ( w = ( a +s ( b /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su q ) ) ) ) ) : No typesetting found for |- ( p = q -> ( w = ( a +s ( b /su ( 2s ^su p ) ) ) <-> w = ( a +s ( b /su ( 2s ^su q ) ) ) ) ) with typecode |-
29	24	breq2d	Could not format ( p = q -> ( b b ( b b
30		oveq2	$$⊢p=q\to a{+}_{s}p=a{+}_{s}q$$
31	30	breq1d	$$⊢p=q\to \left(\left(a{+}_{s}p\right){<}_{s}N\leftrightarrow \left(a{+}_{s}q\right){<}_{s}N\right)$$
32	28 29 31	3anbi123d	Could not format ( p = q -> ( ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b ( ( w = ( a +s ( b /su ( 2s ^su p ) ) ) /\ b ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
33	32	cbvrexvw	Could not format ( 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 E. q e. NN0_s ( w = ( a +s ( b /su ( 2s ^su q ) ) ) /\ b
34	23 33	bitrdi	Could not format ( 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 ( 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	Could not format ( 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 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	Could not format ( 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 ( 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	Could not format ( 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 ( ( 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	Could not format ( 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 ( ( ( ( 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	Could not format ( 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 ( 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	Could not format ( 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 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