Step | Hyp | Ref
| Expression |
1 | | madebdayim 33708 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ ( M ‘𝐴)) → ( bday ‘𝑋) ⊆ 𝐴) |
2 | 1 | ex 416 |
. . 3
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) → (
bday ‘𝑋)
⊆ 𝐴)) |
3 | 2 | adantr 484 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈
No ) → (𝑋
∈ ( M ‘𝐴) →
( bday ‘𝑋) ⊆ 𝐴)) |
4 | | sseq2 3903 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (( bday
‘𝑥) ⊆
𝑎 ↔ ( bday ‘𝑥) ⊆ 𝑏)) |
5 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ( M ‘𝑎) = ( M ‘𝑏)) |
6 | 5 | eleq2d 2818 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝑏))) |
7 | 4, 6 | imbi12d 348 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ((( bday
‘𝑥) ⊆
𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ (( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)))) |
8 | 7 | ralbidv 3109 |
. . . . 5
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑏 → 𝑥 ∈ ( M ‘𝑏)))) |
9 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ( bday
‘𝑥) = ( bday ‘𝑦)) |
10 | 9 | sseq1d 3908 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (( bday
‘𝑥) ⊆
𝑏 ↔ ( bday ‘𝑦) ⊆ 𝑏)) |
11 | | eleq1 2820 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘𝑏))) |
12 | 10, 11 | imbi12d 348 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)) ↔ (( bday
‘𝑦) ⊆
𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
13 | 12 | cbvralvw 3349 |
. . . . 5
⊢
(∀𝑥 ∈
No (( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)) ↔ ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) |
14 | 8, 13 | bitrdi 290 |
. . . 4
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
15 | | sseq2 3903 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (( bday
‘𝑥) ⊆
𝑎 ↔ ( bday ‘𝑥) ⊆ 𝐴)) |
16 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ( M ‘𝑎) = ( M ‘𝐴)) |
17 | 16 | eleq2d 2818 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝐴))) |
18 | 15, 17 | imbi12d 348 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((( bday
‘𝑥) ⊆
𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ (( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)))) |
19 | 18 | ralbidv 3109 |
. . . 4
⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝐴 → 𝑥 ∈ ( M ‘𝐴)))) |
20 | | bdayelon 33612 |
. . . . . . . . 9
⊢ ( bday ‘𝑥) ∈ On |
21 | | onsseleq 6213 |
. . . . . . . . 9
⊢ ((( bday ‘𝑥) ∈ On ∧ 𝑎 ∈ On) → ((
bday ‘𝑥)
⊆ 𝑎 ↔ (( bday ‘𝑥) ∈ 𝑎 ∨ ( bday
‘𝑥) = 𝑎))) |
22 | 20, 21 | mpan 690 |
. . . . . . . 8
⊢ (𝑎 ∈ On → (( bday ‘𝑥) ⊆ 𝑎 ↔ (( bday
‘𝑥) ∈
𝑎 ∨ ( bday ‘𝑥) = 𝑎))) |
23 | 22 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ⊆ 𝑎 ↔ (( bday
‘𝑥) ∈
𝑎 ∨ ( bday ‘𝑥) = 𝑎))) |
24 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ 𝑎 ∈
On) |
25 | | onelss 6214 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (( bday ‘𝑥) ∈ 𝑎 → ( bday
‘𝑥) ⊆
𝑎)) |
26 | 25 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ∈ 𝑎 → ( bday
‘𝑥) ⊆
𝑎)) |
27 | 26 | imp 410 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( bday
‘𝑥) ⊆
𝑎) |
28 | | madess 33697 |
. . . . . . . . . . 11
⊢ ((( bday ‘𝑥) ∈ On ∧ 𝑎 ∈ On ∧ ( bday
‘𝑥) ⊆
𝑎) → ( M ‘( bday ‘𝑥)) ⊆ ( M ‘𝑎)) |
29 | 20, 24, 27, 28 | mp3an2ani 1469 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( M ‘(
bday ‘𝑥))
⊆ ( M ‘𝑎)) |
30 | | ssid 3899 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑥) ⊆ ( bday
‘𝑥) |
31 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( bday
‘𝑥) ∈
𝑎) |
32 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → 𝑥 ∈ No
) |
33 | 31, 32 | jca 515 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → (( bday
‘𝑥) ∈
𝑎 ∧ 𝑥 ∈ No
)) |
34 | | simpllr 776 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) |
35 | | sseq2 3903 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ( bday
‘𝑥) →
(( bday ‘𝑦) ⊆ 𝑏 ↔ ( bday
‘𝑦) ⊆
( bday ‘𝑥))) |
36 | | fveq2 6674 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ( bday
‘𝑥) → ( M
‘𝑏) = ( M
‘( bday ‘𝑥))) |
37 | 36 | eleq2d 2818 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ( bday
‘𝑥) →
(𝑦 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘(
bday ‘𝑥)))) |
38 | 35, 37 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ( bday
‘𝑥) →
((( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ↔ (( bday
‘𝑦) ⊆
( bday ‘𝑥) → 𝑦 ∈ ( M ‘(
bday ‘𝑥))))) |
39 | | fveq2 6674 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ( bday
‘𝑦) = ( bday ‘𝑥)) |
40 | 39 | sseq1d 3908 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (( bday
‘𝑦) ⊆
( bday ‘𝑥) ↔ ( bday
‘𝑥) ⊆
( bday ‘𝑥))) |
41 | | eleq1 2820 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝑦 ∈ ( M ‘(
bday ‘𝑥))
↔ 𝑥 ∈ ( M
‘( bday ‘𝑥)))) |
42 | 40, 41 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((( bday
‘𝑦) ⊆
( bday ‘𝑥) → 𝑦 ∈ ( M ‘(
bday ‘𝑥)))
↔ (( bday ‘𝑥) ⊆ ( bday
‘𝑥) →
𝑥 ∈ ( M ‘( bday ‘𝑥))))) |
43 | 38, 42 | rspc2v 3536 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑥) ∈ 𝑎 ∧ 𝑥 ∈ No )
→ (∀𝑏 ∈
𝑎 ∀𝑦 ∈
No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) → (( bday
‘𝑥) ⊆
( bday ‘𝑥) → 𝑥 ∈ ( M ‘(
bday ‘𝑥))))) |
44 | 33, 34, 43 | sylc 65 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → (( bday
‘𝑥) ⊆
( bday ‘𝑥) → 𝑥 ∈ ( M ‘(
bday ‘𝑥)))) |
45 | 30, 44 | mpi 20 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → 𝑥 ∈ ( M ‘(
bday ‘𝑥))) |
46 | 29, 45 | sseldd 3878 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → 𝑥 ∈ ( M ‘𝑎)) |
47 | 46 | ex 416 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ∈ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
48 | | madebdaylemlrcut 33717 |
. . . . . . . . . . . 12
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( L ‘𝑥) |s (
R ‘𝑥)) = 𝑥) |
49 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( bday ‘𝑥) ∈ On) |
50 | | lltropt 33693 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( L ‘𝑥) <<s ( R ‘𝑥)) |
51 | | leftssold 33699 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( L ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))) |
52 | | rightssold 33700 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( R ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))) |
53 | | madecut 33703 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑥) ∈ On ∧ ( L ‘𝑥) <<s ( R ‘𝑥)) ∧ (( L ‘𝑥) ⊆ ( O ‘( bday ‘𝑥)) ∧ ( R ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))))
→ (( L ‘𝑥) |s (
R ‘𝑥)) ∈ ( M
‘( bday ‘𝑥))) |
54 | 49, 50, 51, 52, 53 | syl22anc 838 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈
No → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘(
bday ‘𝑥))) |
55 | 54 | adantl 485 |
. . . . . . . . . . . 12
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( L ‘𝑥) |s (
R ‘𝑥)) ∈ ( M
‘( bday ‘𝑥))) |
56 | 48, 55 | eqeltrrd 2834 |
. . . . . . . . . . 11
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘( bday ‘𝑥))) |
57 | | raleq 3310 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑥) = 𝑎 → (∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ↔ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
58 | 57 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑥) = 𝑎 → ((∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
↔ (∀𝑏 ∈
𝑎 ∀𝑦 ∈
No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No
))) |
59 | | fveq2 6674 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑥) = 𝑎 → ( M ‘(
bday ‘𝑥)) = (
M ‘𝑎)) |
60 | 59 | eleq2d 2818 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑥) = 𝑎 → (𝑥 ∈ ( M ‘(
bday ‘𝑥))
↔ 𝑥 ∈ ( M
‘𝑎))) |
61 | 58, 60 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑥) = 𝑎 → (((∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘( bday ‘𝑥))) ↔ ((∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘𝑎)))) |
62 | 56, 61 | mpbii 236 |
. . . . . . . . . 10
⊢ (( bday ‘𝑥) = 𝑎 → ((∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘𝑎))) |
63 | 62 | com12 32 |
. . . . . . . . 9
⊢
((∀𝑏 ∈
𝑎 ∀𝑦 ∈
No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) = 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
64 | 63 | adantll 714 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) = 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
65 | 47, 64 | jaod 858 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ ((( bday ‘𝑥) ∈ 𝑎 ∨ ( bday
‘𝑥) = 𝑎) → 𝑥 ∈ ( M ‘𝑎))) |
66 | 23, 65 | sylbid 243 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
67 | 66 | ralrimiva 3096 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) → ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
68 | 67 | ex 416 |
. . . 4
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) → ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)))) |
69 | 14, 19, 68 | tfis3 7591 |
. . 3
⊢ (𝐴 ∈ On → ∀𝑥 ∈
No (( bday ‘𝑥) ⊆ 𝐴 → 𝑥 ∈ ( M ‘𝐴))) |
70 | | fveq2 6674 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ( bday
‘𝑥) = ( bday ‘𝑋)) |
71 | 70 | sseq1d 3908 |
. . . . 5
⊢ (𝑥 = 𝑋 → (( bday
‘𝑥) ⊆
𝐴 ↔ ( bday ‘𝑋) ⊆ 𝐴)) |
72 | | eleq1 2820 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 ∈ ( M ‘𝐴) ↔ 𝑋 ∈ ( M ‘𝐴))) |
73 | 71, 72 | imbi12d 348 |
. . . 4
⊢ (𝑥 = 𝑋 → ((( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)) ↔ (( bday
‘𝑋) ⊆
𝐴 → 𝑋 ∈ ( M ‘𝐴)))) |
74 | 73 | rspccva 3525 |
. . 3
⊢
((∀𝑥 ∈
No (( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)) ∧ 𝑋 ∈ No )
→ (( bday ‘𝑋) ⊆ 𝐴 → 𝑋 ∈ ( M ‘𝐴))) |
75 | 69, 74 | sylan 583 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈
No ) → (( bday ‘𝑋) ⊆ 𝐴 → 𝑋 ∈ ( M ‘𝐴))) |
76 | 3, 75 | impbid 215 |
1
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈
No ) → (𝑋
∈ ( M ‘𝐴) ↔
( bday ‘𝑋) ⊆ 𝐴)) |