Theorem bdayle

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

	Ref	Expression
Assertion	bdayle	⊢ ( ( 𝑋 ∈ No ∧ Ord 𝑂 ) → ( ( bday ‘ 𝑋 ) ⊆ 𝑂 ↔ ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( bday ‘ 𝑦 ) ∈ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		bdayiun	⊢ ( 𝑋 ∈ No → ( bday ‘ 𝑋 ) = ∪ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) suc ( bday ‘ 𝑦 ) )
2	1	sseq1d	⊢ ( 𝑋 ∈ No → ( ( bday ‘ 𝑋 ) ⊆ 𝑂 ↔ ∪ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) suc ( bday ‘ 𝑦 ) ⊆ 𝑂 ) )
3		iunss	⊢ ( ∪ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) suc ( bday ‘ 𝑦 ) ⊆ 𝑂 ↔ ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) suc ( bday ‘ 𝑦 ) ⊆ 𝑂 )
4		fvex	⊢ ( bday ‘ 𝑦 ) ∈ V
5		ordelsuc	⊢ ( ( ( bday ‘ 𝑦 ) ∈ V ∧ Ord 𝑂 ) → ( ( bday ‘ 𝑦 ) ∈ 𝑂 ↔ suc ( bday ‘ 𝑦 ) ⊆ 𝑂 ) )
6	4 5	mpan	⊢ ( Ord 𝑂 → ( ( bday ‘ 𝑦 ) ∈ 𝑂 ↔ suc ( bday ‘ 𝑦 ) ⊆ 𝑂 ) )
7	6	ralbidv	⊢ ( Ord 𝑂 → ( ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( bday ‘ 𝑦 ) ∈ 𝑂 ↔ ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) suc ( bday ‘ 𝑦 ) ⊆ 𝑂 ) )
8	3 7	bitr4id	⊢ ( Ord 𝑂 → ( ∪ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) suc ( bday ‘ 𝑦 ) ⊆ 𝑂 ↔ ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( bday ‘ 𝑦 ) ∈ 𝑂 ) )
9	2 8	sylan9bb	⊢ ( ( 𝑋 ∈ No ∧ Ord 𝑂 ) → ( ( bday ‘ 𝑋 ) ⊆ 𝑂 ↔ ∀ 𝑦 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( bday ‘ 𝑦 ) ∈ 𝑂 ) )