Theorem bdayle

Description: A condition for bounding a birthday above. (Contributed by Scott Fenton, 22-Nov-2025)

	Ref	Expression
Assertion	bdayle	|- ( ( X e. No /\ Ord O ) -> ( ( bday ` X ) C_ O <-> A. y e. ( _Old ` ( bday ` X ) ) ( bday ` y ) e. O ) )

Proof

Step	Hyp	Ref	Expression
1		bdayiun	|- ( X e. No -> ( bday ` X ) = U_ y e. ( _Old ` ( bday ` X ) ) suc ( bday ` y ) )
2	1	sseq1d	|- ( X e. No -> ( ( bday ` X ) C_ O <-> U_ y e. ( _Old ` ( bday ` X ) ) suc ( bday ` y ) C_ O ) )
3		iunss	|- ( U_ y e. ( _Old ` ( bday ` X ) ) suc ( bday ` y ) C_ O <-> A. y e. ( _Old ` ( bday ` X ) ) suc ( bday ` y ) C_ O )
4		fvex	|- ( bday ` y ) e. _V
5		ordelsuc	|- ( ( ( bday ` y ) e. _V /\ Ord O ) -> ( ( bday ` y ) e. O <-> suc ( bday ` y ) C_ O ) )
6	4 5	mpan	|- ( Ord O -> ( ( bday ` y ) e. O <-> suc ( bday ` y ) C_ O ) )
7	6	ralbidv	|- ( Ord O -> ( A. y e. ( _Old ` ( bday ` X ) ) ( bday ` y ) e. O <-> A. y e. ( _Old ` ( bday ` X ) ) suc ( bday ` y ) C_ O ) )
8	3 7	bitr4id	|- ( Ord O -> ( U_ y e. ( _Old ` ( bday ` X ) ) suc ( bday ` y ) C_ O <-> A. y e. ( _Old ` ( bday ` X ) ) ( bday ` y ) e. O ) )
9	2 8	sylan9bb	|- ( ( X e. No /\ Ord O ) -> ( ( bday ` X ) C_ O <-> A. y e. ( _Old ` ( bday ` X ) ) ( bday ` y ) e. O ) )