Theorem relexpdmg

Description: The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020)

	Ref	Expression
Assertion	relexpdmg	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2		relexpnndm	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 )
3		ssun1	⊢ dom 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
4	2 3	sstrdi	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
5	4	ex	⊢ ( 𝑁 ∈ ℕ → ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
6		simpl	⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
7	6	oveq2d	⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
8		relexp0g	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
9	8	adantl	⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
10	7 9	eqtrd	⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
11	10	dmeqd	⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) = dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
12		dmresi	⊢ dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( dom 𝑅 ∪ ran 𝑅 )
13	11 12	eqtrdi	⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) = ( dom 𝑅 ∪ ran 𝑅 ) )
14		eqimss	⊢ ( dom ( 𝑅 ↑𝑟 𝑁 ) = ( dom 𝑅 ∪ ran 𝑅 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
15	13 14	syl	⊢ ( ( 𝑁 = 0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
16	15	ex	⊢ ( 𝑁 = 0 → ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
17	5 16	jaoi	⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
18	1 17	sylbi	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
19	18	imp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )