| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | etasslt 27858 | . 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ 
No  (𝐴 <<s
{𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂)) | 
| 2 |  | simpl1 1192 | . . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈  No 
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝐴 <<s 𝐵) | 
| 3 |  | scutbday 27849 | . . . . 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 27818 | . . . . . 6
⊢  bday  Fn  No | 
| 6 |  | ssrab2 4080 | . . . . . 6
⊢ {𝑦 ∈ 
No  ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆  No | 
| 7 |  | sneq 4636 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → {𝑦} = {𝑥}) | 
| 8 | 7 | breq2d 5155 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑥})) | 
| 9 | 7 | breq1d 5153 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → ({𝑦} <<s 𝐵 ↔ {𝑥} <<s 𝐵)) | 
| 10 | 8, 9 | anbi12d 632 | . . . . . . 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 511 | . . . . . . 7
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈  No 
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)) | 
| 15 | 10, 11, 14 | elrabd 3694 | . . . . . 6
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈  No 
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → 𝑥 ∈ {𝑦 ∈  No 
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) | 
| 16 |  | fnfvima 7253 | . . . . . 6
⊢ (( bday  Fn  No  ∧ {𝑦 ∈ 
No  ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆  No 
∧ 𝑥 ∈ {𝑦 ∈ 
No  ∣ (𝐴
<<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday
‘𝑥) ∈
( bday  “ {𝑦 ∈  No 
∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) | 
| 17 | 5, 6, 15, 16 | mp3an12i 1467 | . . . . 5
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈  No 
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ( bday ‘𝑥) ∈ ( bday 
“ {𝑦 ∈  No  ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) | 
| 18 |  | intss1 4963 | . . . . 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 4018 | . . 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 3994 | . 2
⊢ (((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) ∧ (𝑥 ∈  No 
∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday
‘𝑥) ⊆
𝑂))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ 𝑂) | 
| 23 | 1, 22 | rexlimddv 3161 | 1
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ (
bday  “ (𝐴
∪ 𝐵)) ⊆ 𝑂) → (
bday ‘(𝐴 |s
𝐵)) ⊆ 𝑂) |