| Step | Hyp | Ref
| Expression |
| 1 | | etasslt2 27859 |
. 2
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No
(𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
| 2 | | scutbday 27849 |
. . . . . 6
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
| 3 | 2 | adantr 480 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
| 4 | | bdayfn 27818 |
. . . . . . 7
⊢ bday Fn No
|
| 5 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
|
| 6 | | simprl 771 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → 𝑥 ∈ No
) |
| 7 | | simprr1 1222 |
. . . . . . . . 9
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → 𝐴 <<s {𝑥}) |
| 8 | | simprr2 1223 |
. . . . . . . . 9
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → {𝑥} <<s 𝐵) |
| 9 | 7, 8 | jca 511 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)) |
| 10 | | sneq 4636 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → {𝑦} = {𝑥}) |
| 11 | 10 | breq2d 5155 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑥})) |
| 12 | 10 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ({𝑦} <<s 𝐵 ↔ {𝑥} <<s 𝐵)) |
| 13 | 11, 12 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))) |
| 14 | 13 | elrab 3692 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))) |
| 15 | 6, 9, 14 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → 𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) |
| 16 | | fnfvima 7253 |
. . . . . . 7
⊢ (( bday Fn No ∧ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
∧ 𝑥 ∈ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday
‘𝑥) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
| 17 | 4, 5, 15, 16 | mp3an12i 1467 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘𝑥) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
| 18 | | intss1 4963 |
. . . . . 6
⊢ (( bday ‘𝑥) ∈ ( bday
“ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ∩
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday
‘𝑥)) |
| 19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ∩
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday
‘𝑥)) |
| 20 | 3, 19 | eqsstrd 4018 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥)) |
| 21 | | simprr3 1224 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) |
| 22 | 20, 21 | sstrd 3994 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
| 23 | 22 | rexlimdvaa 3156 |
. 2
⊢ (𝐴 <<s 𝐵 → (∃𝑥 ∈ No
(𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
| 24 | 1, 23 | mpd 15 |
1
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |