Step |
Hyp |
Ref |
Expression |
1 |
|
iordsmo.1 |
|- Ord A |
2 |
|
fnresi |
|- ( _I |` A ) Fn A |
3 |
|
rnresi |
|- ran ( _I |` A ) = A |
4 |
|
ordsson |
|- ( Ord A -> A C_ On ) |
5 |
1 4
|
ax-mp |
|- A C_ On |
6 |
3 5
|
eqsstri |
|- ran ( _I |` A ) C_ On |
7 |
|
df-f |
|- ( ( _I |` A ) : A --> On <-> ( ( _I |` A ) Fn A /\ ran ( _I |` A ) C_ On ) ) |
8 |
2 6 7
|
mpbir2an |
|- ( _I |` A ) : A --> On |
9 |
|
fvresi |
|- ( x e. A -> ( ( _I |` A ) ` x ) = x ) |
10 |
9
|
adantr |
|- ( ( x e. A /\ y e. A ) -> ( ( _I |` A ) ` x ) = x ) |
11 |
|
fvresi |
|- ( y e. A -> ( ( _I |` A ) ` y ) = y ) |
12 |
11
|
adantl |
|- ( ( x e. A /\ y e. A ) -> ( ( _I |` A ) ` y ) = y ) |
13 |
10 12
|
eleq12d |
|- ( ( x e. A /\ y e. A ) -> ( ( ( _I |` A ) ` x ) e. ( ( _I |` A ) ` y ) <-> x e. y ) ) |
14 |
13
|
biimprd |
|- ( ( x e. A /\ y e. A ) -> ( x e. y -> ( ( _I |` A ) ` x ) e. ( ( _I |` A ) ` y ) ) ) |
15 |
|
dmresi |
|- dom ( _I |` A ) = A |
16 |
8 1 14 15
|
issmo |
|- Smo ( _I |` A ) |