| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cuteq0.1 | . 2
⊢ (𝜑 → 𝐴 <<s { 0s
}) | 
| 2 |  | cuteq0.2 | . 2
⊢ (𝜑 → { 0s }
<<s 𝐵) | 
| 3 |  | bday0s 27873 | . . 3
⊢ ( bday ‘ 0s ) = ∅ | 
| 4 | 3 | a1i 11 | . . . . . 6
⊢ (𝜑 → (
bday ‘ 0s ) = ∅) | 
| 5 |  | 0sno 27871 | . . . . . . 7
⊢ 
0s ∈  No | 
| 6 |  | sneq 4636 | . . . . . . . . . . 11
⊢ (𝑦 = 0s → {𝑦} = { 0s
}) | 
| 7 | 6 | breq2d 5155 | . . . . . . . . . 10
⊢ (𝑦 = 0s → (𝐴 <<s {𝑦} ↔ 𝐴 <<s { 0s
})) | 
| 8 | 6 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝑦 = 0s → ({𝑦} <<s 𝐵 ↔ { 0s } <<s 𝐵)) | 
| 9 | 7, 8 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑦 = 0s → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s { 0s } ∧ {
0s } <<s 𝐵))) | 
| 10 |  | fveqeq2 6915 | . . . . . . . . 9
⊢ (𝑦 = 0s → (( bday ‘𝑦) = ∅ ↔ (
bday ‘ 0s ) = ∅)) | 
| 11 | 9, 10 | anbi12d 632 | . . . . . . . 8
⊢ (𝑦 = 0s → (((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) = ∅)
↔ ((𝐴 <<s {
0s } ∧ { 0s } <<s 𝐵) ∧ ( bday
‘ 0s ) = ∅))) | 
| 12 | 11 | rspcev 3622 | . . . . . . 7
⊢ ((
0s ∈  No  ∧ ((𝐴 <<s { 0s }
∧ { 0s } <<s 𝐵) ∧ ( bday
‘ 0s ) = ∅)) → ∃𝑦 ∈  No 
((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) | 
| 13 | 5, 12 | mpan 690 | . . . . . 6
⊢ (((𝐴 <<s { 0s }
∧ { 0s } <<s 𝐵) ∧ ( bday
‘ 0s ) = ∅) → ∃𝑦 ∈  No 
((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) | 
| 14 | 1, 2, 4, 13 | syl21anc 838 | . . . . 5
⊢ (𝜑 → ∃𝑦 ∈  No 
((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) | 
| 15 |  | bdayfn 27818 | . . . . . . 7
⊢  bday  Fn  No | 
| 16 |  | ssrab2 4080 | . . . . . . 7
⊢ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)} ⊆  No | 
| 17 |  | fvelimab 6981 | . . . . . . 7
⊢ (( bday  Fn  No  ∧ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)} ⊆  No
) → (∅ ∈ ( bday  “
{𝑥 ∈  No  ∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ ∃𝑦 ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) =
∅)) | 
| 18 | 15, 16, 17 | mp2an 692 | . . . . . 6
⊢ (∅
∈ ( bday  “ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ ∃𝑦 ∈ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) =
∅) | 
| 19 |  | sneq 4636 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) | 
| 20 | 19 | breq2d 5155 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐴 <<s {𝑥} ↔ 𝐴 <<s {𝑦})) | 
| 21 | 19 | breq1d 5153 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → ({𝑥} <<s 𝐵 ↔ {𝑦} <<s 𝐵)) | 
| 22 | 20, 21 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵) ↔ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵))) | 
| 23 | 22 | rexrab 3702 | . . . . . 6
⊢
(∃𝑦 ∈
{𝑥 ∈  No  ∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) = ∅
↔ ∃𝑦 ∈
 No  ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) | 
| 24 | 18, 23 | bitri 275 | . . . . 5
⊢ (∅
∈ ( bday  “ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ ∃𝑦 ∈  No 
((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) | 
| 25 | 14, 24 | sylibr 234 | . . . 4
⊢ (𝜑 → ∅ ∈ ( bday  “ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)})) | 
| 26 |  | int0el 4979 | . . . 4
⊢ (∅
∈ ( bday  “ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) → ∩
( bday  “ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) = ∅) | 
| 27 | 25, 26 | syl 17 | . . 3
⊢ (𝜑 → ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)}) = ∅) | 
| 28 | 3, 27 | eqtr4id 2796 | . 2
⊢ (𝜑 → (
bday ‘ 0s ) = ∩ ( bday  “ {𝑥 ∈  No 
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)})) | 
| 29 | 5 | elexi 3503 | . . . . . 6
⊢ 
0s ∈ V | 
| 30 | 29 | snnz 4776 | . . . . 5
⊢ {
0s } ≠ ∅ | 
| 31 |  | sslttr 27852 | . . . . 5
⊢ ((𝐴 <<s { 0s }
∧ { 0s } <<s 𝐵 ∧ { 0s } ≠ ∅)
→ 𝐴 <<s 𝐵) | 
| 32 | 30, 31 | mp3an3 1452 | . . . 4
⊢ ((𝐴 <<s { 0s }
∧ { 0s } <<s 𝐵) → 𝐴 <<s 𝐵) | 
| 33 | 1, 2, 32 | syl2anc 584 | . . 3
⊢ (𝜑 → 𝐴 <<s 𝐵) | 
| 34 |  | eqscut 27850 | . . 3
⊢ ((𝐴 <<s 𝐵 ∧ 0s ∈  No ) → ((𝐴 |s 𝐵) = 0s ↔ (𝐴 <<s { 0s } ∧ {
0s } <<s 𝐵
∧ ( bday ‘ 0s ) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)})))) | 
| 35 | 33, 5, 34 | sylancl 586 | . 2
⊢ (𝜑 → ((𝐴 |s 𝐵) = 0s ↔ (𝐴 <<s { 0s } ∧ {
0s } <<s 𝐵
∧ ( bday ‘ 0s ) = ∩ ( bday  “ {𝑥 ∈ 
No  ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)})))) | 
| 36 | 1, 2, 28, 35 | mpbir3and 1343 | 1
⊢ (𝜑 → (𝐴 |s 𝐵) = 0s ) |