| 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 |
1 2 3
|
pmtrdifellem2 |
|- ( Q e. T -> dom ( S \ _I ) = dom ( Q \ _I ) ) |
| 5 |
4
|
adantr |
|- ( ( Q e. T /\ x e. ( N \ { K } ) ) -> dom ( S \ _I ) = dom ( Q \ _I ) ) |
| 6 |
5
|
eleq2d |
|- ( ( Q e. T /\ x e. ( N \ { K } ) ) -> ( x e. dom ( S \ _I ) <-> x e. dom ( Q \ _I ) ) ) |
| 7 |
4
|
difeq1d |
|- ( Q e. T -> ( dom ( S \ _I ) \ { x } ) = ( dom ( Q \ _I ) \ { x } ) ) |
| 8 |
7
|
unieqd |
|- ( Q e. T -> U. ( dom ( S \ _I ) \ { x } ) = U. ( dom ( Q \ _I ) \ { x } ) ) |
| 9 |
8
|
adantr |
|- ( ( Q e. T /\ x e. ( N \ { K } ) ) -> U. ( dom ( S \ _I ) \ { x } ) = U. ( dom ( Q \ _I ) \ { x } ) ) |
| 10 |
6 9
|
ifbieq1d |
|- ( ( Q e. T /\ x e. ( N \ { K } ) ) -> if ( x e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { x } ) , x ) = if ( x e. dom ( Q \ _I ) , U. ( dom ( Q \ _I ) \ { x } ) , x ) ) |
| 11 |
1 2 3
|
pmtrdifellem1 |
|- ( Q e. T -> S e. R ) |
| 12 |
|
eldifi |
|- ( x e. ( N \ { K } ) -> x e. N ) |
| 13 |
|
eqid |
|- ( pmTrsp ` N ) = ( pmTrsp ` N ) |
| 14 |
|
eqid |
|- dom ( S \ _I ) = dom ( S \ _I ) |
| 15 |
13 2 14
|
pmtrffv |
|- ( ( S e. R /\ x e. N ) -> ( S ` x ) = if ( x e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { x } ) , x ) ) |
| 16 |
11 12 15
|
syl2an |
|- ( ( Q e. T /\ x e. ( N \ { K } ) ) -> ( S ` x ) = if ( x e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { x } ) , x ) ) |
| 17 |
|
eqid |
|- ( pmTrsp ` ( N \ { K } ) ) = ( pmTrsp ` ( N \ { K } ) ) |
| 18 |
|
eqid |
|- dom ( Q \ _I ) = dom ( Q \ _I ) |
| 19 |
17 1 18
|
pmtrffv |
|- ( ( Q e. T /\ x e. ( N \ { K } ) ) -> ( Q ` x ) = if ( x e. dom ( Q \ _I ) , U. ( dom ( Q \ _I ) \ { x } ) , x ) ) |
| 20 |
10 16 19
|
3eqtr4rd |
|- ( ( Q e. T /\ x e. ( N \ { K } ) ) -> ( Q ` x ) = ( S ` x ) ) |
| 21 |
20
|
ralrimiva |
|- ( Q e. T -> A. x e. ( N \ { K } ) ( Q ` x ) = ( S ` x ) ) |