| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fveq2 |
⊢ ( 𝑦 = 𝑋 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑋 ) ) |
| 2 |
1
|
sseq1d |
⊢ ( 𝑦 = 𝑋 → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑋 ) ⊆ 𝑏 ) ) |
| 3 |
|
eleq1 |
⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∈ ( M ‘ 𝑏 ) ↔ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) |
| 4 |
2 3
|
imbi12d |
⊢ ( 𝑦 = 𝑋 → ( ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝑏 → 𝑋 ∈ ( M ‘ 𝑏 ) ) ) ) |
| 5 |
4
|
rspcv |
⊢ ( 𝑋 ∈ No → ( ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) → ( ( bday ‘ 𝑋 ) ⊆ 𝑏 → 𝑋 ∈ ( M ‘ 𝑏 ) ) ) ) |
| 6 |
5
|
ralimdv |
⊢ ( 𝑋 ∈ No → ( ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) → ∀ 𝑏 ∈ 𝐴 ( ( bday ‘ 𝑋 ) ⊆ 𝑏 → 𝑋 ∈ ( M ‘ 𝑏 ) ) ) ) |
| 7 |
6
|
impcom |
⊢ ( ( ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ∀ 𝑏 ∈ 𝐴 ( ( bday ‘ 𝑋 ) ⊆ 𝑏 → 𝑋 ∈ ( M ‘ 𝑏 ) ) ) |
| 8 |
|
rexim |
⊢ ( ∀ 𝑏 ∈ 𝐴 ( ( bday ‘ 𝑋 ) ⊆ 𝑏 → 𝑋 ∈ ( M ‘ 𝑏 ) ) → ( ∃ 𝑏 ∈ 𝐴 ( bday ‘ 𝑋 ) ⊆ 𝑏 → ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) ) |
| 9 |
7 8
|
syl |
⊢ ( ( ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ∃ 𝑏 ∈ 𝐴 ( bday ‘ 𝑋 ) ⊆ 𝑏 → ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) ) |
| 10 |
9
|
3adant1 |
⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ∃ 𝑏 ∈ 𝐴 ( bday ‘ 𝑋 ) ⊆ 𝑏 → ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) ) |
| 11 |
|
bdayelon |
⊢ ( bday ‘ 𝑋 ) ∈ On |
| 12 |
|
onelssex |
⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( bday ‘ 𝑋 ) ∈ 𝐴 ↔ ∃ 𝑏 ∈ 𝐴 ( bday ‘ 𝑋 ) ⊆ 𝑏 ) ) |
| 13 |
11 12
|
mpan |
⊢ ( 𝐴 ∈ On → ( ( bday ‘ 𝑋 ) ∈ 𝐴 ↔ ∃ 𝑏 ∈ 𝐴 ( bday ‘ 𝑋 ) ⊆ 𝑏 ) ) |
| 14 |
13
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) ∈ 𝐴 ↔ ∃ 𝑏 ∈ 𝐴 ( bday ‘ 𝑋 ) ⊆ 𝑏 ) ) |
| 15 |
|
elold |
⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) ) |
| 16 |
15
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) ) |
| 17 |
10 14 16
|
3imtr4d |
⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) ∈ 𝐴 → 𝑋 ∈ ( O ‘ 𝐴 ) ) ) |