Theorem fvmptiunrelexplb0d

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

	Ref	Expression
Hypotheses	fvmptiunrelexplb0d.c	|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
	fvmptiunrelexplb0d.r	|- ( ph -> R e. _V )
	fvmptiunrelexplb0d.n	|- ( ph -> N e. _V )
	fvmptiunrelexplb0d.0	|- ( ph -> 0 e. N )
Assertion	fvmptiunrelexplb0d	|- ( ph -> ( _I |` ( dom R u. ran R ) ) C_ ( C ` R ) )

Proof

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