Step | Hyp | Ref
| Expression |
1 | | madebdayim 27382 |
. 2
⊢ (𝑋 ∈ ( M ‘𝐴) → (
bday ‘𝑋)
⊆ 𝐴) |
2 | | sseq2 4009 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (( bday
‘𝑥) ⊆
𝑎 ↔ ( bday ‘𝑥) ⊆ 𝑏)) |
3 | | fveq2 6892 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ( M ‘𝑎) = ( M ‘𝑏)) |
4 | 3 | eleq2d 2820 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝑏))) |
5 | 2, 4 | imbi12d 345 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ((( bday
‘𝑥) ⊆
𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ (( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)))) |
6 | 5 | ralbidv 3178 |
. . . . 5
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑏 → 𝑥 ∈ ( M ‘𝑏)))) |
7 | | fveq2 6892 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ( bday
‘𝑥) = ( bday ‘𝑦)) |
8 | 7 | sseq1d 4014 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (( bday
‘𝑥) ⊆
𝑏 ↔ ( bday ‘𝑦) ⊆ 𝑏)) |
9 | | eleq1 2822 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘𝑏))) |
10 | 8, 9 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)) ↔ (( bday
‘𝑦) ⊆
𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
11 | 10 | cbvralvw 3235 |
. . . . 5
⊢
(∀𝑥 ∈
No (( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)) ↔ ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) |
12 | 6, 11 | bitrdi 287 |
. . . 4
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
13 | | sseq2 4009 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (( bday
‘𝑥) ⊆
𝑎 ↔ ( bday ‘𝑥) ⊆ 𝐴)) |
14 | | fveq2 6892 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ( M ‘𝑎) = ( M ‘𝐴)) |
15 | 14 | eleq2d 2820 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝐴))) |
16 | 13, 15 | imbi12d 345 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((( bday
‘𝑥) ⊆
𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ (( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)))) |
17 | 16 | ralbidv 3178 |
. . . 4
⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝐴 → 𝑥 ∈ ( M ‘𝐴)))) |
18 | | bdayelon 27278 |
. . . . . . . . 9
⊢ ( bday ‘𝑥) ∈ On |
19 | | onsseleq 6406 |
. . . . . . . . 9
⊢ ((( bday ‘𝑥) ∈ On ∧ 𝑎 ∈ On) → ((
bday ‘𝑥)
⊆ 𝑎 ↔ (( bday ‘𝑥) ∈ 𝑎 ∨ ( bday
‘𝑥) = 𝑎))) |
20 | 18, 19 | mpan 689 |
. . . . . . . 8
⊢ (𝑎 ∈ On → (( bday ‘𝑥) ⊆ 𝑎 ↔ (( bday
‘𝑥) ∈
𝑎 ∨ ( bday ‘𝑥) = 𝑎))) |
21 | 20 | ad2antrr 725 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ⊆ 𝑎 ↔ (( bday
‘𝑥) ∈
𝑎 ∨ ( bday ‘𝑥) = 𝑎))) |
22 | | simpll 766 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ 𝑎 ∈
On) |
23 | | onelss 6407 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (( bday ‘𝑥) ∈ 𝑎 → ( bday
‘𝑥) ⊆
𝑎)) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ∈ 𝑎 → ( bday
‘𝑥) ⊆
𝑎)) |
25 | 24 | imp 408 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( bday
‘𝑥) ⊆
𝑎) |
26 | | madess 27371 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ On ∧ ( bday ‘𝑥) ⊆ 𝑎) → ( M ‘(
bday ‘𝑥))
⊆ ( M ‘𝑎)) |
27 | 22, 25, 26 | syl2an2r 684 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( M ‘(
bday ‘𝑥))
⊆ ( M ‘𝑎)) |
28 | | ssid 4005 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑥) ⊆ ( bday
‘𝑥) |
29 | | simpr 486 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( bday
‘𝑥) ∈
𝑎) |
30 | | simplr 768 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → 𝑥 ∈ No
) |
31 | 29, 30 | jca 513 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → (( bday
‘𝑥) ∈
𝑎 ∧ 𝑥 ∈ No
)) |
32 | | simpllr 775 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) |
33 | | sseq2 4009 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ( bday
‘𝑥) →
(( bday ‘𝑦) ⊆ 𝑏 ↔ ( bday
‘𝑦) ⊆
( bday ‘𝑥))) |
34 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ( bday
‘𝑥) → ( M
‘𝑏) = ( M
‘( bday ‘𝑥))) |
35 | 34 | eleq2d 2820 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ( bday
‘𝑥) →
(𝑦 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘(
bday ‘𝑥)))) |
36 | 33, 35 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ( bday
‘𝑥) →
((( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ↔ (( bday
‘𝑦) ⊆
( bday ‘𝑥) → 𝑦 ∈ ( M ‘(
bday ‘𝑥))))) |
37 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ( bday
‘𝑦) = ( bday ‘𝑥)) |
38 | 37 | sseq1d 4014 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (( bday
‘𝑦) ⊆
( bday ‘𝑥) ↔ ( bday
‘𝑥) ⊆
( bday ‘𝑥))) |
39 | | eleq1 2822 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝑦 ∈ ( M ‘(
bday ‘𝑥))
↔ 𝑥 ∈ ( M
‘( bday ‘𝑥)))) |
40 | 38, 39 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((( bday
‘𝑦) ⊆
( bday ‘𝑥) → 𝑦 ∈ ( M ‘(
bday ‘𝑥)))
↔ (( bday ‘𝑥) ⊆ ( bday
‘𝑥) →
𝑥 ∈ ( M ‘( bday ‘𝑥))))) |
41 | 36, 40 | rspc2v 3623 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑥) ∈ 𝑎 ∧ 𝑥 ∈ No )
→ (∀𝑏 ∈
𝑎 ∀𝑦 ∈
No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) → (( bday
‘𝑥) ⊆
( bday ‘𝑥) → 𝑥 ∈ ( M ‘(
bday ‘𝑥))))) |
42 | 31, 32, 41 | sylc 65 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → (( bday
‘𝑥) ⊆
( bday ‘𝑥) → 𝑥 ∈ ( M ‘(
bday ‘𝑥)))) |
43 | 28, 42 | mpi 20 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → 𝑥 ∈ ( M ‘(
bday ‘𝑥))) |
44 | 27, 43 | sseldd 3984 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → 𝑥 ∈ ( M ‘𝑎)) |
45 | 44 | ex 414 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ∈ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
46 | | madebdaylemlrcut 27393 |
. . . . . . . . . . . 12
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( L ‘𝑥) |s (
R ‘𝑥)) = 𝑥) |
47 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( bday ‘𝑥) ∈ On) |
48 | | lltropt 27367 |
. . . . . . . . . . . . . . 15
⊢ ( L
‘𝑥) <<s ( R
‘𝑥) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( L ‘𝑥) <<s ( R ‘𝑥)) |
50 | | leftssold 27373 |
. . . . . . . . . . . . . . 15
⊢ ( L
‘𝑥) ⊆ ( O
‘( bday ‘𝑥)) |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( L ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))) |
52 | | rightssold 27374 |
. . . . . . . . . . . . . . 15
⊢ ( R
‘𝑥) ⊆ ( O
‘( bday ‘𝑥)) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( R ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))) |
54 | | madecut 27377 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑥) ∈ On ∧ ( L ‘𝑥) <<s ( R ‘𝑥)) ∧ (( L ‘𝑥) ⊆ ( O ‘( bday ‘𝑥)) ∧ ( R ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))))
→ (( L ‘𝑥) |s (
R ‘𝑥)) ∈ ( M
‘( bday ‘𝑥))) |
55 | 47, 49, 51, 53, 54 | syl22anc 838 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈
No → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘(
bday ‘𝑥))) |
56 | 55 | adantl 483 |
. . . . . . . . . . . 12
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( L ‘𝑥) |s (
R ‘𝑥)) ∈ ( M
‘( bday ‘𝑥))) |
57 | 46, 56 | eqeltrrd 2835 |
. . . . . . . . . . 11
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘( bday ‘𝑥))) |
58 | | raleq 3323 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑥) = 𝑎 → (∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ↔ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
59 | 58 | anbi1d 631 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑥) = 𝑎 → ((∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
↔ (∀𝑏 ∈
𝑎 ∀𝑦 ∈
No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No
))) |
60 | | fveq2 6892 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑥) = 𝑎 → ( M ‘(
bday ‘𝑥)) = (
M ‘𝑎)) |
61 | 60 | eleq2d 2820 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑥) = 𝑎 → (𝑥 ∈ ( M ‘(
bday ‘𝑥))
↔ 𝑥 ∈ ( M
‘𝑎))) |
62 | 59, 61 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑥) = 𝑎 → (((∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘( bday ‘𝑥))) ↔ ((∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘𝑎)))) |
63 | 57, 62 | mpbii 232 |
. . . . . . . . . 10
⊢ (( bday ‘𝑥) = 𝑎 → ((∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘𝑎))) |
64 | 63 | com12 32 |
. . . . . . . . 9
⊢
((∀𝑏 ∈
𝑎 ∀𝑦 ∈
No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) = 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
65 | 64 | adantll 713 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) = 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
66 | 45, 65 | jaod 858 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ ((( bday ‘𝑥) ∈ 𝑎 ∨ ( bday
‘𝑥) = 𝑎) → 𝑥 ∈ ( M ‘𝑎))) |
67 | 21, 66 | sylbid 239 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
68 | 67 | ralrimiva 3147 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) → ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
69 | 68 | ex 414 |
. . . 4
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) → ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)))) |
70 | 12, 17, 69 | tfis3 7847 |
. . 3
⊢ (𝐴 ∈ On → ∀𝑥 ∈
No (( bday ‘𝑥) ⊆ 𝐴 → 𝑥 ∈ ( M ‘𝐴))) |
71 | | fveq2 6892 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ( bday
‘𝑥) = ( bday ‘𝑋)) |
72 | 71 | sseq1d 4014 |
. . . . 5
⊢ (𝑥 = 𝑋 → (( bday
‘𝑥) ⊆
𝐴 ↔ ( bday ‘𝑋) ⊆ 𝐴)) |
73 | | eleq1 2822 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 ∈ ( M ‘𝐴) ↔ 𝑋 ∈ ( M ‘𝐴))) |
74 | 72, 73 | imbi12d 345 |
. . . 4
⊢ (𝑥 = 𝑋 → ((( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)) ↔ (( bday
‘𝑋) ⊆
𝐴 → 𝑋 ∈ ( M ‘𝐴)))) |
75 | 74 | rspccva 3612 |
. . 3
⊢
((∀𝑥 ∈
No (( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)) ∧ 𝑋 ∈ No )
→ (( bday ‘𝑋) ⊆ 𝐴 → 𝑋 ∈ ( M ‘𝐴))) |
76 | 70, 75 | sylan 581 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈
No ) → (( bday ‘𝑋) ⊆ 𝐴 → 𝑋 ∈ ( M ‘𝐴))) |
77 | 1, 76 | impbid2 225 |
1
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈
No ) → (𝑋
∈ ( M ‘𝐴) ↔
( bday ‘𝑋) ⊆ 𝐴)) |