Metamath Proof Explorer

Theorem bdayle

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

Ref Expression
Assertion bdayle ⊢ X ∈ No ∧ Ord ⁡ O → bday ⁡ X ⊆ O ↔ ∀ y ∈ Old ⁡ bday ⁡ X bday ⁡ y ∈ O

Proof

Step Hyp Ref Expression
1 bdayiun ⊢ X ∈ No → bday ⁡ X = ⋃ y ∈ Old ⁡ bday ⁡ X suc ⁡ bday ⁡ y
2 1 sseq1d ⊢ X ∈ No → bday ⁡ X ⊆ O ↔ ⋃ y ∈ Old ⁡ bday ⁡ X suc ⁡ bday ⁡ y ⊆ O
3 iunss ⊢ ⋃ y ∈ Old ⁡ bday ⁡ X suc ⁡ bday ⁡ y ⊆ O ↔ ∀ y ∈ Old ⁡ bday ⁡ X suc ⁡ bday ⁡ y ⊆ O
4 fvex ⊢ bday ⁡ y ∈ V
5 ordelsuc ⊢ bday ⁡ y ∈ V ∧ Ord ⁡ O → bday ⁡ y ∈ O ↔ suc ⁡ bday ⁡ y ⊆ O
6 4 5 mpan ⊢ Ord ⁡ O → bday ⁡ y ∈ O ↔ suc ⁡ bday ⁡ y ⊆ O
7 6 ralbidv ⊢ Ord ⁡ O → ∀ y ∈ Old ⁡ bday ⁡ X bday ⁡ y ∈ O ↔ ∀ y ∈ Old ⁡ bday ⁡ X suc ⁡ bday ⁡ y ⊆ O
8 3 7 bitr4id ⊢ Ord ⁡ O → ⋃ y ∈ Old ⁡ bday ⁡ X suc ⁡ bday ⁡ y ⊆ O ↔ ∀ y ∈ Old ⁡ bday ⁡ X bday ⁡ y ∈ O
9 2 8 sylan9bb ⊢ X ∈ No ∧ Ord ⁡ O → bday ⁡ X ⊆ O ↔ ∀ y ∈ Old ⁡ bday ⁡ X bday ⁡ y ∈ O