Step | Hyp | Ref
| Expression |
1 | | df-scut 33248 |
. . . 4
⊢ |s =
(𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
2 | 1 | mpofun 7270 |
. . 3
⊢ Fun
|s |
3 | | dmscut 33267 |
. . 3
⊢ dom |s =
<<s |
4 | | df-fn 6352 |
. . 3
⊢ ( |s Fn
<<s ↔ (Fun |s ∧ dom |s = <<s )) |
5 | 2, 3, 4 | mpbir2an 709 |
. 2
⊢ |s Fn
<<s |
6 | 1 | rnmpo 7278 |
. . 3
⊢ ran |s =
{𝑧 ∣ ∃𝑎 ∈ 𝒫 No ∃𝑏 ∈ ( <<s “ {𝑎})𝑧 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))} |
7 | | vex 3497 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
8 | | vex 3497 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
9 | 7, 8 | elimasn 5948 |
. . . . . . . . 9
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
10 | | df-br 5059 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 ↔ 〈𝑎, 𝑏〉 ∈ <<s ) |
11 | 9, 10 | bitr4i 280 |
. . . . . . . 8
⊢ (𝑏 ∈ ( <<s “
{𝑎}) ↔ 𝑎 <<s 𝑏) |
12 | | scutval 33260 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
13 | | scutcut 33261 |
. . . . . . . . . 10
⊢ (𝑎 <<s 𝑏 → ((𝑎 |s 𝑏) ∈ No
∧ 𝑎 <<s {(𝑎 |s 𝑏)} ∧ {(𝑎 |s 𝑏)} <<s 𝑏)) |
14 | 13 | simp1d 1138 |
. . . . . . . . 9
⊢ (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) ∈ No
) |
15 | 12, 14 | eqeltrrd 2914 |
. . . . . . . 8
⊢ (𝑎 <<s 𝑏 → (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No
) |
16 | 11, 15 | sylbi 219 |
. . . . . . 7
⊢ (𝑏 ∈ ( <<s “
{𝑎}) →
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No
) |
17 | | eleq1a 2908 |
. . . . . . 7
⊢
((℩𝑥
∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ No
→ (𝑧 =
(℩𝑥 ∈
{𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 ∈ No
)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (𝑏 ∈ ( <<s “
{𝑎}) → (𝑧 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 ∈ No
)) |
19 | 18 | adantl 484 |
. . . . 5
⊢ ((𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ {𝑎})) → (𝑧 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 ∈ No
)) |
20 | 19 | rexlimivv 3292 |
. . . 4
⊢
(∃𝑎 ∈
𝒫 No ∃𝑏 ∈ ( <<s “ {𝑎})𝑧 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) → 𝑧 ∈ No
) |
21 | 20 | abssi 4045 |
. . 3
⊢ {𝑧 ∣ ∃𝑎 ∈ 𝒫 No ∃𝑏 ∈ ( <<s “ {𝑎})𝑧 = (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))} ⊆ No
|
22 | 6, 21 | eqsstri 4000 |
. 2
⊢ ran |s
⊆ No |
23 | | df-f 6353 |
. 2
⊢ ( |s :
<<s ⟶ No ↔ ( |s Fn <<s
∧ ran |s ⊆ No )) |
24 | 5, 22, 23 | mpbir2an 709 |
1
⊢ |s :
<<s ⟶ No |