| Step | Hyp | Ref
| Expression |
| 1 | | eqscut 27850 |
. 2
⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
→ ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)})))) |
| 2 | | eqss 3999 |
. . . . 5
⊢ (( bday ‘𝑋) = ∩ ( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ (( bday
‘𝑋) ⊆
∩ ( bday “
{𝑥 ∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ∧ ∩
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday
‘𝑋))) |
| 3 | | sneq 4636 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
| 4 | 3 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (𝐿 <<s {𝑥} ↔ 𝐿 <<s {𝑋})) |
| 5 | 3 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → ({𝑥} <<s 𝑅 ↔ {𝑋} <<s 𝑅)) |
| 6 | 4, 5 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅))) |
| 7 | 6 | elrab3 3693 |
. . . . . . . . . 10
⊢ (𝑋 ∈
No → (𝑋 ∈
{𝑥 ∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅))) |
| 8 | 7 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
→ (𝑋 ∈ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)} ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅))) |
| 9 | 8 | biimpar 477 |
. . . . . . . 8
⊢ (((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → 𝑋 ∈ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) |
| 10 | | bdayfn 27818 |
. . . . . . . . 9
⊢ bday Fn No
|
| 11 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)} ⊆ No
|
| 12 | | fnfvima 7253 |
. . . . . . . . 9
⊢ (( bday Fn No ∧ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)} ⊆ No
∧ 𝑋 ∈ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday
‘𝑋) ∈
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})) |
| 13 | 10, 11, 12 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝑋 ∈ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} → ( bday
‘𝑋) ∈
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})) |
| 14 | | intss1 4963 |
. . . . . . . 8
⊢ (( bday ‘𝑋) ∈ ( bday
“ {𝑥 ∈
No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ∩
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday
‘𝑋)) |
| 15 | 9, 13, 14 | 3syl 18 |
. . . . . . 7
⊢ (((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → ∩
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday
‘𝑋)) |
| 16 | 15 | biantrud 531 |
. . . . . 6
⊢ (((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → (( bday
‘𝑋) ⊆
∩ ( bday “
{𝑥 ∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ (( bday
‘𝑋) ⊆
∩ ( bday “
{𝑥 ∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ∧ ∩
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday
‘𝑋)))) |
| 17 | | ssint 4964 |
. . . . . . 7
⊢ (( bday ‘𝑋) ⊆ ∩
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∀𝑧 ∈ ( bday
“ {𝑥 ∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})( bday
‘𝑋) ⊆
𝑧) |
| 18 | | fvelimab 6981 |
. . . . . . . . . . . . . 14
⊢ (( bday Fn No ∧ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)} ⊆ No
) → (𝑧 ∈
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∃𝑦 ∈ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ( bday
‘𝑦) = 𝑧)) |
| 19 | 10, 11, 18 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (
bday “ {𝑥
∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∃𝑦 ∈ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ( bday
‘𝑦) = 𝑧) |
| 20 | | sneq 4636 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
| 21 | 20 | breq2d 5155 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐿 <<s {𝑥} ↔ 𝐿 <<s {𝑦})) |
| 22 | 20 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ({𝑥} <<s 𝑅 ↔ {𝑦} <<s 𝑅)) |
| 23 | 21, 22 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ↔ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅))) |
| 24 | 23 | rexrab 3702 |
. . . . . . . . . . . . 13
⊢
(∃𝑦 ∈
{𝑥 ∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ( bday
‘𝑦) = 𝑧 ↔ ∃𝑦 ∈
No ((𝐿 <<s
{𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧)) |
| 25 | 19, 24 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (
bday “ {𝑥
∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∃𝑦 ∈ No
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧)) |
| 26 | 25 | imbi1i 349 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (
bday “ {𝑥
∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday
‘𝑋) ⊆
𝑧) ↔ (∃𝑦 ∈
No ((𝐿 <<s
{𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧) → (
bday ‘𝑋)
⊆ 𝑧)) |
| 27 | | r19.23v 3183 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
No (((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧) → (
bday ‘𝑋)
⊆ 𝑧) ↔
(∃𝑦 ∈ No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧) → (
bday ‘𝑋)
⊆ 𝑧)) |
| 28 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑦) = 𝑧 ↔ 𝑧 = ( bday
‘𝑦)) |
| 29 | 28 | anbi1ci 626 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧) ↔ (𝑧 = ( bday
‘𝑦) ∧
(𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅))) |
| 30 | 29 | imbi1i 349 |
. . . . . . . . . . . . 13
⊢ ((((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧) → (
bday ‘𝑋)
⊆ 𝑧) ↔ ((𝑧 = ( bday
‘𝑦) ∧
(𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)) → ( bday
‘𝑋) ⊆
𝑧)) |
| 31 | | impexp 450 |
. . . . . . . . . . . . 13
⊢ (((𝑧 = ( bday
‘𝑦) ∧
(𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)) → ( bday
‘𝑋) ⊆
𝑧) ↔ (𝑧 = ( bday
‘𝑦) →
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧))) |
| 32 | 30, 31 | bitri 275 |
. . . . . . . . . . . 12
⊢ ((((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧) → (
bday ‘𝑋)
⊆ 𝑧) ↔ (𝑧 = ( bday
‘𝑦) →
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧))) |
| 33 | 32 | ralbii 3093 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
No (((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday
‘𝑦) = 𝑧) → (
bday ‘𝑋)
⊆ 𝑧) ↔
∀𝑦 ∈ No (𝑧 = ( bday
‘𝑦) →
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧))) |
| 34 | 26, 27, 33 | 3bitr2i 299 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (
bday “ {𝑥
∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday
‘𝑋) ⊆
𝑧) ↔ ∀𝑦 ∈
No (𝑧 = ( bday ‘𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧))) |
| 35 | 34 | albii 1819 |
. . . . . . . . 9
⊢
(∀𝑧(𝑧 ∈ (
bday “ {𝑥
∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday
‘𝑋) ⊆
𝑧) ↔ ∀𝑧∀𝑦 ∈ No
(𝑧 = ( bday ‘𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧))) |
| 36 | | df-ral 3062 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})( bday
‘𝑋) ⊆
𝑧 ↔ ∀𝑧(𝑧 ∈ ( bday
“ {𝑥 ∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday
‘𝑋) ⊆
𝑧)) |
| 37 | | ralcom4 3286 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
No ∀𝑧(𝑧 = ( bday
‘𝑦) →
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧)) ↔ ∀𝑧∀𝑦 ∈ No
(𝑧 = ( bday ‘𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧))) |
| 38 | 35, 36, 37 | 3bitr4i 303 |
. . . . . . . 8
⊢
(∀𝑧 ∈
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})( bday
‘𝑋) ⊆
𝑧 ↔ ∀𝑦 ∈
No ∀𝑧(𝑧 = ( bday
‘𝑦) →
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧))) |
| 39 | | fvex 6919 |
. . . . . . . . . 10
⊢ ( bday ‘𝑦) ∈ V |
| 40 | | sseq2 4010 |
. . . . . . . . . . 11
⊢ (𝑧 = ( bday
‘𝑦) →
(( bday ‘𝑋) ⊆ 𝑧 ↔ ( bday
‘𝑋) ⊆
( bday ‘𝑦))) |
| 41 | 40 | imbi2d 340 |
. . . . . . . . . 10
⊢ (𝑧 = ( bday
‘𝑦) →
(((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧) ↔ ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦)))) |
| 42 | 39, 41 | ceqsalv 3521 |
. . . . . . . . 9
⊢
(∀𝑧(𝑧 = ( bday
‘𝑦) →
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧)) ↔ ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦))) |
| 43 | 42 | ralbii 3093 |
. . . . . . . 8
⊢
(∀𝑦 ∈
No ∀𝑧(𝑧 = ( bday
‘𝑦) →
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
𝑧)) ↔ ∀𝑦 ∈
No ((𝐿 <<s
{𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦))) |
| 44 | 38, 43 | bitri 275 |
. . . . . . 7
⊢
(∀𝑧 ∈
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})( bday
‘𝑋) ⊆
𝑧 ↔ ∀𝑦 ∈
No ((𝐿 <<s
{𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦))) |
| 45 | 17, 44 | bitri 275 |
. . . . . 6
⊢ (( bday ‘𝑋) ⊆ ∩
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∀𝑦 ∈ No
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦))) |
| 46 | 16, 45 | bitr3di 286 |
. . . . 5
⊢ (((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → ((( bday
‘𝑋) ⊆
∩ ( bday “
{𝑥 ∈ No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ∧ ∩
( bday “ {𝑥 ∈ No
∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday
‘𝑋)) ↔
∀𝑦 ∈ No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦)))) |
| 47 | 2, 46 | bitrid 283 |
. . . 4
⊢ (((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → (( bday
‘𝑋) = ∩ ( bday “ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∀𝑦 ∈ No
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦)))) |
| 48 | 47 | pm5.32da 579 |
. . 3
⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
→ (((𝐿 <<s
{𝑋} ∧ {𝑋} <<s 𝑅) ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)})) ↔ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅) ∧ ∀𝑦 ∈ No
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦))))) |
| 49 | | df-3an 1089 |
. . 3
⊢ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)})) ↔ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅) ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)}))) |
| 50 | | df-3an 1089 |
. . 3
⊢ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 ∈ No
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦))) ↔ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅) ∧ ∀𝑦 ∈ No
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦)))) |
| 51 | 48, 49, 50 | 3bitr4g 314 |
. 2
⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
→ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday
‘𝑋) = ∩ ( bday “ {𝑥 ∈
No ∣ (𝐿
<<s {𝑥} ∧ {𝑥} <<s 𝑅)})) ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 ∈ No
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦))))) |
| 52 | 1, 51 | bitrd 279 |
1
⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No )
→ ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 ∈ No
((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday
‘𝑋) ⊆
( bday ‘𝑦))))) |