| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( M ‘ 𝑎 ) = ( M ‘ 𝑏 ) ) |
| 2 |
|
sseq2 |
⊢ ( 𝑎 = 𝑏 → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝑏 ) ) |
| 3 |
1 2
|
raleqbidv |
⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑥 ) ⊆ 𝑏 ) ) |
| 4 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) ) |
| 5 |
4
|
sseq1d |
⊢ ( 𝑥 = 𝑦 → ( ( bday ‘ 𝑥 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ) |
| 6 |
5
|
cbvralvw |
⊢ ( ∀ 𝑥 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑥 ) ⊆ 𝑏 ↔ ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) |
| 7 |
3 6
|
bitrdi |
⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ) |
| 8 |
|
fveq2 |
⊢ ( 𝑎 = 𝐴 → ( M ‘ 𝑎 ) = ( M ‘ 𝐴 ) ) |
| 9 |
|
sseq2 |
⊢ ( 𝑎 = 𝐴 → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝐴 ) ) |
| 10 |
8 9
|
raleqbidv |
⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 ) ) |
| 11 |
|
elmade2 |
⊢ ( 𝑎 ∈ On → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) ) |
| 12 |
11
|
adantr |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) ) |
| 13 |
|
pwuncl |
⊢ ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( 𝑙 ∪ 𝑟 ) ∈ 𝒫 ( O ‘ 𝑎 ) ) |
| 14 |
13
|
elpwid |
⊢ ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) |
| 15 |
|
simprr |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → 𝑙 <<s 𝑟 ) |
| 16 |
|
simpll |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → 𝑎 ∈ On ) |
| 17 |
|
dfss3 |
⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) 𝑧 ∈ ( O ‘ 𝑎 ) ) |
| 18 |
|
fveq2 |
⊢ ( 𝑦 = 𝑧 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑧 ) ) |
| 19 |
18
|
sseq1d |
⊢ ( 𝑦 = 𝑧 → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 20 |
19
|
rspccv |
⊢ ( ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 21 |
20
|
ralimi |
⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ∀ 𝑏 ∈ 𝑎 ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 22 |
|
rexim |
⊢ ( ∀ 𝑏 ∈ 𝑎 ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 23 |
21 22
|
syl |
⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 24 |
23
|
adantl |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 25 |
|
elold |
⊢ ( 𝑎 ∈ On → ( 𝑧 ∈ ( O ‘ 𝑎 ) ↔ ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) ) ) |
| 26 |
25
|
adantr |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑧 ∈ ( O ‘ 𝑎 ) ↔ ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) ) ) |
| 27 |
|
bdayelon |
⊢ ( bday ‘ 𝑧 ) ∈ On |
| 28 |
|
onelssex |
⊢ ( ( ( bday ‘ 𝑧 ) ∈ On ∧ 𝑎 ∈ On ) → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 29 |
27 28
|
mpan |
⊢ ( 𝑎 ∈ On → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 30 |
29
|
adantr |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 31 |
24 26 30
|
3imtr4d |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑧 ∈ ( O ‘ 𝑎 ) → ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 32 |
31
|
ralimdv |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) 𝑧 ∈ ( O ‘ 𝑎 ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 33 |
17 32
|
syl5bi |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 34 |
33
|
imp |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) |
| 35 |
34
|
adantrr |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) |
| 36 |
|
bdayfun |
⊢ Fun bday |
| 37 |
|
ssltss1 |
⊢ ( 𝑙 <<s 𝑟 → 𝑙 ⊆ No ) |
| 38 |
|
ssltss2 |
⊢ ( 𝑙 <<s 𝑟 → 𝑟 ⊆ No ) |
| 39 |
37 38
|
unssd |
⊢ ( 𝑙 <<s 𝑟 → ( 𝑙 ∪ 𝑟 ) ⊆ No ) |
| 40 |
39
|
adantl |
⊢ ( ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) → ( 𝑙 ∪ 𝑟 ) ⊆ No ) |
| 41 |
40
|
adantl |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → ( 𝑙 ∪ 𝑟 ) ⊆ No ) |
| 42 |
|
bdaydm |
⊢ dom bday = No |
| 43 |
41 42
|
sseqtrrdi |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → ( 𝑙 ∪ 𝑟 ) ⊆ dom bday ) |
| 44 |
|
funimass4 |
⊢ ( ( Fun bday ∧ ( 𝑙 ∪ 𝑟 ) ⊆ dom bday ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 45 |
36 43 44
|
sylancr |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 46 |
35 45
|
mpbird |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ) |
| 47 |
|
scutbdaybnd |
⊢ ( ( 𝑙 <<s 𝑟 ∧ 𝑎 ∈ On ∧ ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ) → ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 ) |
| 48 |
15 16 46 47
|
syl3anc |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 ) |
| 49 |
|
fveq2 |
⊢ ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( bday ‘ ( 𝑙 |s 𝑟 ) ) = ( bday ‘ 𝑥 ) ) |
| 50 |
49
|
sseq1d |
⊢ ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 51 |
48 50
|
syl5ibcom |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ 𝑙 <<s 𝑟 ) ) → ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 52 |
51
|
expr |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ( 𝑙 <<s 𝑟 → ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) ) |
| 53 |
52
|
impd |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 54 |
53
|
ex |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) ) |
| 55 |
14 54
|
syl5 |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) ) |
| 56 |
55
|
rexlimdvv |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 57 |
12 56
|
sylbid |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑥 ∈ ( M ‘ 𝑎 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 58 |
57
|
ralrimiv |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ) |
| 59 |
58
|
ex |
⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 60 |
7 10 59
|
tfis3 |
⊢ ( 𝐴 ∈ On → ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 ) |
| 61 |
|
fveq2 |
⊢ ( 𝑥 = 𝑋 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑋 ) ) |
| 62 |
61
|
sseq1d |
⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) ⊆ 𝐴 ↔ ( bday ‘ 𝑋 ) ⊆ 𝐴 ) ) |
| 63 |
62
|
rspccva |
⊢ ( ( ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝐴 ) ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 ) |
| 64 |
60 63
|
sylan |
⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ ( M ‘ 𝐴 ) ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 ) |