Theorem fvmptiunrelexplb0da

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	fvmptiunrelexplb0da.c	|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
	fvmptiunrelexplb0da.r	|- ( ph -> R e. _V )
	fvmptiunrelexplb0da.n	|- ( ph -> N e. _V )
	fvmptiunrelexplb0da.rel	|- ( ph -> Rel R )
	fvmptiunrelexplb0da.0	|- ( ph -> 0 e. N )
Assertion	fvmptiunrelexplb0da	|- ( ph -> ( _I |` U. U. R ) C_ ( C ` R ) )

Proof

Step	Hyp	Ref	Expression
1		fvmptiunrelexplb0da.c	|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
2		fvmptiunrelexplb0da.r	|- ( ph -> R e. _V )
3		fvmptiunrelexplb0da.n	|- ( ph -> N e. _V )
4		fvmptiunrelexplb0da.rel	|- ( ph -> Rel R )
5		fvmptiunrelexplb0da.0	|- ( ph -> 0 e. N )
6		relfld	|- ( Rel R -> U. U. R = ( dom R u. ran R ) )
7	4 6	syl	|- ( ph -> U. U. R = ( dom R u. ran R ) )
8	7	reseq2d	|- ( ph -> ( _I |` U. U. R ) = ( _I |` ( dom R u. ran R ) ) )
9	1 2 3 5	fvmptiunrelexplb0d	|- ( ph -> ( _I |` ( dom R u. ran R ) ) C_ ( C ` R ) )
10	8 9	eqsstrd	|- ( ph -> ( _I |` U. U. R ) C_ ( C ` R ) )