Step | Hyp | Ref
| Expression |
1 | | dmoprab 7463 |
. 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 27145 |
. . . 4
⊢ |s =
(𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
3 | | df-mpo 7367 |
. . . 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 5865 |
. 2
⊢ dom |s =
dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
6 | | df-sslt 27143 |
. . . . 5
⊢
<<s = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆
No ∧ 𝑏 ⊆
No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)} |
7 | 6 | relopabiv 5781 |
. . . 4
⊢ Rel
<<s |
8 | | 19.42v 1958 |
. . . . . 6
⊢
(∃𝑐((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) ↔ ((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ ∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))) |
9 | | ssltss1 27150 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 → 𝑎 ⊆ No
) |
10 | | velpw 4570 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 No ↔ 𝑎 ⊆ No
) |
11 | 9, 10 | sylibr 233 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 → 𝑎 ∈ 𝒫 No
) |
12 | 11 | pm4.71ri 562 |
. . . . . . 7
⊢ (𝑎 <<s 𝑏 ↔ (𝑎 ∈ 𝒫 No
∧ 𝑎 <<s
𝑏)) |
13 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
14 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
15 | 13, 14 | elimasn 6046 |
. . . . . . . . 9
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ <<s ) |
16 | | df-br 5111 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ <<s ) |
17 | 15, 16 | bitr4i 278 |
. . . . . . . 8
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 𝑎 <<s 𝑏) |
18 | 17 | anbi2i 624 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) ↔ (𝑎 ∈ 𝒫 No
∧ 𝑎 <<s
𝑏)) |
19 | | riotaex 7322 |
. . . . . . . . 9
⊢
(℩𝑥
∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ V |
20 | 19 | isseti 3463 |
. . . . . . . 8
⊢
∃𝑐 𝑐 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) |
21 | 20 | biantru 531 |
. . . . . . 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 5810 |
. . 3
⊢ (⊤
→ <<s = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}) |
26 | 25 | mptru 1549 |
. 2
⊢
<<s = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐((𝑎 ∈ 𝒫 No
∧ 𝑏 ∈ (
<<s “ {𝑎}))
∧ 𝑐 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} |
27 | 1, 5, 26 | 3eqtr4i 2775 |
1
⊢ dom |s =
<<s |