Theorem fvmptiunrelexplb1d

Description: If the indexed union ranges over the first power of the relation, then the relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypotheses	fvmptiunrelexplb1d.c	|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
	fvmptiunrelexplb1d.r	|- ( ph -> R e. _V )
	fvmptiunrelexplb1d.n	|- ( ph -> N e. _V )
	fvmptiunrelexplb1d.1	|- ( ph -> 1 e. N )
Assertion	fvmptiunrelexplb1d	|- ( ph -> R C_ ( C ` R ) )

Proof

Step	Hyp	Ref	Expression
1		fvmptiunrelexplb1d.c	|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
2		fvmptiunrelexplb1d.r	|- ( ph -> R e. _V )
3		fvmptiunrelexplb1d.n	|- ( ph -> N e. _V )
4		fvmptiunrelexplb1d.1	|- ( ph -> 1 e. N )
5		oveq2	|- ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
6	5	ssiun2s	|- ( 1 e. N -> ( R ^r 1 ) C_ U_ n e. N ( R ^r n ) )
7	4 6	syl	|- ( ph -> ( R ^r 1 ) C_ U_ n e. N ( R ^r n ) )
8	2	relexp1d	|- ( ph -> ( R ^r 1 ) = R )
9		oveq1	|- ( r = R -> ( r ^r n ) = ( R ^r n ) )
10	9	iuneq2d	|- ( r = R -> U_ n e. N ( r ^r n ) = U_ n e. N ( R ^r n ) )
11		ovex	|- ( R ^r n ) e. _V
12	11	rgenw	|- A. n e. N ( R ^r n ) e. _V
13		iunexg	|- ( ( N e. _V /\ A. n e. N ( R ^r n ) e. _V ) -> U_ n e. N ( R ^r n ) e. _V )
14	3 12 13	sylancl	|- ( ph -> U_ n e. N ( R ^r n ) e. _V )
15	1 10 2 14	fvmptd3	|- ( ph -> ( C ` R ) = U_ n e. N ( R ^r n ) )
16	15	eqcomd	|- ( ph -> U_ n e. N ( R ^r n ) = ( C ` R ) )
17	7 8 16	3sstr3d	|- ( ph -> R C_ ( C ` R ) )