Step |
Hyp |
Ref |
Expression |
1 |
|
pmtrrn.t |
|- T = ( pmTrsp ` D ) |
2 |
|
pmtrrn.r |
|- R = ran T |
3 |
|
eqid |
|- dom ( F \ _I ) = dom ( F \ _I ) |
4 |
1 2 3
|
pmtrfrn |
|- ( F e. R -> ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) /\ F = ( T ` dom ( F \ _I ) ) ) ) |
5 |
|
simpl1 |
|- ( ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) /\ F = ( T ` dom ( F \ _I ) ) ) -> D e. _V ) |
6 |
4 5
|
syl |
|- ( F e. R -> D e. _V ) |
7 |
1 2
|
pmtrff1o |
|- ( F e. R -> F : D -1-1-onto-> D ) |
8 |
|
simpl3 |
|- ( ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) /\ F = ( T ` dom ( F \ _I ) ) ) -> dom ( F \ _I ) ~~ 2o ) |
9 |
4 8
|
syl |
|- ( F e. R -> dom ( F \ _I ) ~~ 2o ) |
10 |
6 7 9
|
3jca |
|- ( F e. R -> ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) ) |
11 |
|
simp2 |
|- ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> F : D -1-1-onto-> D ) |
12 |
|
difss |
|- ( F \ _I ) C_ F |
13 |
|
dmss |
|- ( ( F \ _I ) C_ F -> dom ( F \ _I ) C_ dom F ) |
14 |
12 13
|
ax-mp |
|- dom ( F \ _I ) C_ dom F |
15 |
|
f1odm |
|- ( F : D -1-1-onto-> D -> dom F = D ) |
16 |
14 15
|
sseqtrid |
|- ( F : D -1-1-onto-> D -> dom ( F \ _I ) C_ D ) |
17 |
1 2
|
pmtrrn |
|- ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) -> ( T ` dom ( F \ _I ) ) e. R ) |
18 |
16 17
|
syl3an2 |
|- ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> ( T ` dom ( F \ _I ) ) e. R ) |
19 |
1 2
|
pmtrff1o |
|- ( ( T ` dom ( F \ _I ) ) e. R -> ( T ` dom ( F \ _I ) ) : D -1-1-onto-> D ) |
20 |
18 19
|
syl |
|- ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> ( T ` dom ( F \ _I ) ) : D -1-1-onto-> D ) |
21 |
|
simp3 |
|- ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> dom ( F \ _I ) ~~ 2o ) |
22 |
1
|
pmtrmvd |
|- ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) -> dom ( ( T ` dom ( F \ _I ) ) \ _I ) = dom ( F \ _I ) ) |
23 |
16 22
|
syl3an2 |
|- ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> dom ( ( T ` dom ( F \ _I ) ) \ _I ) = dom ( F \ _I ) ) |
24 |
|
f1otrspeq |
|- ( ( ( F : D -1-1-onto-> D /\ ( T ` dom ( F \ _I ) ) : D -1-1-onto-> D ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( ( T ` dom ( F \ _I ) ) \ _I ) = dom ( F \ _I ) ) ) -> F = ( T ` dom ( F \ _I ) ) ) |
25 |
11 20 21 23 24
|
syl22anc |
|- ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> F = ( T ` dom ( F \ _I ) ) ) |
26 |
25 18
|
eqeltrd |
|- ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> F e. R ) |
27 |
10 26
|
impbii |
|- ( F e. R <-> ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) ) |