| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | scutval 27845 | . . 3
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) = (℩𝑦 ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)}))) | 
| 2 | 1 | eqcomd 2743 | . 2
⊢ (𝐴 <<s 𝐵 → (℩𝑦 ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)})) = (𝐴 |s 𝐵)) | 
| 3 |  | scutcut 27846 | . . . 4
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈  No 
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) | 
| 4 |  | sneq 4636 | . . . . . . . 8
⊢ (𝑥 = (𝐴 |s 𝐵) → {𝑥} = {(𝐴 |s 𝐵)}) | 
| 5 | 4 | breq2d 5155 | . . . . . . 7
⊢ (𝑥 = (𝐴 |s 𝐵) → (𝐴 <<s {𝑥} ↔ 𝐴 <<s {(𝐴 |s 𝐵)})) | 
| 6 | 4 | breq1d 5153 | . . . . . . 7
⊢ (𝑥 = (𝐴 |s 𝐵) → ({𝑥} <<s 𝐵 ↔ {(𝐴 |s 𝐵)} <<s 𝐵)) | 
| 7 | 5, 6 | anbi12d 632 | . . . . . 6
⊢ (𝑥 = (𝐴 |s 𝐵) → ((𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵) ↔ (𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))) | 
| 8 | 7 | elrab 3692 | . . . . 5
⊢ ((𝐴 |s 𝐵) ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ↔ ((𝐴 |s 𝐵) ∈  No 
∧ (𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))) | 
| 9 |  | 3anass 1095 | . . . . 5
⊢ (((𝐴 |s 𝐵) ∈  No 
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵) ↔ ((𝐴 |s 𝐵) ∈  No 
∧ (𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))) | 
| 10 | 8, 9 | bitr4i 278 | . . . 4
⊢ ((𝐴 |s 𝐵) ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ↔ ((𝐴 |s 𝐵) ∈  No 
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) | 
| 11 | 3, 10 | sylibr 234 | . . 3
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) | 
| 12 |  | conway 27844 | . . 3
⊢ (𝐴 <<s 𝐵 → ∃!𝑦 ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)})) | 
| 13 |  | fveqeq2 6915 | . . . 4
⊢ (𝑦 = (𝐴 |s 𝐵) → (( bday
‘𝑦) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)}))) | 
| 14 | 13 | riota2 7413 | . . 3
⊢ (((𝐴 |s 𝐵) ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ∧ ∃!𝑦 ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)})) → (( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ (℩𝑦 ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)})) = (𝐴 |s 𝐵))) | 
| 15 | 11, 12, 14 | syl2anc 584 | . 2
⊢ (𝐴 <<s 𝐵 → (( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ (℩𝑦 ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)})) = (𝐴 |s 𝐵))) | 
| 16 | 2, 15 | mpbird 257 | 1
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)})) |