Step | Hyp | Ref
| Expression |
1 | | etasslt2 33649 |
. 2
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No
(𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
2 | | scutbday 33639 |
. . . . . 6
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
3 | 2 | adantr 484 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
4 | | bdayfn 33609 |
. . . . . . 7
⊢ bday Fn No
|
5 | | ssrab2 3969 |
. . . . . . 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 515 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)) |
10 | | sneq 4526 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → {𝑦} = {𝑥}) |
11 | 10 | breq2d 5042 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑥})) |
12 | 10 | breq1d 5040 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ({𝑦} <<s 𝐵 ↔ {𝑥} <<s 𝐵)) |
13 | 11, 12 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))) |
14 | 13 | elrab 3588 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))) |
15 | 6, 9, 14 | sylanbrc 586 |
. . . . . . 7
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → 𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) |
16 | | fnfvima 7006 |
. . . . . . 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 4851 |
. . . . . 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 3915 |
. . . 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 3887 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
23 | 22 | rexlimdvaa 3195 |
. 2
⊢ (𝐴 <<s 𝐵 → (∃𝑥 ∈ No
(𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
24 | 1, 23 | mpd 15 |
1
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |