Metamath Proof Explorer

Theorem madebdaylemold

Description: Lemma for madebday . If the inductive hypothesis of madebday is satisfied, the converse of oldbdayim holds. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion madebdaylemold ⊢ A ∈ On ∧ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → bday ⁡ X ∈ A → X ∈ Old ⁡ A

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ y = X → bday ⁡ y = bday ⁡ X
2 1 sseq1d ⊢ y = X → bday ⁡ y ⊆ b ↔ bday ⁡ X ⊆ b
3 eleq1 ⊢ y = X → y ∈ M ⁡ b ↔ X ∈ M ⁡ b
4 2 3 imbi12d ⊢ y = X → bday ⁡ y ⊆ b → y ∈ M ⁡ b ↔ bday ⁡ X ⊆ b → X ∈ M ⁡ b
5 4 rspcv ⊢ X ∈ No → ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b → bday ⁡ X ⊆ b → X ∈ M ⁡ b
6 5 ralimdv ⊢ X ∈ No → ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b → ∀ b ∈ A bday ⁡ X ⊆ b → X ∈ M ⁡ b
7 6 impcom ⊢ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → ∀ b ∈ A bday ⁡ X ⊆ b → X ∈ M ⁡ b
8 rexim ⊢ ∀ b ∈ A bday ⁡ X ⊆ b → X ∈ M ⁡ b → ∃ b ∈ A bday ⁡ X ⊆ b → ∃ b ∈ A X ∈ M ⁡ b
9 7 8 syl ⊢ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → ∃ b ∈ A bday ⁡ X ⊆ b → ∃ b ∈ A X ∈ M ⁡ b
10 9 3adant1 ⊢ A ∈ On ∧ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → ∃ b ∈ A bday ⁡ X ⊆ b → ∃ b ∈ A X ∈ M ⁡ b
11 bdayelon ⊢ bday ⁡ X ∈ On
12 onelssex ⊢ bday ⁡ X ∈ On ∧ A ∈ On → bday ⁡ X ∈ A ↔ ∃ b ∈ A bday ⁡ X ⊆ b
13 11 12 mpan ⊢ A ∈ On → bday ⁡ X ∈ A ↔ ∃ b ∈ A bday ⁡ X ⊆ b
14 13 3ad2ant1 ⊢ A ∈ On ∧ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → bday ⁡ X ∈ A ↔ ∃ b ∈ A bday ⁡ X ⊆ b
15 elold ⊢ A ∈ On → X ∈ Old ⁡ A ↔ ∃ b ∈ A X ∈ M ⁡ b
16 15 3ad2ant1 ⊢ A ∈ On ∧ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → X ∈ Old ⁡ A ↔ ∃ b ∈ A X ∈ M ⁡ b
17 10 14 16 3imtr4d ⊢ A ∈ On ∧ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → bday ⁡ X ∈ A → X ∈ Old ⁡ A