Step | Hyp | Ref
| Expression |
1 | | madebdayim 34070 |
. 2
⊢ (𝑋 ∈ ( M ‘𝐴) → (
bday ‘𝑋)
⊆ 𝐴) |
2 | | sseq2 3947 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (( bday
‘𝑥) ⊆
𝑎 ↔ ( bday ‘𝑥) ⊆ 𝑏)) |
3 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ( M ‘𝑎) = ( M ‘𝑏)) |
4 | 3 | eleq2d 2824 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝑏))) |
5 | 2, 4 | imbi12d 345 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ((( bday
‘𝑥) ⊆
𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ (( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)))) |
6 | 5 | ralbidv 3112 |
. . . . 5
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑏 → 𝑥 ∈ ( M ‘𝑏)))) |
7 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ( bday
‘𝑥) = ( bday ‘𝑦)) |
8 | 7 | sseq1d 3952 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (( bday
‘𝑥) ⊆
𝑏 ↔ ( bday ‘𝑦) ⊆ 𝑏)) |
9 | | eleq1 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘𝑏))) |
10 | 8, 9 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)) ↔ (( bday
‘𝑦) ⊆
𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
11 | 10 | cbvralvw 3383 |
. . . . 5
⊢
(∀𝑥 ∈
No (( bday
‘𝑥) ⊆
𝑏 → 𝑥 ∈ ( M ‘𝑏)) ↔ ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) |
12 | 6, 11 | bitrdi 287 |
. . . 4
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
13 | | sseq2 3947 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (( bday
‘𝑥) ⊆
𝑎 ↔ ( bday ‘𝑥) ⊆ 𝐴)) |
14 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ( M ‘𝑎) = ( M ‘𝐴)) |
15 | 14 | eleq2d 2824 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑥 ∈ ( M ‘𝑎) ↔ 𝑥 ∈ ( M ‘𝐴))) |
16 | 13, 15 | imbi12d 345 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((( bday
‘𝑥) ⊆
𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ (( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)))) |
17 | 16 | ralbidv 3112 |
. . . 4
⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)) ↔ ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝐴 → 𝑥 ∈ ( M ‘𝐴)))) |
18 | | bdayelon 33971 |
. . . . . . . . 9
⊢ ( bday ‘𝑥) ∈ On |
19 | | onsseleq 6307 |
. . . . . . . . 9
⊢ ((( bday ‘𝑥) ∈ On ∧ 𝑎 ∈ On) → ((
bday ‘𝑥)
⊆ 𝑎 ↔ (( bday ‘𝑥) ∈ 𝑎 ∨ ( bday
‘𝑥) = 𝑎))) |
20 | 18, 19 | mpan 687 |
. . . . . . . 8
⊢ (𝑎 ∈ On → (( bday ‘𝑥) ⊆ 𝑎 ↔ (( bday
‘𝑥) ∈
𝑎 ∨ ( bday ‘𝑥) = 𝑎))) |
21 | 20 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ⊆ 𝑎 ↔ (( bday
‘𝑥) ∈
𝑎 ∨ ( bday ‘𝑥) = 𝑎))) |
22 | | simpll 764 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ 𝑎 ∈
On) |
23 | | onelss 6308 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ On → (( bday ‘𝑥) ∈ 𝑎 → ( bday
‘𝑥) ⊆
𝑎)) |
24 | 23 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ∈ 𝑎 → ( bday
‘𝑥) ⊆
𝑎)) |
25 | 24 | imp 407 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( bday
‘𝑥) ⊆
𝑎) |
26 | | madess 34059 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ On ∧ ( bday ‘𝑥) ⊆ 𝑎) → ( M ‘(
bday ‘𝑥))
⊆ ( M ‘𝑎)) |
27 | 22, 25, 26 | syl2an2r 682 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( M ‘(
bday ‘𝑥))
⊆ ( M ‘𝑎)) |
28 | | ssid 3943 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑥) ⊆ ( bday
‘𝑥) |
29 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ( bday
‘𝑥) ∈
𝑎) |
30 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → 𝑥 ∈ No
) |
31 | 29, 30 | jca 512 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → (( bday
‘𝑥) ∈
𝑎 ∧ 𝑥 ∈ No
)) |
32 | | simpllr 773 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) |
33 | | sseq2 3947 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ( bday
‘𝑥) →
(( bday ‘𝑦) ⊆ 𝑏 ↔ ( bday
‘𝑦) ⊆
( bday ‘𝑥))) |
34 | | fveq2 6774 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ( bday
‘𝑥) → ( M
‘𝑏) = ( M
‘( bday ‘𝑥))) |
35 | 34 | eleq2d 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ( bday
‘𝑥) →
(𝑦 ∈ ( M ‘𝑏) ↔ 𝑦 ∈ ( M ‘(
bday ‘𝑥)))) |
36 | 33, 35 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ( bday
‘𝑥) →
((( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ↔ (( bday
‘𝑦) ⊆
( bday ‘𝑥) → 𝑦 ∈ ( M ‘(
bday ‘𝑥))))) |
37 | | fveq2 6774 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ( bday
‘𝑦) = ( bday ‘𝑥)) |
38 | 37 | sseq1d 3952 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (( bday
‘𝑦) ⊆
( bday ‘𝑥) ↔ ( bday
‘𝑥) ⊆
( bday ‘𝑥))) |
39 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝑦 ∈ ( M ‘(
bday ‘𝑥))
↔ 𝑥 ∈ ( M
‘( bday ‘𝑥)))) |
40 | 38, 39 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((( bday
‘𝑦) ⊆
( bday ‘𝑥) → 𝑦 ∈ ( M ‘(
bday ‘𝑥)))
↔ (( bday ‘𝑥) ⊆ ( bday
‘𝑥) →
𝑥 ∈ ( M ‘( bday ‘𝑥))))) |
41 | 36, 40 | rspc2v 3570 |
. . . . . . . . . . . 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 3922 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
∧ ( bday ‘𝑥) ∈ 𝑎) → 𝑥 ∈ ( M ‘𝑎)) |
45 | 44 | ex 413 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ∈ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
46 | | madebdaylemlrcut 34079 |
. . . . . . . . . . . 12
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( L ‘𝑥) |s (
R ‘𝑥)) = 𝑥) |
47 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( bday ‘𝑥) ∈ On) |
48 | | lltropt 34056 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( L ‘𝑥) <<s ( R ‘𝑥)) |
49 | | leftssold 34061 |
. . . . . . . . . . . . . . 15
⊢ ( L
‘𝑥) ⊆ ( O
‘( bday ‘𝑥)) |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( L ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))) |
51 | | rightssold 34062 |
. . . . . . . . . . . . . . 15
⊢ ( R
‘𝑥) ⊆ ( O
‘( bday ‘𝑥)) |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
No → ( R ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))) |
53 | | madecut 34065 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑥) ∈ On ∧ ( L ‘𝑥) <<s ( R ‘𝑥)) ∧ (( L ‘𝑥) ⊆ ( O ‘( bday ‘𝑥)) ∧ ( R ‘𝑥) ⊆ ( O ‘(
bday ‘𝑥))))
→ (( L ‘𝑥) |s (
R ‘𝑥)) ∈ ( M
‘( bday ‘𝑥))) |
54 | 47, 48, 50, 52, 53 | syl22anc 836 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈
No → (( L ‘𝑥) |s ( R ‘𝑥)) ∈ ( M ‘(
bday ‘𝑥))) |
55 | 54 | adantl 482 |
. . . . . . . . . . . 12
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( L ‘𝑥) |s (
R ‘𝑥)) ∈ ( M
‘( bday ‘𝑥))) |
56 | 46, 55 | eqeltrrd 2840 |
. . . . . . . . . . 11
⊢
((∀𝑏 ∈
( bday ‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘( bday ‘𝑥))) |
57 | | raleq 3342 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑥) = 𝑎 → (∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ↔ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)))) |
58 | 57 | anbi1d 630 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑥) = 𝑎 → ((∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
↔ (∀𝑏 ∈
𝑎 ∀𝑦 ∈
No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No
))) |
59 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑥) = 𝑎 → ( M ‘(
bday ‘𝑥)) = (
M ‘𝑎)) |
60 | 59 | eleq2d 2824 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑥) = 𝑎 → (𝑥 ∈ ( M ‘(
bday ‘𝑥))
↔ 𝑥 ∈ ( M
‘𝑎))) |
61 | 58, 60 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑥) = 𝑎 → (((∀𝑏 ∈ ( bday
‘𝑥)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘( bday ‘𝑥))) ↔ ((∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘𝑎)))) |
62 | 56, 61 | mpbii 232 |
. . . . . . . . . 10
⊢ (( bday ‘𝑥) = 𝑎 → ((∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ 𝑥 ∈ ( M
‘𝑎))) |
63 | 62 | com12 32 |
. . . . . . . . 9
⊢
((∀𝑏 ∈
𝑎 ∀𝑦 ∈
No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) = 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
64 | 63 | adantll 711 |
. . . . . . . 8
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) = 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
65 | 45, 64 | jaod 856 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ ((( bday ‘𝑥) ∈ 𝑎 ∨ ( bday
‘𝑥) = 𝑎) → 𝑥 ∈ ( M ‘𝑎))) |
66 | 21, 65 | sylbid 239 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) ∧ 𝑥 ∈ No )
→ (( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
67 | 66 | ralrimiva 3103 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) → ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎))) |
68 | 67 | ex 413 |
. . . 4
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) → ∀𝑥 ∈ No
(( bday ‘𝑥) ⊆ 𝑎 → 𝑥 ∈ ( M ‘𝑎)))) |
69 | 12, 17, 68 | tfis3 7704 |
. . 3
⊢ (𝐴 ∈ On → ∀𝑥 ∈
No (( bday ‘𝑥) ⊆ 𝐴 → 𝑥 ∈ ( M ‘𝐴))) |
70 | | fveq2 6774 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ( bday
‘𝑥) = ( bday ‘𝑋)) |
71 | 70 | sseq1d 3952 |
. . . . 5
⊢ (𝑥 = 𝑋 → (( bday
‘𝑥) ⊆
𝐴 ↔ ( bday ‘𝑋) ⊆ 𝐴)) |
72 | | eleq1 2826 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 ∈ ( M ‘𝐴) ↔ 𝑋 ∈ ( M ‘𝐴))) |
73 | 71, 72 | imbi12d 345 |
. . . 4
⊢ (𝑥 = 𝑋 → ((( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)) ↔ (( bday
‘𝑋) ⊆
𝐴 → 𝑋 ∈ ( M ‘𝐴)))) |
74 | 73 | rspccva 3560 |
. . 3
⊢
((∀𝑥 ∈
No (( bday
‘𝑥) ⊆
𝐴 → 𝑥 ∈ ( M ‘𝐴)) ∧ 𝑋 ∈ No )
→ (( bday ‘𝑋) ⊆ 𝐴 → 𝑋 ∈ ( M ‘𝐴))) |
75 | 69, 74 | sylan 580 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈
No ) → (( bday ‘𝑋) ⊆ 𝐴 → 𝑋 ∈ ( M ‘𝐴))) |
76 | 1, 75 | impbid2 225 |
1
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈
No ) → (𝑋
∈ ( M ‘𝐴) ↔
( bday ‘𝑋) ⊆ 𝐴)) |