Step |
Hyp |
Ref |
Expression |
1 |
|
rankf |
|
2 |
|
rankelb |
|
3 |
|
epel |
|
4 |
|
fvex |
|
5 |
4
|
epeli |
|
6 |
2 3 5
|
3imtr4g |
|
7 |
6
|
rgen |
|
8 |
7
|
rgenw |
|
9 |
|
df-relp |
Could not format ( rank RelPres _E , _E ( U. ( R1 " On ) , On ) <-> ( rank : U. ( R1 " On ) --> On /\ A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( x _E y -> ( rank ` x ) _E ( rank ` y ) ) ) ) : No typesetting found for |- ( rank RelPres _E , _E ( U. ( R1 " On ) , On ) <-> ( rank : U. ( R1 " On ) --> On /\ A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( x _E y -> ( rank ` x ) _E ( rank ` y ) ) ) ) with typecode |- |
10 |
1 8 9
|
mpbir2an |
Could not format rank RelPres _E , _E ( U. ( R1 " On ) , On ) : No typesetting found for |- rank RelPres _E , _E ( U. ( R1 " On ) , On ) with typecode |- |