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	⊢ ( 𝜑 → Rel 𝑅 )
	relexpreld.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	relexpreld	⊢ ( 𝜑 → Rel ( 𝑅 ↑𝑟 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		relexpreld.1	⊢ ( 𝜑 → Rel 𝑅 )
2		relexpreld.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3	2	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑁 ∈ ℕ0 )
4		simpr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → Rel 𝑅 )
6		relexprel	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ V ∧ Rel 𝑅 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
7	3 4 5 6	syl3anc	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
8	7	ex	⊢ ( 𝜑 → ( 𝑅 ∈ V → Rel ( 𝑅 ↑𝑟 𝑁 ) ) )
9		rel0	⊢ Rel ∅
10		reldmrelexp	⊢ Rel dom ↑𝑟
11	10	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 𝑁 ) = ∅ )
12	11	releqd	⊢ ( ¬ 𝑅 ∈ V → ( Rel ( 𝑅 ↑𝑟 𝑁 ) ↔ Rel ∅ ) )
13	9 12	mpbiri	⊢ ( ¬ 𝑅 ∈ V → Rel ( 𝑅 ↑𝑟 𝑁 ) )
14	8 13	pm2.61d1	⊢ ( 𝜑 → Rel ( 𝑅 ↑𝑟 𝑁 ) )