Step | Hyp | Ref
| Expression |
1 | | ssltleft 34054 |
. . 3
⊢ (𝑋 ∈
No → ( L ‘𝑋) <<s {𝑋}) |
2 | 1 | adantl 482 |
. 2
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ( L ‘𝑋)
<<s {𝑋}) |
3 | | ssltright 34055 |
. . 3
⊢ (𝑋 ∈
No → {𝑋}
<<s ( R ‘𝑋)) |
4 | 3 | adantl 482 |
. 2
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ {𝑋} <<s ( R
‘𝑋)) |
5 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑋 = 𝑤 → ( bday
‘𝑋) = ( bday ‘𝑤)) |
6 | | eqimss 3977 |
. . . . . . . . 9
⊢ (( bday ‘𝑋) = ( bday
‘𝑤) →
( bday ‘𝑋) ⊆ ( bday
‘𝑤)) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝑋 = 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤)) |
8 | 7 | a1i 11 |
. . . . . . 7
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)))) → (𝑋 = 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
9 | | ssltsep 33985 |
. . . . . . . . . 10
⊢ (( L
‘𝑋) <<s {𝑤} → ∀𝑥 ∈ ( L ‘𝑋)∀𝑦 ∈ {𝑤}𝑥 <s 𝑦) |
10 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑤 ∈ V |
11 | | breq2 5078 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝑥 <s 𝑦 ↔ 𝑥 <s 𝑤)) |
12 | 10, 11 | ralsn 4617 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
{𝑤}𝑥 <s 𝑦 ↔ 𝑥 <s 𝑤) |
13 | 12 | ralbii 3092 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈ (
L ‘𝑋)∀𝑦 ∈ {𝑤}𝑥 <s 𝑦 ↔ ∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤) |
14 | 9, 13 | sylib 217 |
. . . . . . . . 9
⊢ (( L
‘𝑋) <<s {𝑤} → ∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤) |
15 | | ssltsep 33985 |
. . . . . . . . . 10
⊢ ({𝑤} <<s ( R ‘𝑋) → ∀𝑦 ∈ {𝑤}∀𝑥 ∈ ( R ‘𝑋)𝑦 <s 𝑥) |
16 | | breq1 5077 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝑦 <s 𝑥 ↔ 𝑤 <s 𝑥)) |
17 | 16 | ralbidv 3112 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (∀𝑥 ∈ ( R ‘𝑋)𝑦 <s 𝑥 ↔ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥)) |
18 | 10, 17 | ralsn 4617 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
{𝑤}∀𝑥 ∈ ( R ‘𝑋)𝑦 <s 𝑥 ↔ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) |
19 | 15, 18 | sylib 217 |
. . . . . . . . 9
⊢ ({𝑤} <<s ( R ‘𝑋) → ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) |
20 | 14, 19 | anim12i 613 |
. . . . . . . 8
⊢ ((( L
‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → (∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥)) |
21 | | leftval 34047 |
. . . . . . . . . . . . . . 15
⊢ ( L
‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑧 <s 𝑋} |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈
No → ( L ‘𝑋) = {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑧 <s 𝑋}) |
23 | 22 | raleqdv 3348 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈
No → (∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ↔ ∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑧 <s 𝑋}𝑥 <s 𝑤)) |
24 | | rightval 34048 |
. . . . . . . . . . . . . . 15
⊢ ( R
‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧} |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈
No → ( R ‘𝑋) = {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}) |
26 | 25 | raleqdv 3348 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈
No → (∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥 ↔ ∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}𝑤 <s 𝑥)) |
27 | 23, 26 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈
No → ((∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) ↔ (∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑧 <s 𝑋}𝑥 <s 𝑤 ∧ ∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}𝑤 <s 𝑥))) |
28 | | breq1 5077 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑧 <s 𝑋 ↔ 𝑥 <s 𝑋)) |
29 | 28 | ralrab 3630 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
{𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑧 <s 𝑋}𝑥 <s 𝑤 ↔ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤)) |
30 | | breq2 5078 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑋 <s 𝑧 ↔ 𝑋 <s 𝑥)) |
31 | 30 | ralrab 3630 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
{𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}𝑤 <s 𝑥 ↔ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)) |
32 | 29, 31 | anbi12i 627 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
{𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑧 <s 𝑋}𝑥 <s 𝑤 ∧ ∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}𝑤 <s 𝑥) ↔ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥))) |
33 | 27, 32 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑋 ∈
No → ((∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) ↔ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) |
34 | 33 | ad2antlr 724 |
. . . . . . . . . 10
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ 𝑤 ∈ No ) → ((∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) ↔ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) |
35 | | simplrl 774 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → 𝑤 ∈ No
) |
36 | | sltirr 33949 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈
No → ¬ 𝑤
<s 𝑤) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → ¬ 𝑤 <s 𝑤) |
38 | | bdayelon 33971 |
. . . . . . . . . . . . . . . 16
⊢ ( bday ‘𝑋) ∈ On |
39 | | bdayelon 33971 |
. . . . . . . . . . . . . . . 16
⊢ ( bday ‘𝑤) ∈ On |
40 | | ontri1 6300 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑤)
∈ On) → (( bday ‘𝑋) ⊆ ( bday
‘𝑤) ↔
¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋))) |
41 | 38, 39, 40 | mp2an 689 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑋) ⊆ ( bday
‘𝑤) ↔
¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋)) |
42 | 41 | con2bii 358 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘𝑤) ∈ ( bday
‘𝑋) ↔
¬ ( bday ‘𝑋) ⊆ ( bday
‘𝑤)) |
43 | | simplll 772 |
. . . . . . . . . . . . . . . 16
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → ∀𝑏 ∈ ( bday
‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) |
44 | | madebdaylemold 34078 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑋) ∈ On ∧ ∀𝑏 ∈ ( bday
‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑤 ∈ No )
→ (( bday ‘𝑤) ∈ ( bday
‘𝑋) →
𝑤 ∈ ( O ‘( bday ‘𝑋)))) |
45 | 38, 43, 35, 44 | mp3an2i 1465 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → (( bday
‘𝑤) ∈
( bday ‘𝑋) → 𝑤 ∈ ( O ‘(
bday ‘𝑋)))) |
46 | | slttrine 33954 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈
No ∧ 𝑤 ∈
No ) → (𝑋 ≠ 𝑤 ↔ (𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋))) |
47 | 46 | ad2ant2lr 745 |
. . . . . . . . . . . . . . . . 17
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑋 ≠ 𝑤 ↔ (𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋))) |
48 | | simprrr 779 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)) |
49 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (𝑋 <s 𝑥 ↔ 𝑋 <s 𝑤)) |
50 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (𝑤 <s 𝑥 ↔ 𝑤 <s 𝑤)) |
51 | 49, 50 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → ((𝑋 <s 𝑥 → 𝑤 <s 𝑥) ↔ (𝑋 <s 𝑤 → 𝑤 <s 𝑤))) |
52 | 51 | rspccv 3558 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈ (
O ‘( bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑋 <s 𝑤 → 𝑤 <s 𝑤))) |
53 | 48, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑋 <s 𝑤 → 𝑤 <s 𝑤))) |
54 | 53 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑋 <s 𝑤 → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤))) |
55 | | simprrl 778 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤)) |
56 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (𝑥 <s 𝑋 ↔ 𝑤 <s 𝑋)) |
57 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (𝑥 <s 𝑤 ↔ 𝑤 <s 𝑤)) |
58 | 56, 57 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → ((𝑥 <s 𝑋 → 𝑥 <s 𝑤) ↔ (𝑤 <s 𝑋 → 𝑤 <s 𝑤))) |
59 | 58 | rspccv 3558 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈ (
O ‘( bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑤 <s 𝑋 → 𝑤 <s 𝑤))) |
60 | 55, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑤 <s 𝑋 → 𝑤 <s 𝑤))) |
61 | 60 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑤 <s 𝑋 → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤))) |
62 | 54, 61 | jaod 856 |
. . . . . . . . . . . . . . . . 17
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → ((𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤))) |
63 | 47, 62 | sylbid 239 |
. . . . . . . . . . . . . . . 16
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑋 ≠ 𝑤 → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤))) |
64 | 63 | imp 407 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤)) |
65 | 45, 64 | syld 47 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → (( bday
‘𝑤) ∈
( bday ‘𝑋) → 𝑤 <s 𝑤)) |
66 | 42, 65 | syl5bir 242 |
. . . . . . . . . . . . 13
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → (¬ ( bday
‘𝑋) ⊆
( bday ‘𝑤) → 𝑤 <s 𝑤)) |
67 | 37, 66 | mt3d 148 |
. . . . . . . . . . . 12
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → ( bday
‘𝑋) ⊆
( bday ‘𝑤)) |
68 | 67 | ex 413 |
. . . . . . . . . . 11
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
69 | 68 | expr 457 |
. . . . . . . . . 10
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ 𝑤 ∈ No ) → ((∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤)))) |
70 | 34, 69 | sylbid 239 |
. . . . . . . . 9
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ 𝑤 ∈ No ) → ((∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤)))) |
71 | 70 | impr 455 |
. . . . . . . 8
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥))) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
72 | 20, 71 | sylanr2 680 |
. . . . . . 7
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)))) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
73 | 8, 72 | pm2.61dne 3031 |
. . . . . 6
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)))) → ( bday
‘𝑋) ⊆
( bday ‘𝑤)) |
74 | 73 | expr 457 |
. . . . 5
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ 𝑤 ∈ No ) → ((( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
75 | 74 | ralrimiva 3103 |
. . . 4
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ∀𝑤 ∈
No ((( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
76 | | bdayfn 33968 |
. . . . . 6
⊢ bday Fn No
|
77 | | ssrab2 4013 |
. . . . . 6
⊢ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ⊆ No
|
78 | | fnssintima 33676 |
. . . . . 6
⊢ (( bday Fn No ∧ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ⊆ No
) → (( bday ‘𝑋) ⊆ ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ↔ ∀𝑤 ∈ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
79 | 76, 77, 78 | mp2an 689 |
. . . . 5
⊢ (( bday ‘𝑋) ⊆ ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ↔ ∀𝑤 ∈ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ( bday
‘𝑋) ⊆
( bday ‘𝑤)) |
80 | | sneq 4571 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → {𝑧} = {𝑤}) |
81 | 80 | breq2d 5086 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (( L ‘𝑋) <<s {𝑧} ↔ ( L ‘𝑋) <<s {𝑤})) |
82 | 80 | breq1d 5084 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → ({𝑧} <<s ( R ‘𝑋) ↔ {𝑤} <<s ( R ‘𝑋))) |
83 | 81, 82 | anbi12d 631 |
. . . . . 6
⊢ (𝑧 = 𝑤 → ((( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋)) ↔ (( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)))) |
84 | 83 | ralrab 3630 |
. . . . 5
⊢
(∀𝑤 ∈
{𝑧 ∈ No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ( bday
‘𝑋) ⊆
( bday ‘𝑤) ↔ ∀𝑤 ∈ No (((
L ‘𝑋) <<s
{𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → ( bday ‘𝑋) ⊆ ( bday
‘𝑤))) |
85 | 79, 84 | bitri 274 |
. . . 4
⊢ (( bday ‘𝑋) ⊆ ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ↔ ∀𝑤 ∈
No ((( L ‘𝑋)
<<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → ( bday ‘𝑋) ⊆ ( bday
‘𝑤))) |
86 | 75, 85 | sylibr 233 |
. . 3
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ( bday ‘𝑋) ⊆ ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})) |
87 | | sneq 4571 |
. . . . . . . 8
⊢ (𝑧 = 𝑋 → {𝑧} = {𝑋}) |
88 | 87 | breq2d 5086 |
. . . . . . 7
⊢ (𝑧 = 𝑋 → (( L ‘𝑋) <<s {𝑧} ↔ ( L ‘𝑋) <<s {𝑋})) |
89 | 87 | breq1d 5084 |
. . . . . . 7
⊢ (𝑧 = 𝑋 → ({𝑧} <<s ( R ‘𝑋) ↔ {𝑋} <<s ( R ‘𝑋))) |
90 | 88, 89 | anbi12d 631 |
. . . . . 6
⊢ (𝑧 = 𝑋 → ((( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋)) ↔ (( L ‘𝑋) <<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋)))) |
91 | | simpr 485 |
. . . . . 6
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ 𝑋 ∈ No ) |
92 | 2, 4 | jca 512 |
. . . . . 6
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ (( L ‘𝑋)
<<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋))) |
93 | 90, 91, 92 | elrabd 3626 |
. . . . 5
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ 𝑋 ∈ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) |
94 | | fnfvima 7109 |
. . . . 5
⊢ (( bday Fn No ∧ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ⊆ No
∧ 𝑋 ∈
{𝑧 ∈ No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) → ( bday
‘𝑋) ∈
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})) |
95 | 76, 77, 93, 94 | mp3an12i 1464 |
. . . 4
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ( bday ‘𝑋) ∈ ( bday
“ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})) |
96 | | intss1 4894 |
. . . 4
⊢ (( bday ‘𝑋) ∈ ( bday
“ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) → ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ⊆ ( bday ‘𝑋)) |
97 | 95, 96 | syl 17 |
. . 3
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ∩ ( bday
“ {𝑧 ∈ No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ⊆ ( bday
‘𝑋)) |
98 | 86, 97 | eqssd 3938 |
. 2
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ( bday ‘𝑋) = ∩ ( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})) |
99 | | lltropt 34056 |
. . . 4
⊢ (𝑋 ∈
No → ( L ‘𝑋) <<s ( R ‘𝑋)) |
100 | | eqscut 33999 |
. . . 4
⊢ ((( L
‘𝑋) <<s ( R
‘𝑋) ∧ 𝑋 ∈
No ) → ((( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋 ↔ (( L ‘𝑋) <<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋) ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})))) |
101 | 99, 100 | mpancom 685 |
. . 3
⊢ (𝑋 ∈
No → ((( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋 ↔ (( L ‘𝑋) <<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋) ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})))) |
102 | 101 | adantl 482 |
. 2
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ((( L ‘𝑋) |s (
R ‘𝑋)) = 𝑋 ↔ (( L ‘𝑋) <<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋) ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})))) |
103 | 2, 4, 98, 102 | mpbir3and 1341 |
1
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ (( L ‘𝑋) |s (
R ‘𝑋)) = 𝑋) |