Step |
Hyp |
Ref |
Expression |
1 |
|
df-rngisom |
|- RngIsom = ( r e. _V , s e. _V |-> { f e. ( r RngHomo s ) | `' f e. ( s RngHomo r ) } ) |
2 |
1
|
a1i |
|- ( ( R e. V /\ S e. W ) -> RngIsom = ( r e. _V , s e. _V |-> { f e. ( r RngHomo s ) | `' f e. ( s RngHomo r ) } ) ) |
3 |
|
oveq12 |
|- ( ( r = R /\ s = S ) -> ( r RngHomo s ) = ( R RngHomo S ) ) |
4 |
3
|
adantl |
|- ( ( ( R e. V /\ S e. W ) /\ ( r = R /\ s = S ) ) -> ( r RngHomo s ) = ( R RngHomo S ) ) |
5 |
|
oveq12 |
|- ( ( s = S /\ r = R ) -> ( s RngHomo r ) = ( S RngHomo R ) ) |
6 |
5
|
ancoms |
|- ( ( r = R /\ s = S ) -> ( s RngHomo r ) = ( S RngHomo R ) ) |
7 |
6
|
adantl |
|- ( ( ( R e. V /\ S e. W ) /\ ( r = R /\ s = S ) ) -> ( s RngHomo r ) = ( S RngHomo R ) ) |
8 |
7
|
eleq2d |
|- ( ( ( R e. V /\ S e. W ) /\ ( r = R /\ s = S ) ) -> ( `' f e. ( s RngHomo r ) <-> `' f e. ( S RngHomo R ) ) ) |
9 |
4 8
|
rabeqbidv |
|- ( ( ( R e. V /\ S e. W ) /\ ( r = R /\ s = S ) ) -> { f e. ( r RngHomo s ) | `' f e. ( s RngHomo r ) } = { f e. ( R RngHomo S ) | `' f e. ( S RngHomo R ) } ) |
10 |
|
elex |
|- ( R e. V -> R e. _V ) |
11 |
10
|
adantr |
|- ( ( R e. V /\ S e. W ) -> R e. _V ) |
12 |
|
elex |
|- ( S e. W -> S e. _V ) |
13 |
12
|
adantl |
|- ( ( R e. V /\ S e. W ) -> S e. _V ) |
14 |
|
ovex |
|- ( R RngHomo S ) e. _V |
15 |
14
|
rabex |
|- { f e. ( R RngHomo S ) | `' f e. ( S RngHomo R ) } e. _V |
16 |
15
|
a1i |
|- ( ( R e. V /\ S e. W ) -> { f e. ( R RngHomo S ) | `' f e. ( S RngHomo R ) } e. _V ) |
17 |
2 9 11 13 16
|
ovmpod |
|- ( ( R e. V /\ S e. W ) -> ( R RngIsom S ) = { f e. ( R RngHomo S ) | `' f e. ( S RngHomo R ) } ) |
18 |
17
|
eleq2d |
|- ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIsom S ) <-> F e. { f e. ( R RngHomo S ) | `' f e. ( S RngHomo R ) } ) ) |
19 |
|
cnveq |
|- ( f = F -> `' f = `' F ) |
20 |
19
|
eleq1d |
|- ( f = F -> ( `' f e. ( S RngHomo R ) <-> `' F e. ( S RngHomo R ) ) ) |
21 |
20
|
elrab |
|- ( F e. { f e. ( R RngHomo S ) | `' f e. ( S RngHomo R ) } <-> ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) ) |
22 |
18 21
|
bitrdi |
|- ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIsom S ) <-> ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) ) ) |