Step |
Hyp |
Ref |
Expression |
0 |
|
cscut |
⊢ |s |
1 |
|
va |
⊢ 𝑎 |
2 |
|
csur |
⊢ No |
3 |
2
|
cpw |
⊢ 𝒫 No |
4 |
|
vb |
⊢ 𝑏 |
5 |
|
csslt |
⊢ <<s |
6 |
1
|
cv |
⊢ 𝑎 |
7 |
6
|
csn |
⊢ { 𝑎 } |
8 |
5 7
|
cima |
⊢ ( <<s “ { 𝑎 } ) |
9 |
|
vx |
⊢ 𝑥 |
10 |
|
vy |
⊢ 𝑦 |
11 |
10
|
cv |
⊢ 𝑦 |
12 |
11
|
csn |
⊢ { 𝑦 } |
13 |
6 12 5
|
wbr |
⊢ 𝑎 <<s { 𝑦 } |
14 |
4
|
cv |
⊢ 𝑏 |
15 |
12 14 5
|
wbr |
⊢ { 𝑦 } <<s 𝑏 |
16 |
13 15
|
wa |
⊢ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) |
17 |
16 10 2
|
crab |
⊢ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } |
18 |
|
cbday |
⊢ bday |
19 |
9
|
cv |
⊢ 𝑥 |
20 |
19 18
|
cfv |
⊢ ( bday ‘ 𝑥 ) |
21 |
18 17
|
cima |
⊢ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) |
22 |
21
|
cint |
⊢ ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) |
23 |
20 22
|
wceq |
⊢ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) |
24 |
23 9 17
|
crio |
⊢ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) |
25 |
1 4 3 8 24
|
cmpo |
⊢ ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) |
26 |
0 25
|
wceq |
⊢ |s = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) |