| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfvdm 6943 | . . 3
⊢ (𝑋 ∈ ( M ‘𝐴) → 𝐴 ∈ dom M ) | 
| 2 |  | madef 27895 | . . . 4
⊢  M
:On⟶𝒫  No | 
| 3 | 2 | fdmi 6747 | . . 3
⊢ dom M =
On | 
| 4 | 1, 3 | eleqtrdi 2851 | . 2
⊢ (𝑋 ∈ ( M ‘𝐴) → 𝐴 ∈ On) | 
| 5 |  | fveq2 6906 | . . . . . 6
⊢ (𝑎 = 𝑏 → ( M ‘𝑎) = ( M ‘𝑏)) | 
| 6 |  | sseq2 4010 | . . . . . 6
⊢ (𝑎 = 𝑏 → (( bday
‘𝑥) ⊆
𝑎 ↔ ( bday ‘𝑥) ⊆ 𝑏)) | 
| 7 | 5, 6 | raleqbidv 3346 | . . . . 5
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ ( M ‘𝑎)( bday
‘𝑥) ⊆
𝑎 ↔ ∀𝑥 ∈ ( M ‘𝑏)( bday
‘𝑥) ⊆
𝑏)) | 
| 8 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑥 = 𝑦 → ( bday
‘𝑥) = ( bday ‘𝑦)) | 
| 9 | 8 | sseq1d 4015 | . . . . . 6
⊢ (𝑥 = 𝑦 → (( bday
‘𝑥) ⊆
𝑏 ↔ ( bday ‘𝑦) ⊆ 𝑏)) | 
| 10 | 9 | cbvralvw 3237 | . . . . 5
⊢
(∀𝑥 ∈ (
M ‘𝑏)( bday ‘𝑥) ⊆ 𝑏 ↔ ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) | 
| 11 | 7, 10 | bitrdi 287 | . . . 4
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ ( M ‘𝑎)( bday
‘𝑥) ⊆
𝑎 ↔ ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏)) | 
| 12 |  | fveq2 6906 | . . . . 5
⊢ (𝑎 = 𝐴 → ( M ‘𝑎) = ( M ‘𝐴)) | 
| 13 |  | sseq2 4010 | . . . . 5
⊢ (𝑎 = 𝐴 → (( bday
‘𝑥) ⊆
𝑎 ↔ ( bday ‘𝑥) ⊆ 𝐴)) | 
| 14 | 12, 13 | raleqbidv 3346 | . . . 4
⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ ( M ‘𝑎)( bday
‘𝑥) ⊆
𝑎 ↔ ∀𝑥 ∈ ( M ‘𝐴)( bday
‘𝑥) ⊆
𝐴)) | 
| 15 |  | elmade2 27907 | . . . . . . . 8
⊢ (𝑎 ∈ On → (𝑥 ∈ ( M ‘𝑎) ↔ ∃𝑙 ∈ 𝒫 ( O
‘𝑎)∃𝑟 ∈ 𝒫 ( O
‘𝑎)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) | 
| 16 | 15 | adantr 480 | . . . . . . 7
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → (𝑥 ∈ ( M ‘𝑎) ↔ ∃𝑙 ∈ 𝒫 ( O
‘𝑎)∃𝑟 ∈ 𝒫 ( O
‘𝑎)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥))) | 
| 17 |  | elpwi 4607 | . . . . . . . . . . 11
⊢ (𝑙 ∈ 𝒫 ( O
‘𝑎) → 𝑙 ⊆ ( O ‘𝑎)) | 
| 18 |  | elpwi 4607 | . . . . . . . . . . 11
⊢ (𝑟 ∈ 𝒫 ( O
‘𝑎) → 𝑟 ⊆ ( O ‘𝑎)) | 
| 19 | 17, 18 | anim12i 613 | . . . . . . . . . 10
⊢ ((𝑙 ∈ 𝒫 ( O
‘𝑎) ∧ 𝑟 ∈ 𝒫 ( O
‘𝑎)) → (𝑙 ⊆ ( O ‘𝑎) ∧ 𝑟 ⊆ ( O ‘𝑎))) | 
| 20 |  | unss 4190 | . . . . . . . . . 10
⊢ ((𝑙 ⊆ ( O ‘𝑎) ∧ 𝑟 ⊆ ( O ‘𝑎)) ↔ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) | 
| 21 | 19, 20 | sylib 218 | . . . . . . . . 9
⊢ ((𝑙 ∈ 𝒫 ( O
‘𝑎) ∧ 𝑟 ∈ 𝒫 ( O
‘𝑎)) → (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) | 
| 22 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) ∧ 𝑙 <<s 𝑟) → 𝑙 <<s 𝑟) | 
| 23 |  | simplll 775 | . . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) ∧ 𝑙 <<s 𝑟) → 𝑎 ∈ On) | 
| 24 |  | dfss3 3972 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎) ↔ ∀𝑧 ∈ (𝑙 ∪ 𝑟)𝑧 ∈ ( O ‘𝑎)) | 
| 25 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑧 → ( bday
‘𝑦) = ( bday ‘𝑧)) | 
| 26 | 25 | sseq1d 4015 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑧 → (( bday
‘𝑦) ⊆
𝑏 ↔ ( bday ‘𝑧) ⊆ 𝑏)) | 
| 27 | 26 | rspccv 3619 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈ (
M ‘𝑏)( bday ‘𝑦) ⊆ 𝑏 → (𝑧 ∈ ( M ‘𝑏) → ( bday
‘𝑧) ⊆
𝑏)) | 
| 28 | 27 | ralimi 3083 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑏 ∈
𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏 → ∀𝑏 ∈ 𝑎 (𝑧 ∈ ( M ‘𝑏) → ( bday
‘𝑧) ⊆
𝑏)) | 
| 29 |  | rexim 3087 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑏 ∈
𝑎 (𝑧 ∈ ( M ‘𝑏) → ( bday
‘𝑧) ⊆
𝑏) → (∃𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘𝑏) → ∃𝑏 ∈ 𝑎 ( bday
‘𝑧) ⊆
𝑏)) | 
| 30 | 28, 29 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑏 ∈
𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏 → (∃𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘𝑏) → ∃𝑏 ∈ 𝑎 ( bday
‘𝑧) ⊆
𝑏)) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → (∃𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘𝑏) → ∃𝑏 ∈ 𝑎 ( bday
‘𝑧) ⊆
𝑏)) | 
| 32 |  | elold 27908 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ On → (𝑧 ∈ ( O ‘𝑎) ↔ ∃𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘𝑏))) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → (𝑧 ∈ ( O ‘𝑎) ↔ ∃𝑏 ∈ 𝑎 𝑧 ∈ ( M ‘𝑏))) | 
| 34 |  | bdayelon 27821 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ( bday ‘𝑧) ∈ On | 
| 35 |  | onelssex 6432 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((( bday ‘𝑧) ∈ On ∧ 𝑎 ∈ On) → ((
bday ‘𝑧)
∈ 𝑎 ↔
∃𝑏 ∈ 𝑎 ( bday
‘𝑧) ⊆
𝑏)) | 
| 36 | 34, 35 | mpan 690 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ On → (( bday ‘𝑧) ∈ 𝑎 ↔ ∃𝑏 ∈ 𝑎 ( bday
‘𝑧) ⊆
𝑏)) | 
| 37 | 36 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → (( bday ‘𝑧) ∈ 𝑎 ↔ ∃𝑏 ∈ 𝑎 ( bday
‘𝑧) ⊆
𝑏)) | 
| 38 | 31, 33, 37 | 3imtr4d 294 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → (𝑧 ∈ ( O ‘𝑎) → (
bday ‘𝑧)
∈ 𝑎)) | 
| 39 | 38 | ralimdv 3169 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → (∀𝑧 ∈ (𝑙 ∪ 𝑟)𝑧 ∈ ( O ‘𝑎) → ∀𝑧 ∈ (𝑙 ∪ 𝑟)( bday
‘𝑧) ∈
𝑎)) | 
| 40 | 24, 39 | biimtrid 242 | . . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → ((𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎) → ∀𝑧 ∈ (𝑙 ∪ 𝑟)( bday
‘𝑧) ∈
𝑎)) | 
| 41 | 40 | imp 406 | . . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) → ∀𝑧 ∈ (𝑙 ∪ 𝑟)( bday
‘𝑧) ∈
𝑎) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) ∧ 𝑙 <<s 𝑟) → ∀𝑧 ∈ (𝑙 ∪ 𝑟)( bday
‘𝑧) ∈
𝑎) | 
| 43 |  | bdayfun 27817 | . . . . . . . . . . . . . . . . 17
⊢ Fun  bday | 
| 44 |  | oldssno 27900 | . . . . . . . . . . . . . . . . . . 19
⊢ ( O
‘𝑎) ⊆  No | 
| 45 |  | sstr 3992 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎) ∧ ( O ‘𝑎) ⊆  No )
→ (𝑙 ∪ 𝑟) ⊆ 
No ) | 
| 46 | 44, 45 | mpan2 691 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎) → (𝑙 ∪ 𝑟) ⊆  No
) | 
| 47 |  | bdaydm 27819 | . . . . . . . . . . . . . . . . . 18
⊢ dom  bday  =  No | 
| 48 | 46, 47 | sseqtrrdi 4025 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎) → (𝑙 ∪ 𝑟) ⊆ dom  bday
) | 
| 49 |  | funimass4 6973 | . . . . . . . . . . . . . . . . 17
⊢ ((Fun
 bday  ∧ (𝑙 ∪ 𝑟) ⊆ dom  bday
) → (( bday  “ (𝑙 ∪ 𝑟)) ⊆ 𝑎 ↔ ∀𝑧 ∈ (𝑙 ∪ 𝑟)( bday
‘𝑧) ∈
𝑎)) | 
| 50 | 43, 48, 49 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ ((𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎) → (( bday
 “ (𝑙 ∪
𝑟)) ⊆ 𝑎 ↔ ∀𝑧 ∈ (𝑙 ∪ 𝑟)( bday
‘𝑧) ∈
𝑎)) | 
| 51 | 50 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) → (( bday
 “ (𝑙 ∪
𝑟)) ⊆ 𝑎 ↔ ∀𝑧 ∈ (𝑙 ∪ 𝑟)( bday
‘𝑧) ∈
𝑎)) | 
| 52 | 51 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) ∧ 𝑙 <<s 𝑟) → (( bday
 “ (𝑙 ∪
𝑟)) ⊆ 𝑎 ↔ ∀𝑧 ∈ (𝑙 ∪ 𝑟)( bday
‘𝑧) ∈
𝑎)) | 
| 53 | 42, 52 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) ∧ 𝑙 <<s 𝑟) → ( bday 
“ (𝑙 ∪ 𝑟)) ⊆ 𝑎) | 
| 54 |  | scutbdaybnd 27860 | . . . . . . . . . . . . 13
⊢ ((𝑙 <<s 𝑟 ∧ 𝑎 ∈ On ∧ ( bday
 “ (𝑙 ∪
𝑟)) ⊆ 𝑎) → (
bday ‘(𝑙 |s
𝑟)) ⊆ 𝑎) | 
| 55 | 22, 23, 53, 54 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) ∧ 𝑙 <<s 𝑟) → ( bday
‘(𝑙 |s 𝑟)) ⊆ 𝑎) | 
| 56 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ ((𝑙 |s 𝑟) = 𝑥 → ( bday
‘(𝑙 |s 𝑟)) = (
bday ‘𝑥)) | 
| 57 | 56 | sseq1d 4015 | . . . . . . . . . . . 12
⊢ ((𝑙 |s 𝑟) = 𝑥 → (( bday
‘(𝑙 |s 𝑟)) ⊆ 𝑎 ↔ ( bday
‘𝑥) ⊆
𝑎)) | 
| 58 | 55, 57 | syl5ibcom 245 | . . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) ∧ 𝑙 <<s 𝑟) → ((𝑙 |s 𝑟) = 𝑥 → ( bday
‘𝑥) ⊆
𝑎)) | 
| 59 | 58 | expimpd 453 | . . . . . . . . . 10
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) ∧ (𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎)) → ((𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ( bday
‘𝑥) ⊆
𝑎)) | 
| 60 | 59 | ex 412 | . . . . . . . . 9
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → ((𝑙 ∪ 𝑟) ⊆ ( O ‘𝑎) → ((𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ( bday
‘𝑥) ⊆
𝑎))) | 
| 61 | 21, 60 | syl5 34 | . . . . . . . 8
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → ((𝑙 ∈ 𝒫 ( O
‘𝑎) ∧ 𝑟 ∈ 𝒫 ( O
‘𝑎)) → ((𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ( bday
‘𝑥) ⊆
𝑎))) | 
| 62 | 61 | rexlimdvv 3212 | . . . . . . 7
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → (∃𝑙 ∈ 𝒫 ( O
‘𝑎)∃𝑟 ∈ 𝒫 ( O
‘𝑎)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) → ( bday
‘𝑥) ⊆
𝑎)) | 
| 63 | 16, 62 | sylbid 240 | . . . . . 6
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → (𝑥 ∈ ( M ‘𝑎) → (
bday ‘𝑥)
⊆ 𝑎)) | 
| 64 | 63 | ralrimiv 3145 | . . . . 5
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏) → ∀𝑥 ∈ ( M ‘𝑎)( bday
‘𝑥) ⊆
𝑎) | 
| 65 | 64 | ex 412 | . . . 4
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ∀𝑦 ∈ ( M ‘𝑏)( bday
‘𝑦) ⊆
𝑏 → ∀𝑥 ∈ ( M ‘𝑎)( bday
‘𝑥) ⊆
𝑎)) | 
| 66 | 11, 14, 65 | tfis3 7879 | . . 3
⊢ (𝐴 ∈ On → ∀𝑥 ∈ ( M ‘𝐴)( bday
‘𝑥) ⊆
𝐴) | 
| 67 |  | fveq2 6906 | . . . . 5
⊢ (𝑥 = 𝑋 → ( bday
‘𝑥) = ( bday ‘𝑋)) | 
| 68 | 67 | sseq1d 4015 | . . . 4
⊢ (𝑥 = 𝑋 → (( bday
‘𝑥) ⊆
𝐴 ↔ ( bday ‘𝑋) ⊆ 𝐴)) | 
| 69 | 68 | rspccv 3619 | . . 3
⊢
(∀𝑥 ∈ (
M ‘𝐴)( bday ‘𝑥) ⊆ 𝐴 → (𝑋 ∈ ( M ‘𝐴) → ( bday
‘𝑋) ⊆
𝐴)) | 
| 70 | 66, 69 | syl 17 | . 2
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) → (
bday ‘𝑋)
⊆ 𝐴)) | 
| 71 | 4, 70 | mpcom 38 | 1
⊢ (𝑋 ∈ ( M ‘𝐴) → (
bday ‘𝑋)
⊆ 𝐴) |