Step |
Hyp |
Ref |
Expression |
0 |
|
cscut |
|- |s |
1 |
|
va |
|- a |
2 |
|
csur |
|- No |
3 |
2
|
cpw |
|- ~P No |
4 |
|
vb |
|- b |
5 |
|
csslt |
|- < |
6 |
1
|
cv |
|- a |
7 |
6
|
csn |
|- { a } |
8 |
5 7
|
cima |
|- ( < |
9 |
|
vx |
|- x |
10 |
|
vy |
|- y |
11 |
10
|
cv |
|- y |
12 |
11
|
csn |
|- { y } |
13 |
6 12 5
|
wbr |
|- a < |
14 |
4
|
cv |
|- b |
15 |
12 14 5
|
wbr |
|- { y } < |
16 |
13 15
|
wa |
|- ( a < |
17 |
16 10 2
|
crab |
|- { y e. No | ( a < |
18 |
|
cbday |
|- bday |
19 |
9
|
cv |
|- x |
20 |
19 18
|
cfv |
|- ( bday ` x ) |
21 |
18 17
|
cima |
|- ( bday " { y e. No | ( a < |
22 |
21
|
cint |
|- |^| ( bday " { y e. No | ( a < |
23 |
20 22
|
wceq |
|- ( bday ` x ) = |^| ( bday " { y e. No | ( a < |
24 |
23 9 17
|
crio |
|- ( iota_ x e. { y e. No | ( a < |
25 |
1 4 3 8 24
|
cmpo |
|- ( a e. ~P No , b e. ( < ( iota_ x e. { y e. No | ( a < |
26 |
0 25
|
wceq |
|- |s = ( a e. ~P No , b e. ( < ( iota_ x e. { y e. No | ( a < |