Step | Hyp | Ref
| Expression |
1 | | ssltleft 33683 |
. . 3
⊢ (𝑋 ∈
No → ( L ‘𝑋) <<s {𝑋}) |
2 | 1 | adantl 485 |
. 2
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ( L ‘𝑋)
<<s {𝑋}) |
3 | | ssltright 33684 |
. . 3
⊢ (𝑋 ∈
No → {𝑋}
<<s ( R ‘𝑋)) |
4 | 3 | adantl 485 |
. 2
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ {𝑋} <<s ( R
‘𝑋)) |
5 | | fveq2 6668 |
. . . . . . . . 9
⊢ (𝑋 = 𝑤 → ( bday
‘𝑋) = ( bday ‘𝑤)) |
6 | | eqimss 3931 |
. . . . . . . . 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 33618 |
. . . . . . . . . 10
⊢ (( L
‘𝑋) <<s {𝑤} → ∀𝑥 ∈ ( L ‘𝑋)∀𝑦 ∈ {𝑤}𝑥 <s 𝑦) |
10 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑤 ∈ V |
11 | | breq2 5031 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝑥 <s 𝑦 ↔ 𝑥 <s 𝑤)) |
12 | 10, 11 | ralsn 4569 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
{𝑤}𝑥 <s 𝑦 ↔ 𝑥 <s 𝑤) |
13 | 12 | ralbii 3080 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈ (
L ‘𝑋)∀𝑦 ∈ {𝑤}𝑥 <s 𝑦 ↔ ∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤) |
14 | 9, 13 | sylib 221 |
. . . . . . . . 9
⊢ (( L
‘𝑋) <<s {𝑤} → ∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤) |
15 | | ssltsep 33618 |
. . . . . . . . . 10
⊢ ({𝑤} <<s ( R ‘𝑋) → ∀𝑦 ∈ {𝑤}∀𝑥 ∈ ( R ‘𝑋)𝑦 <s 𝑥) |
16 | | breq1 5030 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝑦 <s 𝑥 ↔ 𝑤 <s 𝑥)) |
17 | 16 | ralbidv 3109 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (∀𝑥 ∈ ( R ‘𝑋)𝑦 <s 𝑥 ↔ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥)) |
18 | 10, 17 | ralsn 4569 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
{𝑤}∀𝑥 ∈ ( R ‘𝑋)𝑦 <s 𝑥 ↔ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) |
19 | 15, 18 | sylib 221 |
. . . . . . . . 9
⊢ ({𝑤} <<s ( R ‘𝑋) → ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) |
20 | 14, 19 | anim12i 616 |
. . . . . . . 8
⊢ ((( L
‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → (∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥)) |
21 | | leftval 33676 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈
No → ( L ‘𝑋) = {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑧 <s 𝑋}) |
22 | 21 | raleqdv 3315 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈
No → (∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ↔ ∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑧 <s 𝑋}𝑥 <s 𝑤)) |
23 | | rightval 33677 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈
No → ( R ‘𝑋) = {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}) |
24 | 23 | raleqdv 3315 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈
No → (∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥 ↔ ∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}𝑤 <s 𝑥)) |
25 | 22, 24 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈
No → ((∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) ↔ (∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑧 <s 𝑋}𝑥 <s 𝑤 ∧ ∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}𝑤 <s 𝑥))) |
26 | | breq1 5030 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑧 <s 𝑋 ↔ 𝑥 <s 𝑋)) |
27 | 26 | ralrab 3591 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
{𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑧 <s 𝑋}𝑥 <s 𝑤 ↔ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤)) |
28 | | breq2 5031 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑋 <s 𝑧 ↔ 𝑋 <s 𝑥)) |
29 | 28 | ralrab 3591 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
{𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}𝑤 <s 𝑥 ↔ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)) |
30 | 27, 29 | anbi12i 630 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
{𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑧 <s 𝑋}𝑥 <s 𝑤 ∧ ∀𝑥 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}𝑤 <s 𝑥) ↔ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥))) |
31 | 25, 30 | bitrdi 290 |
. . . . . . . . . . 11
⊢ (𝑋 ∈
No → ((∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) ↔ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) |
32 | 31 | ad2antlr 727 |
. . . . . . . . . 10
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ 𝑤 ∈ No ) → ((∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) ↔ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) |
33 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → 𝑤 ∈ No
) |
34 | | sltirr 33582 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈
No → ¬ 𝑤
<s 𝑤) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → ¬ 𝑤 <s 𝑤) |
36 | | bdayelon 33604 |
. . . . . . . . . . . . . . . 16
⊢ ( bday ‘𝑋) ∈ On |
37 | | bdayelon 33604 |
. . . . . . . . . . . . . . . 16
⊢ ( bday ‘𝑤) ∈ On |
38 | | ontri1 6200 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑤)
∈ On) → (( bday ‘𝑋) ⊆ ( bday
‘𝑤) ↔
¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋))) |
39 | 36, 37, 38 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑋) ⊆ ( bday
‘𝑤) ↔
¬ ( bday ‘𝑤) ∈ ( bday
‘𝑋)) |
40 | 39 | con2bii 361 |
. . . . . . . . . . . . . 14
⊢ (( bday ‘𝑤) ∈ ( bday
‘𝑋) ↔
¬ ( bday ‘𝑋) ⊆ ( bday
‘𝑤)) |
41 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → ∀𝑏 ∈ ( bday
‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏))) |
42 | | madebdaylemold 33708 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑋) ∈ On ∧ ∀𝑏 ∈ ( bday
‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑤 ∈ No )
→ (( bday ‘𝑤) ∈ ( bday
‘𝑋) →
𝑤 ∈ ( O ‘( bday ‘𝑋)))) |
43 | 36, 41, 33, 42 | mp3an2i 1467 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → (( bday
‘𝑤) ∈
( bday ‘𝑋) → 𝑤 ∈ ( O ‘(
bday ‘𝑋)))) |
44 | | slttrine 33587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈
No ∧ 𝑤 ∈
No ) → (𝑋 ≠ 𝑤 ↔ (𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋))) |
45 | 44 | ad2ant2lr 748 |
. . . . . . . . . . . . . . . . 17
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑋 ≠ 𝑤 ↔ (𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋))) |
46 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)) |
47 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (𝑋 <s 𝑥 ↔ 𝑋 <s 𝑤)) |
48 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (𝑤 <s 𝑥 ↔ 𝑤 <s 𝑤)) |
49 | 47, 48 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → ((𝑋 <s 𝑥 → 𝑤 <s 𝑥) ↔ (𝑋 <s 𝑤 → 𝑤 <s 𝑤))) |
50 | 49 | rspccv 3521 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈ (
O ‘( bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑋 <s 𝑤 → 𝑤 <s 𝑤))) |
51 | 46, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑋 <s 𝑤 → 𝑤 <s 𝑤))) |
52 | 51 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑋 <s 𝑤 → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤))) |
53 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤)) |
54 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (𝑥 <s 𝑋 ↔ 𝑤 <s 𝑋)) |
55 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (𝑥 <s 𝑤 ↔ 𝑤 <s 𝑤)) |
56 | 54, 55 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → ((𝑥 <s 𝑋 → 𝑥 <s 𝑤) ↔ (𝑤 <s 𝑋 → 𝑤 <s 𝑤))) |
57 | 56 | rspccv 3521 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈ (
O ‘( bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑤 <s 𝑋 → 𝑤 <s 𝑤))) |
58 | 53, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑤 <s 𝑋 → 𝑤 <s 𝑤))) |
59 | 58 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑤 <s 𝑋 → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤))) |
60 | 52, 59 | jaod 858 |
. . . . . . . . . . . . . . . . 17
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → ((𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤))) |
61 | 45, 60 | sylbid 243 |
. . . . . . . . . . . . . . . 16
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑋 ≠ 𝑤 → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤))) |
62 | 61 | imp 410 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → (𝑤 ∈ ( O ‘(
bday ‘𝑋))
→ 𝑤 <s 𝑤)) |
63 | 43, 62 | syld 47 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → (( bday
‘𝑤) ∈
( bday ‘𝑋) → 𝑤 <s 𝑤)) |
64 | 40, 63 | syl5bir 246 |
. . . . . . . . . . . . 13
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → (¬ ( bday
‘𝑋) ⊆
( bday ‘𝑤) → 𝑤 <s 𝑤)) |
65 | 35, 64 | mt3d 150 |
. . . . . . . . . . . 12
⊢
((((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) ∧ 𝑋 ≠ 𝑤) → ( bday
‘𝑋) ⊆
( bday ‘𝑤)) |
66 | 65 | ex 416 |
. . . . . . . . . . 11
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)))) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
67 | 66 | expr 460 |
. . . . . . . . . 10
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ 𝑤 ∈ No ) → ((∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑥 <s 𝑋 → 𝑥 <s 𝑤) ∧ ∀𝑥 ∈ ( O ‘(
bday ‘𝑋))(𝑋 <s 𝑥 → 𝑤 <s 𝑥)) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤)))) |
68 | 32, 67 | sylbid 243 |
. . . . . . . . 9
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ 𝑤 ∈ No ) → ((∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤)))) |
69 | 68 | impr 458 |
. . . . . . . 8
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (∀𝑥 ∈ ( L ‘𝑋)𝑥 <s 𝑤 ∧ ∀𝑥 ∈ ( R ‘𝑋)𝑤 <s 𝑥))) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
70 | 20, 69 | sylanr2 683 |
. . . . . . 7
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)))) → (𝑋 ≠ 𝑤 → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
71 | 8, 70 | pm2.61dne 3020 |
. . . . . 6
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ (𝑤 ∈ No ∧ (( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)))) → ( bday
‘𝑋) ⊆
( bday ‘𝑤)) |
72 | 71 | expr 460 |
. . . . 5
⊢
(((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
∧ 𝑤 ∈ No ) → ((( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
73 | 72 | ralrimiva 3096 |
. . . 4
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ∀𝑤 ∈
No ((( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
74 | | bdayfn 33601 |
. . . . . 6
⊢ bday Fn No
|
75 | | ssrab2 3967 |
. . . . . 6
⊢ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ⊆ No
|
76 | | fnssintima 33241 |
. . . . . 6
⊢ (( bday Fn No ∧ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ⊆ No
) → (( bday ‘𝑋) ⊆ ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ↔ ∀𝑤 ∈ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ( bday
‘𝑋) ⊆
( bday ‘𝑤))) |
77 | 74, 75, 76 | mp2an 692 |
. . . . 5
⊢ (( bday ‘𝑋) ⊆ ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ↔ ∀𝑤 ∈ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ( bday
‘𝑋) ⊆
( bday ‘𝑤)) |
78 | | sneq 4523 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → {𝑧} = {𝑤}) |
79 | 78 | breq2d 5039 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (( L ‘𝑋) <<s {𝑧} ↔ ( L ‘𝑋) <<s {𝑤})) |
80 | 78 | breq1d 5037 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → ({𝑧} <<s ( R ‘𝑋) ↔ {𝑤} <<s ( R ‘𝑋))) |
81 | 79, 80 | anbi12d 634 |
. . . . . 6
⊢ (𝑧 = 𝑤 → ((( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋)) ↔ (( L ‘𝑋) <<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)))) |
82 | 81 | ralrab 3591 |
. . . . 5
⊢
(∀𝑤 ∈
{𝑧 ∈ No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ( bday
‘𝑋) ⊆
( bday ‘𝑤) ↔ ∀𝑤 ∈ No (((
L ‘𝑋) <<s
{𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → ( bday ‘𝑋) ⊆ ( bday
‘𝑤))) |
83 | 77, 82 | bitri 278 |
. . . 4
⊢ (( bday ‘𝑋) ⊆ ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ↔ ∀𝑤 ∈
No ((( L ‘𝑋)
<<s {𝑤} ∧ {𝑤} <<s ( R ‘𝑋)) → ( bday ‘𝑋) ⊆ ( bday
‘𝑤))) |
84 | 73, 83 | sylibr 237 |
. . 3
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ( bday ‘𝑋) ⊆ ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})) |
85 | | sneq 4523 |
. . . . . . . 8
⊢ (𝑧 = 𝑋 → {𝑧} = {𝑋}) |
86 | 85 | breq2d 5039 |
. . . . . . 7
⊢ (𝑧 = 𝑋 → (( L ‘𝑋) <<s {𝑧} ↔ ( L ‘𝑋) <<s {𝑋})) |
87 | 85 | breq1d 5037 |
. . . . . . 7
⊢ (𝑧 = 𝑋 → ({𝑧} <<s ( R ‘𝑋) ↔ {𝑋} <<s ( R ‘𝑋))) |
88 | 86, 87 | anbi12d 634 |
. . . . . 6
⊢ (𝑧 = 𝑋 → ((( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋)) ↔ (( L ‘𝑋) <<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋)))) |
89 | | simpr 488 |
. . . . . 6
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ 𝑋 ∈ No ) |
90 | 2, 4 | jca 515 |
. . . . . 6
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ (( L ‘𝑋)
<<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋))) |
91 | 88, 89, 90 | elrabd 3587 |
. . . . 5
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ 𝑋 ∈ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) |
92 | | fnfvima 7000 |
. . . . 5
⊢ (( bday Fn No ∧ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))} ⊆ No
∧ 𝑋 ∈
{𝑧 ∈ No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) → ( bday
‘𝑋) ∈
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})) |
93 | 74, 75, 91, 92 | mp3an12i 1466 |
. . . 4
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ( bday ‘𝑋) ∈ ( bday
“ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})) |
94 | | intss1 4848 |
. . . 4
⊢ (( bday ‘𝑋) ∈ ( bday
“ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) → ∩
( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ⊆ ( bday ‘𝑋)) |
95 | 93, 94 | syl 17 |
. . 3
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ∩ ( bday
“ {𝑧 ∈ No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))}) ⊆ ( bday
‘𝑋)) |
96 | 84, 95 | eqssd 3892 |
. 2
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ( bday ‘𝑋) = ∩ ( bday “ {𝑧 ∈ No
∣ (( L ‘𝑋)
<<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})) |
97 | | lltropt 33685 |
. . . 4
⊢ (𝑋 ∈
No → ( L ‘𝑋) <<s ( R ‘𝑋)) |
98 | | eqscut 33632 |
. . . 4
⊢ ((( L
‘𝑋) <<s ( R
‘𝑋) ∧ 𝑋 ∈
No ) → ((( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋 ↔ (( L ‘𝑋) <<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋) ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})))) |
99 | 97, 98 | mpancom 688 |
. . 3
⊢ (𝑋 ∈
No → ((( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋 ↔ (( L ‘𝑋) <<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋) ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})))) |
100 | 99 | adantl 485 |
. 2
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ ((( L ‘𝑋) |s (
R ‘𝑋)) = 𝑋 ↔ (( L ‘𝑋) <<s {𝑋} ∧ {𝑋} <<s ( R ‘𝑋) ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑧 ∈
No ∣ (( L ‘𝑋) <<s {𝑧} ∧ {𝑧} <<s ( R ‘𝑋))})))) |
101 | 2, 4, 96, 100 | mpbir3and 1343 |
1
⊢
((∀𝑏 ∈
( bday ‘𝑋)∀𝑦 ∈ No
(( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No )
→ (( L ‘𝑋) |s (
R ‘𝑋)) = 𝑋) |