Theorem relexpfldd

Description: The field of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypothesis	relexpfldd.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	relexpfldd	⊢ ( 𝜑 → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		relexpfldd.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		relexpfld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ V ) → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 )
3	1 2	sylan	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 )
4	3	ex	⊢ ( 𝜑 → ( 𝑅 ∈ V → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 ) )
5		reldmrelexp	⊢ Rel dom ↑𝑟
6	5	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 𝑁 ) = ∅ )
7	6	unieqd	⊢ ( ¬ 𝑅 ∈ V → ∪ ( 𝑅 ↑𝑟 𝑁 ) = ∪ ∅ )
8		uni0	⊢ ∪ ∅ = ∅
9	7 8	eqtrdi	⊢ ( ¬ 𝑅 ∈ V → ∪ ( 𝑅 ↑𝑟 𝑁 ) = ∅ )
10	9	unieqd	⊢ ( ¬ 𝑅 ∈ V → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) = ∪ ∅ )
11	10 8	eqtrdi	⊢ ( ¬ 𝑅 ∈ V → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) = ∅ )
12		0ss	⊢ ∅ ⊆ ∪ ∪ 𝑅
13	11 12	eqsstrdi	⊢ ( ¬ 𝑅 ∈ V → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 )
14	4 13	pm2.61d1	⊢ ( 𝜑 → ∪ ∪ ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 )