| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pmtrdifel.t |
|- T = ran ( pmTrsp ` ( N \ { K } ) ) |
| 2 |
|
pmtrdifel.r |
|- R = ran ( pmTrsp ` N ) |
| 3 |
|
pmtrdifel.0 |
|- S = ( ( pmTrsp ` N ) ` dom ( Q \ _I ) ) |
| 4 |
|
eqid |
|- ( pmTrsp ` ( N \ { K } ) ) = ( pmTrsp ` ( N \ { K } ) ) |
| 5 |
4 1
|
pmtrfb |
|- ( Q e. T <-> ( ( N \ { K } ) e. _V /\ Q : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) /\ dom ( Q \ _I ) ~~ 2o ) ) |
| 6 |
|
difsnexi |
|- ( ( N \ { K } ) e. _V -> N e. _V ) |
| 7 |
|
f1of |
|- ( Q : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) -> Q : ( N \ { K } ) --> ( N \ { K } ) ) |
| 8 |
|
fdm |
|- ( Q : ( N \ { K } ) --> ( N \ { K } ) -> dom Q = ( N \ { K } ) ) |
| 9 |
|
difssd |
|- ( dom Q = ( N \ { K } ) -> ( Q \ _I ) C_ Q ) |
| 10 |
|
dmss |
|- ( ( Q \ _I ) C_ Q -> dom ( Q \ _I ) C_ dom Q ) |
| 11 |
9 10
|
syl |
|- ( dom Q = ( N \ { K } ) -> dom ( Q \ _I ) C_ dom Q ) |
| 12 |
|
difssd |
|- ( dom Q = ( N \ { K } ) -> ( N \ { K } ) C_ N ) |
| 13 |
|
sseq1 |
|- ( dom Q = ( N \ { K } ) -> ( dom Q C_ N <-> ( N \ { K } ) C_ N ) ) |
| 14 |
12 13
|
mpbird |
|- ( dom Q = ( N \ { K } ) -> dom Q C_ N ) |
| 15 |
11 14
|
sstrd |
|- ( dom Q = ( N \ { K } ) -> dom ( Q \ _I ) C_ N ) |
| 16 |
7 8 15
|
3syl |
|- ( Q : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) -> dom ( Q \ _I ) C_ N ) |
| 17 |
|
id |
|- ( dom ( Q \ _I ) ~~ 2o -> dom ( Q \ _I ) ~~ 2o ) |
| 18 |
|
eqid |
|- ( pmTrsp ` N ) = ( pmTrsp ` N ) |
| 19 |
18 2
|
pmtrrn |
|- ( ( N e. _V /\ dom ( Q \ _I ) C_ N /\ dom ( Q \ _I ) ~~ 2o ) -> ( ( pmTrsp ` N ) ` dom ( Q \ _I ) ) e. R ) |
| 20 |
3 19
|
eqeltrid |
|- ( ( N e. _V /\ dom ( Q \ _I ) C_ N /\ dom ( Q \ _I ) ~~ 2o ) -> S e. R ) |
| 21 |
6 16 17 20
|
syl3an |
|- ( ( ( N \ { K } ) e. _V /\ Q : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) /\ dom ( Q \ _I ) ~~ 2o ) -> S e. R ) |
| 22 |
5 21
|
sylbi |
|- ( Q e. T -> S e. R ) |