Theorem relexpnul

Description: If the domain and range of powers of a relation are disjoint then the relation raised to the sum of those exponents is empty. (Contributed by RP, 1-Jun-2020)

	Ref	Expression
Assertion	relexpnul	|- ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( dom ( R ^r N ) i^i ran ( R ^r M ) ) = (/) <-> ( R ^r ( N + M ) ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		coeq0	|- ( ( ( R ^r N ) o. ( R ^r M ) ) = (/) <-> ( dom ( R ^r N ) i^i ran ( R ^r M ) ) = (/) )
2		simplr	|- ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> Rel R )
3		simprl	|- ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> N e. NN0 )
4		simprr	|- ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> M e. NN0 )
5	2 3 4	relexpaddd	|- ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
6	5	eqeq1d	|- ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( ( R ^r N ) o. ( R ^r M ) ) = (/) <-> ( R ^r ( N + M ) ) = (/) ) )
7	1 6	bitr3id	|- ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( dom ( R ^r N ) i^i ran ( R ^r M ) ) = (/) <-> ( R ^r ( N + M ) ) = (/) ) )