| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elfvdm |
⊢ ( 𝑋 ∈ ( M ‘ 𝐴 ) → 𝐴 ∈ dom M ) |
| 2 |
|
madef |
⊢ M : On ⟶ 𝒫 No |
| 3 |
2
|
fdmi |
⊢ dom M = On |
| 4 |
1 3
|
eleqtrdi |
⊢ ( 𝑋 ∈ ( M ‘ 𝐴 ) → 𝐴 ∈ On ) |
| 5 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( M ‘ 𝑎 ) = ( M ‘ 𝑏 ) ) |
| 6 |
|
sseq2 |
⊢ ( 𝑎 = 𝑏 → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝑏 ) ) |
| 7 |
5 6
|
raleqbidv |
⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑥 ) ⊆ 𝑏 ) ) |
| 8 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) ) |
| 9 |
8
|
sseq1d |
⊢ ( 𝑥 = 𝑦 → ( ( bday ‘ 𝑥 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ) |
| 10 |
9
|
cbvralvw |
⊢ ( ∀ 𝑥 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑥 ) ⊆ 𝑏 ↔ ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) |
| 11 |
7 10
|
bitrdi |
⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ) |
| 12 |
|
fveq2 |
⊢ ( 𝑎 = 𝐴 → ( M ‘ 𝑎 ) = ( M ‘ 𝐴 ) ) |
| 13 |
|
sseq2 |
⊢ ( 𝑎 = 𝐴 → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝐴 ) ) |
| 14 |
12 13
|
raleqbidv |
⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 ) ) |
| 15 |
|
elmade2 |
⊢ ( 𝑎 ∈ On → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) ) |
| 16 |
15
|
adantr |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) ) |
| 17 |
|
elpwi |
⊢ ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) → 𝑙 ⊆ ( O ‘ 𝑎 ) ) |
| 18 |
|
elpwi |
⊢ ( 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) → 𝑟 ⊆ ( O ‘ 𝑎 ) ) |
| 19 |
17 18
|
anim12i |
⊢ ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( 𝑙 ⊆ ( O ‘ 𝑎 ) ∧ 𝑟 ⊆ ( O ‘ 𝑎 ) ) ) |
| 20 |
|
unss |
⊢ ( ( 𝑙 ⊆ ( O ‘ 𝑎 ) ∧ 𝑟 ⊆ ( O ‘ 𝑎 ) ) ↔ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) |
| 21 |
19 20
|
sylib |
⊢ ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) |
| 22 |
|
simpr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → 𝑙 <<s 𝑟 ) |
| 23 |
|
simplll |
⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → 𝑎 ∈ On ) |
| 24 |
|
dfss3 |
⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) 𝑧 ∈ ( O ‘ 𝑎 ) ) |
| 25 |
|
fveq2 |
⊢ ( 𝑦 = 𝑧 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑧 ) ) |
| 26 |
25
|
sseq1d |
⊢ ( 𝑦 = 𝑧 → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 27 |
26
|
rspccv |
⊢ ( ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 28 |
27
|
ralimi |
⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ∀ 𝑏 ∈ 𝑎 ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 29 |
|
rexim |
⊢ ( ∀ 𝑏 ∈ 𝑎 ( 𝑧 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑧 ) ⊆ 𝑏 ) → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 30 |
28 29
|
syl |
⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 31 |
30
|
adantl |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 32 |
|
elold |
⊢ ( 𝑎 ∈ On → ( 𝑧 ∈ ( O ‘ 𝑎 ) ↔ ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) ) ) |
| 33 |
32
|
adantr |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑧 ∈ ( O ‘ 𝑎 ) ↔ ∃ 𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘ 𝑏 ) ) ) |
| 34 |
|
bdayelon |
⊢ ( bday ‘ 𝑧 ) ∈ On |
| 35 |
|
onelssex |
⊢ ( ( ( bday ‘ 𝑧 ) ∈ On ∧ 𝑎 ∈ On ) → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 36 |
34 35
|
mpan |
⊢ ( 𝑎 ∈ On → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 37 |
36
|
adantr |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( bday ‘ 𝑧 ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 ( bday ‘ 𝑧 ) ⊆ 𝑏 ) ) |
| 38 |
31 33 37
|
3imtr4d |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑧 ∈ ( O ‘ 𝑎 ) → ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 39 |
38
|
ralimdv |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) 𝑧 ∈ ( O ‘ 𝑎 ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 40 |
24 39
|
biimtrid |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 41 |
40
|
imp |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) |
| 42 |
41
|
adantr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) |
| 43 |
|
bdayfun |
⊢ Fun bday |
| 44 |
|
oldssno |
⊢ ( O ‘ 𝑎 ) ⊆ No |
| 45 |
|
sstr |
⊢ ( ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ∧ ( O ‘ 𝑎 ) ⊆ No ) → ( 𝑙 ∪ 𝑟 ) ⊆ No ) |
| 46 |
44 45
|
mpan2 |
⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( 𝑙 ∪ 𝑟 ) ⊆ No ) |
| 47 |
|
bdaydm |
⊢ dom bday = No |
| 48 |
46 47
|
sseqtrrdi |
⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( 𝑙 ∪ 𝑟 ) ⊆ dom bday ) |
| 49 |
|
funimass4 |
⊢ ( ( Fun bday ∧ ( 𝑙 ∪ 𝑟 ) ⊆ dom bday ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 50 |
43 48 49
|
sylancr |
⊢ ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 51 |
50
|
adantl |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 52 |
51
|
adantr |
⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ( ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ↔ ∀ 𝑧 ∈ ( 𝑙 ∪ 𝑟 ) ( bday ‘ 𝑧 ) ∈ 𝑎 ) ) |
| 53 |
42 52
|
mpbird |
⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ) |
| 54 |
|
scutbdaybnd |
⊢ ( ( 𝑙 <<s 𝑟 ∧ 𝑎 ∈ On ∧ ( bday “ ( 𝑙 ∪ 𝑟 ) ) ⊆ 𝑎 ) → ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 ) |
| 55 |
22 23 53 54
|
syl3anc |
⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 ) |
| 56 |
|
fveq2 |
⊢ ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( bday ‘ ( 𝑙 |s 𝑟 ) ) = ( bday ‘ 𝑥 ) ) |
| 57 |
56
|
sseq1d |
⊢ ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( ( bday ‘ ( 𝑙 |s 𝑟 ) ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 58 |
55 57
|
syl5ibcom |
⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) ∧ 𝑙 <<s 𝑟 ) → ( ( 𝑙 |s 𝑟 ) = 𝑥 → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 59 |
58
|
expimpd |
⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) ∧ ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 60 |
59
|
ex |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∪ 𝑟 ) ⊆ ( O ‘ 𝑎 ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) ) |
| 61 |
21 60
|
syl5 |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ( 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∧ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ) → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) ) |
| 62 |
61
|
rexlimdvv |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝑎 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝑎 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 63 |
16 62
|
sylbid |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ( 𝑥 ∈ ( M ‘ 𝑎 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 64 |
63
|
ralrimiv |
⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 ) → ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ) |
| 65 |
64
|
ex |
⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ ( M ‘ 𝑏 ) ( bday ‘ 𝑦 ) ⊆ 𝑏 → ∀ 𝑥 ∈ ( M ‘ 𝑎 ) ( bday ‘ 𝑥 ) ⊆ 𝑎 ) ) |
| 66 |
11 14 65
|
tfis3 |
⊢ ( 𝐴 ∈ On → ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 ) |
| 67 |
|
fveq2 |
⊢ ( 𝑥 = 𝑋 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑋 ) ) |
| 68 |
67
|
sseq1d |
⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) ⊆ 𝐴 ↔ ( bday ‘ 𝑋 ) ⊆ 𝐴 ) ) |
| 69 |
68
|
rspccv |
⊢ ( ∀ 𝑥 ∈ ( M ‘ 𝐴 ) ( bday ‘ 𝑥 ) ⊆ 𝐴 → ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 ) ) |
| 70 |
66 69
|
syl |
⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 ) ) |
| 71 |
4 70
|
mpcom |
⊢ ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 ) |