Step | Hyp | Ref
| Expression |
1 | | etasslt2 27175 |
. 2
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No
(𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
2 | | scutbday 27165 |
. . . . . 6
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
3 | 2 | adantr 482 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
4 | | bdayfn 27135 |
. . . . . . 7
⊢ bday Fn No
|
5 | | ssrab2 4038 |
. . . . . . 7
⊢ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
|
6 | | simprl 770 |
. . . . . . . 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 513 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)) |
10 | | sneq 4597 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → {𝑦} = {𝑥}) |
11 | 10 | breq2d 5118 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑥})) |
12 | 10 | breq1d 5116 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ({𝑦} <<s 𝐵 ↔ {𝑥} <<s 𝐵)) |
13 | 11, 12 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))) |
14 | 13 | elrab 3646 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))) |
15 | 6, 9, 14 | sylanbrc 584 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → 𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) |
16 | | fnfvima 7184 |
. . . . . . 7
⊢ (( bday Fn No ∧ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
∧ 𝑥 ∈ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday
‘𝑥) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
17 | 4, 5, 15, 16 | mp3an12i 1466 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘𝑥) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
18 | | intss1 4925 |
. . . . . 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 3983 |
. . . 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 3955 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
23 | 22 | rexlimdvaa 3150 |
. 2
⊢ (𝐴 <<s 𝐵 → (∃𝑥 ∈ No
(𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
24 | 1, 23 | mpd 15 |
1
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |