Step |
Hyp |
Ref |
Expression |
1 |
|
elnn0 |
|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) ) |
2 |
|
relexpnnrn |
|- ( ( N e. NN /\ R e. V ) -> ran ( R ^r N ) C_ ran R ) |
3 |
|
ssun2 |
|- ran R C_ ( dom R u. ran R ) |
4 |
2 3
|
sstrdi |
|- ( ( N e. NN /\ R e. V ) -> ran ( R ^r N ) C_ ( dom R u. ran R ) ) |
5 |
4
|
ex |
|- ( N e. NN -> ( R e. V -> ran ( R ^r N ) C_ ( dom R u. ran R ) ) ) |
6 |
|
simpl |
|- ( ( N = 0 /\ R e. V ) -> N = 0 ) |
7 |
6
|
oveq2d |
|- ( ( N = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) ) |
8 |
|
relexp0g |
|- ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) ) |
9 |
8
|
adantl |
|- ( ( N = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) ) |
10 |
7 9
|
eqtrd |
|- ( ( N = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) ) |
11 |
10
|
rneqd |
|- ( ( N = 0 /\ R e. V ) -> ran ( R ^r N ) = ran ( _I |` ( dom R u. ran R ) ) ) |
12 |
|
rnresi |
|- ran ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R ) |
13 |
11 12
|
eqtrdi |
|- ( ( N = 0 /\ R e. V ) -> ran ( R ^r N ) = ( dom R u. ran R ) ) |
14 |
|
eqimss |
|- ( ran ( R ^r N ) = ( dom R u. ran R ) -> ran ( R ^r N ) C_ ( dom R u. ran R ) ) |
15 |
13 14
|
syl |
|- ( ( N = 0 /\ R e. V ) -> ran ( R ^r N ) C_ ( dom R u. ran R ) ) |
16 |
15
|
ex |
|- ( N = 0 -> ( R e. V -> ran ( R ^r N ) C_ ( dom R u. ran R ) ) ) |
17 |
5 16
|
jaoi |
|- ( ( N e. NN \/ N = 0 ) -> ( R e. V -> ran ( R ^r N ) C_ ( dom R u. ran R ) ) ) |
18 |
1 17
|
sylbi |
|- ( N e. NN0 -> ( R e. V -> ran ( R ^r N ) C_ ( dom R u. ran R ) ) ) |
19 |
18
|
imp |
|- ( ( N e. NN0 /\ R e. V ) -> ran ( R ^r N ) C_ ( dom R u. ran R ) ) |