| Step | Hyp | Ref
| Expression |
| 1 | | dmoprab 7536 |
. 2
⊢ dom
{〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} = {〈𝑎, 𝑏〉 ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
| 2 | | df-scut 27828 |
. . . 4
⊢ |s =
(𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
| 3 | | df-mpo 7436 |
. . . 4
⊢ (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) = {〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
| 4 | 2, 3 | eqtri 2765 |
. . 3
⊢ |s =
{〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
| 5 | 4 | dmeqi 5915 |
. 2
⊢ dom |s =
dom {〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
| 6 | | df-sslt 27826 |
. . . . 5
⊢
<<s = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆
No ∧ 𝑏 ⊆
No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)} |
| 7 | 6 | relopabiv 5830 |
. . . 4
⊢ Rel
<<s |
| 8 | | 19.42v 1953 |
. . . . . 6
⊢
(∃𝑐((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) ↔ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
| 9 | | ssltss1 27833 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 → 𝑎 ⊆ No
) |
| 10 | | velpw 4605 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 No ↔ 𝑎 ⊆ No
) |
| 11 | 9, 10 | sylibr 234 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 → 𝑎 ∈ 𝒫 No
) |
| 12 | 11 | pm4.71ri 560 |
. . . . . . 7
⊢ (𝑎 <<s 𝑏 ↔ (𝑎 ∈ 𝒫 No
∧ 𝑎 <<s
𝑏)) |
| 13 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
| 14 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
| 15 | 13, 14 | elimasn 6108 |
. . . . . . . . 9
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
| 16 | | df-br 5144 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
| 17 | 15, 16 | bitr4i 278 |
. . . . . . . 8
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 𝑎 <<s 𝑏) |
| 18 | 17 | anbi2i 623 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ↔ (𝑎 ∈ 𝒫 No
∧ 𝑎 <<s
𝑏)) |
| 19 | | riotaex 7392 |
. . . . . . . . 9
⊢
(℩𝑥
∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ V |
| 20 | 19 | isseti 3498 |
. . . . . . . 8
⊢
∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) |
| 21 | 20 | biantru 529 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ↔ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
| 22 | 12, 18, 21 | 3bitr2i 299 |
. . . . . 6
⊢ (𝑎 <<s 𝑏 ↔ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
| 23 | 8, 22, 16 | 3bitr2ri 300 |
. . . . 5
⊢
(〈𝑎, 𝑏〉 ∈ <<s ↔
∃𝑐((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
| 24 | 23 | a1i 11 |
. . . 4
⊢ (⊤
→ (〈𝑎, 𝑏〉 ∈ <<s ↔
∃𝑐((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))))) |
| 25 | 7, 24 | opabbi2dv 5860 |
. . 3
⊢ (⊤
→ <<s = {〈𝑎, 𝑏〉 ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}) |
| 26 | 25 | mptru 1547 |
. 2
⊢
<<s = {〈𝑎, 𝑏〉 ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
| 27 | 1, 5, 26 | 3eqtr4i 2775 |
1
⊢ dom |s =
<<s |