Theorem relexpreld

Description: The exponentiation of a relation is a relation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	relexpreld.1	|- ( ph -> Rel R )
	relexpreld.2	|- ( ph -> N e. NN0 )
Assertion	relexpreld	|- ( ph -> Rel ( R ^r N ) )

Proof

Step	Hyp	Ref	Expression
1		relexpreld.1	|- ( ph -> Rel R )
2		relexpreld.2	|- ( ph -> N e. NN0 )
3	2	adantr	|- ( ( ph /\ R e. _V ) -> N e. NN0 )
4		simpr	|- ( ( ph /\ R e. _V ) -> R e. _V )
5	1	adantr	|- ( ( ph /\ R e. _V ) -> Rel R )
6		relexprel	|- ( ( N e. NN0 /\ R e. _V /\ Rel R ) -> Rel ( R ^r N ) )
7	3 4 5 6	syl3anc	|- ( ( ph /\ R e. _V ) -> Rel ( R ^r N ) )
8	7	ex	|- ( ph -> ( R e. _V -> Rel ( R ^r N ) ) )
9		rel0	|- Rel (/)
10		reldmrelexp	|- Rel dom ^r
11	10	ovprc1	|- ( -. R e. _V -> ( R ^r N ) = (/) )
12	11	releqd	|- ( -. R e. _V -> ( Rel ( R ^r N ) <-> Rel (/) ) )
13	9 12	mpbiri	|- ( -. R e. _V -> Rel ( R ^r N ) )
14	8 13	pm2.61d1	|- ( ph -> Rel ( R ^r N ) )