| Step | Hyp | Ref
| Expression |
| 1 | | bdayelon 27821 |
. . . . . . 7
⊢ ( bday ‘𝑥) ∈ On |
| 2 | 1 | onordi 6495 |
. . . . . 6
⊢ Ord
( bday ‘𝑥) |
| 3 | | bdayelon 27821 |
. . . . . . 7
⊢ ( bday ‘𝐴) ∈ On |
| 4 | 3 | onordi 6495 |
. . . . . 6
⊢ Ord
( bday ‘𝐴) |
| 5 | | ordtri2or 6482 |
. . . . . 6
⊢ ((Ord
( bday ‘𝑥) ∧ Ord ( bday
‘𝐴)) →
(( bday ‘𝑥) ∈ ( bday
‘𝐴) ∨
( bday ‘𝐴) ⊆ ( bday
‘𝑥))) |
| 6 | 2, 4, 5 | mp2an 692 |
. . . . 5
⊢ (( bday ‘𝑥) ∈ ( bday
‘𝐴) ∨
( bday ‘𝐴) ⊆ ( bday
‘𝑥)) |
| 7 | 6 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons ∧ 𝑥
<s 𝐴) → (( bday ‘𝑥) ∈ ( bday
‘𝐴) ∨
( bday ‘𝐴) ⊆ ( bday
‘𝑥))) |
| 8 | | madeun 27922 |
. . . . . . . . . 10
⊢ ( M
‘( bday ‘𝑥)) = (( O ‘( bday
‘𝑥)) ∪ ( N
‘( bday ‘𝑥))) |
| 9 | 8 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ 𝐴 ∈ (( O ‘(
bday ‘𝑥))
∪ ( N ‘( bday ‘𝑥)))) |
| 10 | | elun 4153 |
. . . . . . . . 9
⊢ (𝐴 ∈ (( O ‘( bday ‘𝑥)) ∪ ( N ‘(
bday ‘𝑥)))
↔ (𝐴 ∈ ( O
‘( bday ‘𝑥)) ∨ 𝐴 ∈ ( N ‘(
bday ‘𝑥)))) |
| 11 | 9, 10 | bitri 275 |
. . . . . . . 8
⊢ (𝐴 ∈ ( M ‘( bday ‘𝑥)) ↔ (𝐴 ∈ ( O ‘(
bday ‘𝑥)) ∨
𝐴 ∈ ( N ‘( bday ‘𝑥)))) |
| 12 | | lrold 27935 |
. . . . . . . . . . 11
⊢ (( L
‘𝑥) ∪ ( R
‘𝑥)) = ( O
‘( bday ‘𝑥)) |
| 13 | 12 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ↔ 𝐴 ∈ ( O ‘(
bday ‘𝑥))) |
| 14 | | elons 28276 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Ons ↔
(𝑥 ∈ No ∧ ( R ‘𝑥) = ∅)) |
| 15 | 14 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ Ons → (
R ‘𝑥) =
∅) |
| 16 | 15 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → ( R ‘𝑥) = ∅) |
| 17 | 16 | uneq2d 4168 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (( L ‘𝑥) ∪ ( R ‘𝑥)) = (( L ‘𝑥) ∪ ∅)) |
| 18 | | un0 4394 |
. . . . . . . . . . . . 13
⊢ (( L
‘𝑥) ∪ ∅) =
( L ‘𝑥) |
| 19 | 17, 18 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (( L ‘𝑥) ∪ ( R ‘𝑥)) = ( L ‘𝑥)) |
| 20 | 19 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
∈ (( L ‘𝑥) ∪
( R ‘𝑥)) ↔ 𝐴 ∈ ( L ‘𝑥))) |
| 21 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ 𝐴
∈ ( L ‘𝑥))
→ 𝐴 ∈ No ) |
| 22 | | onsno 28278 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ Ons →
𝑥 ∈ No ) |
| 23 | 22 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ 𝐴
∈ ( L ‘𝑥))
→ 𝑥 ∈ No ) |
| 24 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝑂 = 𝐴 → (𝑥𝑂 <s 𝑥 ↔ 𝐴 <s 𝑥)) |
| 25 | | leftval 27902 |
. . . . . . . . . . . . . . . 16
⊢ ( L
‘𝑥) = {𝑥𝑂 ∈ ( O
‘( bday ‘𝑥)) ∣ 𝑥𝑂 <s 𝑥} |
| 26 | 24, 25 | elrab2 3695 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ( L ‘𝑥) ↔ (𝐴 ∈ ( O ‘(
bday ‘𝑥))
∧ 𝐴 <s 𝑥)) |
| 27 | 26 | simprbi 496 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ( L ‘𝑥) → 𝐴 <s 𝑥) |
| 28 | 27 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ 𝐴
∈ ( L ‘𝑥))
→ 𝐴 <s 𝑥) |
| 29 | 21, 23, 28 | sltled 27814 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ 𝐴
∈ ( L ‘𝑥))
→ 𝐴 ≤s 𝑥) |
| 30 | 29 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
∈ ( L ‘𝑥) →
𝐴 ≤s 𝑥)) |
| 31 | 20, 30 | sylbid 240 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
∈ (( L ‘𝑥) ∪
( R ‘𝑥)) → 𝐴 ≤s 𝑥)) |
| 32 | 13, 31 | biimtrrid 243 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
∈ ( O ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥)) |
| 33 | | newbday 27940 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑥) ∈ On ∧ 𝐴 ∈ No )
→ (𝐴 ∈ ( N
‘( bday ‘𝑥)) ↔ ( bday
‘𝐴) = ( bday ‘𝑥))) |
| 34 | 1, 33 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
No → (𝐴 ∈
( N ‘( bday ‘𝑥)) ↔ ( bday
‘𝐴) = ( bday ‘𝑥))) |
| 35 | 34 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
∈ ( N ‘( bday ‘𝑥)) ↔ ( bday
‘𝐴) = ( bday ‘𝑥))) |
| 36 | | leftssold 27917 |
. . . . . . . . . . . . 13
⊢ ( L
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) |
| 37 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝐴) = ( bday
‘𝑥) → ( O
‘( bday ‘𝐴)) = ( O ‘( bday
‘𝑥))) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ ( bday ‘𝐴) = ( bday
‘𝑥)) → (
O ‘( bday ‘𝐴)) = ( O ‘( bday
‘𝑥))) |
| 39 | 15 | uneq2d 4168 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Ons → ((
L ‘𝑥) ∪ ( R
‘𝑥)) = (( L
‘𝑥) ∪
∅)) |
| 40 | 39, 12, 18 | 3eqtr3g 2800 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ Ons → (
O ‘( bday ‘𝑥)) = ( L ‘𝑥)) |
| 41 | 40 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ ( bday ‘𝐴) = ( bday
‘𝑥)) → (
O ‘( bday ‘𝑥)) = ( L ‘𝑥)) |
| 42 | 38, 41 | eqtr2d 2778 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ ( bday ‘𝐴) = ( bday
‘𝑥)) → (
L ‘𝑥) = ( O
‘( bday ‘𝐴))) |
| 43 | 36, 42 | sseqtrrid 4027 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ ( bday ‘𝐴) = ( bday
‘𝑥)) → (
L ‘𝐴) ⊆ ( L
‘𝑥)) |
| 44 | | slelss 27946 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝑥)) → (𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥))) |
| 45 | 22, 44 | syl3an2 1165 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons ∧ ( bday ‘𝐴) = ( bday
‘𝑥)) →
(𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥))) |
| 46 | 45 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ ( bday ‘𝐴) = ( bday
‘𝑥)) →
(𝐴 ≤s 𝑥 ↔ ( L ‘𝐴) ⊆ ( L ‘𝑥))) |
| 47 | 43, 46 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝑥 ∈
Ons) ∧ ( bday ‘𝐴) = ( bday
‘𝑥)) →
𝐴 ≤s 𝑥) |
| 48 | 47 | ex 412 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (( bday ‘𝐴) = ( bday
‘𝑥) →
𝐴 ≤s 𝑥)) |
| 49 | 35, 48 | sylbid 240 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
∈ ( N ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥)) |
| 50 | 32, 49 | jaod 860 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → ((𝐴
∈ ( O ‘( bday ‘𝑥)) ∨ 𝐴 ∈ ( N ‘(
bday ‘𝑥)))
→ 𝐴 ≤s 𝑥)) |
| 51 | 11, 50 | biimtrid 242 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
∈ ( M ‘( bday ‘𝑥)) → 𝐴 ≤s 𝑥)) |
| 52 | | madebday 27938 |
. . . . . . . . 9
⊢ ((( bday ‘𝑥) ∈ On ∧ 𝐴 ∈ No )
→ (𝐴 ∈ ( M
‘( bday ‘𝑥)) ↔ ( bday
‘𝐴) ⊆
( bday ‘𝑥))) |
| 53 | 1, 52 | mpan 690 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝐴 ∈
( M ‘( bday ‘𝑥)) ↔ ( bday
‘𝐴) ⊆
( bday ‘𝑥))) |
| 54 | 53 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
∈ ( M ‘( bday ‘𝑥)) ↔ ( bday
‘𝐴) ⊆
( bday ‘𝑥))) |
| 55 | | slenlt 27797 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
No ) → (𝐴 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴)) |
| 56 | 22, 55 | sylan2 593 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝐴
≤s 𝑥 ↔ ¬ 𝑥 <s 𝐴)) |
| 57 | 51, 54, 56 | 3imtr3d 293 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (( bday ‘𝐴) ⊆ ( bday ‘𝑥) → ¬ 𝑥 <s 𝐴)) |
| 58 | 57 | con2d 134 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons) → (𝑥
<s 𝐴 → ¬ ( bday ‘𝐴) ⊆ ( bday
‘𝑥))) |
| 59 | 58 | 3impia 1118 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons ∧ 𝑥
<s 𝐴) → ¬
( bday ‘𝐴) ⊆ ( bday
‘𝑥)) |
| 60 | 7, 59 | olcnd 878 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons ∧ 𝑥
<s 𝐴) → ( bday ‘𝑥) ∈ ( bday
‘𝐴)) |
| 61 | 22 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons ∧ 𝑥
<s 𝐴) → 𝑥 ∈
No ) |
| 62 | | oldbday 27939 |
. . . 4
⊢ ((( bday ‘𝐴) ∈ On ∧ 𝑥 ∈ No )
→ (𝑥 ∈ ( O
‘( bday ‘𝐴)) ↔ ( bday
‘𝑥) ∈
( bday ‘𝐴))) |
| 63 | 3, 61, 62 | sylancr 587 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons ∧ 𝑥
<s 𝐴) → (𝑥 ∈ ( O ‘( bday ‘𝐴)) ↔ ( bday
‘𝑥) ∈
( bday ‘𝐴))) |
| 64 | 60, 63 | mpbird 257 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
Ons ∧ 𝑥
<s 𝐴) → 𝑥 ∈ ( O ‘( bday ‘𝐴))) |
| 65 | 64 | rabssdv 4075 |
1
⊢ (𝐴 ∈
No → {𝑥 ∈
Ons ∣ 𝑥
<s 𝐴} ⊆ ( O
‘( bday ‘𝐴))) |