Step |
Hyp |
Ref |
Expression |
1 |
|
pmtrfval.t |
|- T = ( pmTrsp ` D ) |
2 |
1
|
pmtrfval |
|- ( D e. V -> T = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) ) |
3 |
2
|
fveq1d |
|- ( D e. V -> ( T ` P ) = ( ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) ` P ) ) |
4 |
3
|
3ad2ant1 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) = ( ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) ` P ) ) |
5 |
|
eqid |
|- ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) |
6 |
|
eleq2 |
|- ( p = P -> ( z e. p <-> z e. P ) ) |
7 |
|
difeq1 |
|- ( p = P -> ( p \ { z } ) = ( P \ { z } ) ) |
8 |
7
|
unieqd |
|- ( p = P -> U. ( p \ { z } ) = U. ( P \ { z } ) ) |
9 |
6 8
|
ifbieq1d |
|- ( p = P -> if ( z e. p , U. ( p \ { z } ) , z ) = if ( z e. P , U. ( P \ { z } ) , z ) ) |
10 |
9
|
mpteq2dv |
|- ( p = P -> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) = ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) ) |
11 |
|
breq1 |
|- ( y = P -> ( y ~~ 2o <-> P ~~ 2o ) ) |
12 |
|
elpw2g |
|- ( D e. V -> ( P e. ~P D <-> P C_ D ) ) |
13 |
12
|
biimpar |
|- ( ( D e. V /\ P C_ D ) -> P e. ~P D ) |
14 |
13
|
3adant3 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P e. ~P D ) |
15 |
|
simp3 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P ~~ 2o ) |
16 |
11 14 15
|
elrabd |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> P e. { y e. ~P D | y ~~ 2o } ) |
17 |
|
mptexg |
|- ( D e. V -> ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) e. _V ) |
18 |
17
|
3ad2ant1 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) e. _V ) |
19 |
5 10 16 18
|
fvmptd3 |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( ( p e. { y e. ~P D | y ~~ 2o } |-> ( z e. D |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) ` P ) = ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) ) |
20 |
4 19
|
eqtrd |
|- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) = ( z e. D |-> if ( z e. P , U. ( P \ { z } ) , z ) ) ) |