Step | Hyp | Ref
| Expression |
1 | | dmoprab 7376 |
. 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 33978 |
. . . 4
⊢ |s =
(𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
3 | | df-mpo 7280 |
. . . 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 2766 |
. . 3
⊢ |s =
{〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
5 | 4 | dmeqi 5813 |
. 2
⊢ dom |s =
dom {〈〈𝑎, 𝑏〉, 𝑐〉 ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
6 | | df-sslt 33976 |
. . . . 5
⊢
<<s = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆
No ∧ 𝑏 ⊆
No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)} |
7 | 6 | relopabiv 5730 |
. . . 4
⊢ Rel
<<s |
8 | | 19.42v 1957 |
. . . . . 6
⊢
(∃𝑐((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) ↔ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
9 | | ssltss1 33983 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 → 𝑎 ⊆ No
) |
10 | | velpw 4538 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 No ↔ 𝑎 ⊆ No
) |
11 | 9, 10 | sylibr 233 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 → 𝑎 ∈ 𝒫 No
) |
12 | 11 | pm4.71ri 561 |
. . . . . . 7
⊢ (𝑎 <<s 𝑏 ↔ (𝑎 ∈ 𝒫 No
∧ 𝑎 <<s
𝑏)) |
13 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
14 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
15 | 13, 14 | elimasn 5997 |
. . . . . . . . 9
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
16 | | df-br 5075 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
17 | 15, 16 | bitr4i 277 |
. . . . . . . 8
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 𝑎 <<s 𝑏) |
18 | 17 | anbi2i 623 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ↔ (𝑎 ∈ 𝒫 No
∧ 𝑎 <<s
𝑏)) |
19 | | riotaex 7236 |
. . . . . . . . 9
⊢
(℩𝑥
∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ V |
20 | 19 | isseti 3447 |
. . . . . . . 8
⊢
∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) |
21 | 20 | biantru 530 |
. . . . . . 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 5758 |
. . 3
⊢ (⊤
→ <<s = {〈𝑎, 𝑏〉 ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}) |
26 | 25 | mptru 1546 |
. 2
⊢
<<s = {〈𝑎, 𝑏〉 ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
27 | 1, 5, 26 | 3eqtr4i 2776 |
1
⊢ dom |s =
<<s |