Step | Hyp | Ref
| Expression |
1 | | dmoprab 6741 |
. 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 31899 |
. . . 4
⊢ |s =
(𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
3 | | df-mpt2 6655 |
. . . 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 2644 |
. . 3
⊢ |s =
{〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
5 | 4 | dmeqi 5325 |
. 2
⊢ dom |s =
dom {〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
6 | | df-sslt 31897 |
. . . . 5
⊢
<<s = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆
No ∧ 𝑏 ⊆
No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)} |
7 | 6 | relopabi 5245 |
. . . 4
⊢ Rel
<<s |
8 | | 19.42v 1918 |
. . . . . 6
⊢
(∃𝑐((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) ↔ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
9 | | ssltss1 31903 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 → 𝑎 ⊆ No
) |
10 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
11 | 10 | elpw 4164 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 No ↔ 𝑎 ⊆ No
) |
12 | 9, 11 | sylibr 224 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 → 𝑎 ∈ 𝒫 No
) |
13 | 12 | pm4.71ri 665 |
. . . . . . 7
⊢ (𝑎 <<s 𝑏 ↔ (𝑎 ∈ 𝒫 No
∧ 𝑎 <<s
𝑏)) |
14 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
15 | 10, 14 | elimasn 5490 |
. . . . . . . . 9
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
16 | | df-br 4654 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
17 | 15, 16 | bitr4i 267 |
. . . . . . . 8
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 𝑎 <<s 𝑏) |
18 | 17 | anbi2i 730 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ↔ (𝑎 ∈ 𝒫 No
∧ 𝑎 <<s
𝑏)) |
19 | | riotaex 6615 |
. . . . . . . . 9
⊢
(℩𝑥
∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ V |
20 | | isset 3207 |
. . . . . . . . 9
⊢
((℩𝑥
∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ V ↔ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
21 | 19, 20 | mpbi 220 |
. . . . . . . 8
⊢
∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) |
22 | 21 | biantru 526 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ↔ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
23 | 13, 18, 22 | 3bitr2i 288 |
. . . . . 6
⊢ (𝑎 <<s 𝑏 ↔ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
24 | 8, 23, 16 | 3bitr2ri 289 |
. . . . 5
⊢
(〈𝑎, 𝑏〉 ∈ <<s ↔
∃𝑐((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
25 | 24 | a1i 11 |
. . . 4
⊢ (⊤
→ (〈𝑎, 𝑏〉 ∈ <<s ↔
∃𝑐((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))))) |
26 | 7, 25 | opabbi2dv 5271 |
. . 3
⊢ (⊤
→ <<s = {〈𝑎, 𝑏〉 ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}) |
27 | 26 | trud 1493 |
. 2
⊢
<<s = {〈𝑎, 𝑏〉 ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
28 | 1, 5, 27 | 3eqtr4i 2654 |
1
⊢ dom |s =
<<s |