Step | Hyp | Ref
| Expression |
1 | | etasslt 33663 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈
No (𝐴 <<s
{𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂)) |
2 | | simpl1 1192 |
. . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝐴 <<s 𝐵) |
3 | | scutbday 33654 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
5 | | bdayfn 33624 |
. . . . . 6
⊢ bday Fn No
|
6 | | ssrab2 3979 |
. . . . . 6
⊢ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
|
7 | | sneq 4536 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → {𝑦} = {𝑥}) |
8 | 7 | breq2d 5052 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑥})) |
9 | 7 | breq1d 5050 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ({𝑦} <<s 𝐵 ↔ {𝑥} <<s 𝐵)) |
10 | 8, 9 | anbi12d 634 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))) |
11 | | simprl 771 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝑥 ∈
No ) |
12 | | simprr1 1222 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝐴 <<s {𝑥}) |
13 | | simprr2 1223 |
. . . . . . . 8
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → {𝑥} <<s 𝐵) |
14 | 12, 13 | jca 515 |
. . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)) |
15 | 10, 11, 14 | elrabd 3595 |
. . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝑥 ∈ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) |
16 | | fnfvima 7019 |
. . . . . 6
⊢ (( bday Fn No ∧ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
∧ 𝑥 ∈ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday
‘𝑥) ∈
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
17 | 5, 6, 15, 16 | mp3an12i 1466 |
. . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ( bday ‘𝑥) ∈ ( bday
“ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) |
18 | | intss1 4861 |
. . . . 5
⊢ (( bday ‘𝑥) ∈ ( bday
“ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ∩
( bday “ {𝑦 ∈ No
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday
‘𝑥)) |
19 | 17, 18 | syl 17 |
. . . 4
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ∩ ( bday “ {𝑦 ∈
No ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday
‘𝑥)) |
20 | 4, 19 | eqsstrd 3925 |
. . 3
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday
‘𝑥)) |
21 | | simprr3 1224 |
. . 3
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ( bday ‘𝑥) ⊆ 𝑂) |
22 | 20, 21 | sstrd 3897 |
. 2
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈ No
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ 𝑂) |
23 | 1, 22 | rexlimddv 3202 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → (
bday ‘(𝐴 |s
𝐵)) ⊆ 𝑂) |