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	|- ( ph -> N e. NN0 )
Assertion	relexpfldd	|- ( ph -> U. U. ( R ^r N ) C_ U. U. R )

Proof

Step	Hyp	Ref	Expression
1		relexpfldd.1	|- ( ph -> N e. NN0 )
2		relexpfld	|- ( ( N e. NN0 /\ R e. _V ) -> U. U. ( R ^r N ) C_ U. U. R )
3	1 2	sylan	|- ( ( ph /\ R e. _V ) -> U. U. ( R ^r N ) C_ U. U. R )
4	3	ex	|- ( ph -> ( R e. _V -> U. U. ( R ^r N ) C_ U. U. R ) )
5		reldmrelexp	|- Rel dom ^r
6	5	ovprc1	|- ( -. R e. _V -> ( R ^r N ) = (/) )
7	6	unieqd	|- ( -. R e. _V -> U. ( R ^r N ) = U. (/) )
8		uni0	|- U. (/) = (/)
9	7 8	eqtrdi	|- ( -. R e. _V -> U. ( R ^r N ) = (/) )
10	9	unieqd	|- ( -. R e. _V -> U. U. ( R ^r N ) = U. (/) )
11	10 8	eqtrdi	|- ( -. R e. _V -> U. U. ( R ^r N ) = (/) )
12		0ss	|- (/) C_ U. U. R
13	11 12	eqsstrdi	|- ( -. R e. _V -> U. U. ( R ^r N ) C_ U. U. R )
14	4 13	pm2.61d1	|- ( ph -> U. U. ( R ^r N ) C_ U. U. R )