Step |
Hyp |
Ref |
Expression |
1 |
|
pmtrrn.t |
|- T = ( pmTrsp ` D ) |
2 |
|
pmtrrn.r |
|- R = ran T |
3 |
|
mptexg |
|- ( D e. V -> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) e. _V ) |
4 |
3
|
ralrimivw |
|- ( D e. V -> A. z e. { x e. ~P D | x ~~ 2o } ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) e. _V ) |
5 |
4
|
3ad2ant1 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> A. z e. { x e. ~P D | x ~~ 2o } ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) e. _V ) |
6 |
|
eqid |
|- ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) = ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) |
7 |
6
|
fnmpt |
|- ( A. z e. { x e. ~P D | x ~~ 2o } ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) e. _V -> ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) Fn { x e. ~P D | x ~~ 2o } ) |
8 |
5 7
|
syl |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) Fn { x e. ~P D | x ~~ 2o } ) |
9 |
1
|
pmtrfval |
|- ( D e. V -> T = ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) ) |
10 |
9
|
3ad2ant1 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> T = ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) ) |
11 |
10
|
fneq1d |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T Fn { x e. ~P D | x ~~ 2o } <-> ( z e. { x e. ~P D | x ~~ 2o } |-> ( y e. D |-> if ( y e. z , U. ( z \ { y } ) , y ) ) ) Fn { x e. ~P D | x ~~ 2o } ) ) |
12 |
8 11
|
mpbird |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> T Fn { x e. ~P D | x ~~ 2o } ) |
13 |
|
breq1 |
|- ( x = P -> ( x ~~ 2o <-> P ~~ 2o ) ) |
14 |
|
elpw2g |
|- ( D e. V -> ( P e. ~P D <-> P C_ D ) ) |
15 |
14
|
biimpar |
|- ( ( D e. V /\ P C_ D ) -> P e. ~P D ) |
16 |
15
|
3adant3 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P e. ~P D ) |
17 |
|
simp3 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P ~~ 2o ) |
18 |
13 16 17
|
elrabd |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P e. { x e. ~P D | x ~~ 2o } ) |
19 |
|
fnfvelrn |
|- ( ( T Fn { x e. ~P D | x ~~ 2o } /\ P e. { x e. ~P D | x ~~ 2o } ) -> ( T ` P ) e. ran T ) |
20 |
12 18 19
|
syl2anc |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) e. ran T ) |
21 |
20 2
|
eleqtrrdi |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) e. R ) |