Step | Hyp | Ref
| Expression |
1 | | cuteq0.1 |
. 2
⊢ (𝜑 → 𝐴 <<s { 0s }) |
2 | | cuteq0.2 |
. 2
⊢ (𝜑 → { 0s } <<s 𝐵) |
3 | | bday0s 27118 |
. . 3
⊢ ( bday ‘ 0s ) = ∅ |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (
bday ‘ 0s ) = ∅) |
5 | | 0sno 27116 |
. . . . . . 7
⊢ 0s
∈ No |
6 | | sneq 4594 |
. . . . . . . . . . 11
⊢ (𝑦 = 0s → {𝑦} = { 0s }) |
7 | 6 | breq2d 5115 |
. . . . . . . . . 10
⊢ (𝑦 = 0s → (𝐴 <<s {𝑦} ↔ 𝐴 <<s { 0s })) |
8 | 6 | breq1d 5113 |
. . . . . . . . . 10
⊢ (𝑦 = 0s → ({𝑦} <<s 𝐵 ↔ { 0s } <<s 𝐵)) |
9 | 7, 8 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑦 = 0s → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s { 0s } ∧ { 0s } <<s
𝐵))) |
10 | | fveqeq2 6848 |
. . . . . . . . 9
⊢ (𝑦 = 0s → (( bday ‘𝑦) = ∅ ↔ (
bday ‘ 0s ) = ∅)) |
11 | 9, 10 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑦 = 0s → (((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) = ∅)
↔ ((𝐴 <<s { 0s }
∧ { 0s } <<s 𝐵)
∧ ( bday ‘ 0s ) =
∅))) |
12 | 11 | rspcev 3579 |
. . . . . . 7
⊢ (( 0s
∈ No ∧ ((𝐴 <<s { 0s } ∧ { 0s } <<s
𝐵) ∧ ( bday ‘ 0s ) = ∅)) → ∃𝑦 ∈
No ((𝐴 <<s
{𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) |
13 | 5, 12 | mpan 688 |
. . . . . 6
⊢ (((𝐴 <<s { 0s } ∧ { 0s }
<<s 𝐵) ∧ ( bday ‘ 0s ) = ∅) → ∃𝑦 ∈
No ((𝐴 <<s
{𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) |
14 | 1, 2, 4, 13 | syl21anc 836 |
. . . . 5
⊢ (𝜑 → ∃𝑦 ∈ No
((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) |
15 | | bdayfn 27064 |
. . . . . . 7
⊢ bday Fn No
|
16 | | ssrab2 4035 |
. . . . . . 7
⊢ {𝑥 ∈
No ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)} ⊆ No
|
17 | | fvelimab 6911 |
. . . . . . 7
⊢ (( bday Fn No ∧ {𝑥 ∈
No ∣ (𝐴
<<s {𝑥} ∧ {𝑥} <<s 𝐵)} ⊆ No
) → (∅ ∈ ( bday “
{𝑥 ∈ No ∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ ∃𝑦 ∈ {𝑥 ∈ No
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) =
∅)) |
18 | 15, 16, 17 | mp2an 690 |
. . . . . 6
⊢ (∅
∈ ( bday “ {𝑥 ∈ No
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ ∃𝑦 ∈ {𝑥 ∈ No
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) =
∅) |
19 | | sneq 4594 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
20 | 19 | breq2d 5115 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐴 <<s {𝑥} ↔ 𝐴 <<s {𝑦})) |
21 | 19 | breq1d 5113 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ({𝑥} <<s 𝐵 ↔ {𝑦} <<s 𝐵)) |
22 | 20, 21 | anbi12d 631 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵) ↔ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵))) |
23 | 22 | rexrab 3652 |
. . . . . 6
⊢
(∃𝑦 ∈
{𝑥 ∈ No ∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)} ( bday
‘𝑦) = ∅
↔ ∃𝑦 ∈
No ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) |
24 | 18, 23 | bitri 274 |
. . . . 5
⊢ (∅
∈ ( bday “ {𝑥 ∈ No
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)}) ↔ ∃𝑦 ∈ No
((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ∧ ( bday
‘𝑦) =
∅)) |
25 | 14, 24 | sylibr 233 |
. . . 4
⊢ (𝜑 → ∅ ∈ ( bday “ {𝑥 ∈ No
∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)})) |
26 | | int0el 4938 |
. . . 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 3462 |
. . . . . 6
⊢ 0s
∈ V |
30 | 29 | snnz 4735 |
. . . . 5
⊢ { 0s }
≠ ∅ |
31 | | sslttr 27097 |
. . . . 5
⊢ ((𝐴 <<s { 0s } ∧ { 0s }
<<s 𝐵 ∧ { 0s }
≠ ∅) → 𝐴
<<s 𝐵) |
32 | 30, 31 | mp3an3 1450 |
. . . 4
⊢ ((𝐴 <<s { 0s } ∧ { 0s }
<<s 𝐵) → 𝐴 <<s 𝐵) |
33 | 1, 2, 32 | syl2anc 584 |
. . 3
⊢ (𝜑 → 𝐴 <<s 𝐵) |
34 | | eqscut 27095 |
. . 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 1342 |
1
⊢ (𝜑 → (𝐴 |s 𝐵) = 0s ) |