Theorem iunrnmptss

Description: A subset relation for an indexed union over the range of function expressed as a mapping. (Contributed by Thierry Arnoux, 27-Mar-2018)

	Ref	Expression
Hypotheses	iunrnmptss.1	|- ( y = B -> C = D )
	iunrnmptss.2	|- ( ( ph /\ x e. A ) -> B e. V )
Assertion	iunrnmptss	|- ( ph -> U_ y e. ran ( x e. A |-> B ) C C_ U_ x e. A D )

Proof

Step	Hyp	Ref	Expression
1		iunrnmptss.1	|- ( y = B -> C = D )
2		iunrnmptss.2	|- ( ( ph /\ x e. A ) -> B e. V )
3		df-rex	|- ( E. y e. ran ( x e. A |-> B ) z e. C <-> E. y ( y e. ran ( x e. A |-> B ) /\ z e. C ) )
4	2	ralrimiva	|- ( ph -> A. x e. A B e. V )
5		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
6	5	elrnmptg	|- ( A. x e. A B e. V -> ( y e. ran ( x e. A |-> B ) <-> E. x e. A y = B ) )
7	4 6	syl	|- ( ph -> ( y e. ran ( x e. A |-> B ) <-> E. x e. A y = B ) )
8	7	anbi1d	|- ( ph -> ( ( y e. ran ( x e. A |-> B ) /\ z e. C ) <-> ( E. x e. A y = B /\ z e. C ) ) )
9	8	exbidv	|- ( ph -> ( E. y ( y e. ran ( x e. A |-> B ) /\ z e. C ) <-> E. y ( E. x e. A y = B /\ z e. C ) ) )
10		r19.41v	|- ( E. x e. A ( y = B /\ z e. C ) <-> ( E. x e. A y = B /\ z e. C ) )
11	1	eleq2d	|- ( y = B -> ( z e. C <-> z e. D ) )
12	11	biimpa	|- ( ( y = B /\ z e. C ) -> z e. D )
13	12	reximi	|- ( E. x e. A ( y = B /\ z e. C ) -> E. x e. A z e. D )
14	10 13	sylbir	|- ( ( E. x e. A y = B /\ z e. C ) -> E. x e. A z e. D )
15	14	exlimiv	|- ( E. y ( E. x e. A y = B /\ z e. C ) -> E. x e. A z e. D )
16	9 15	syl6bi	|- ( ph -> ( E. y ( y e. ran ( x e. A |-> B ) /\ z e. C ) -> E. x e. A z e. D ) )
17	3 16	syl5bi	|- ( ph -> ( E. y e. ran ( x e. A |-> B ) z e. C -> E. x e. A z e. D ) )
18	17	ss2abdv	|- ( ph -> { z | E. y e. ran ( x e. A |-> B ) z e. C } C_ { z | E. x e. A z e. D } )
19		df-iun	|- U_ y e. ran ( x e. A |-> B ) C = { z | E. y e. ran ( x e. A |-> B ) z e. C }
20		df-iun	|- U_ x e. A D = { z | E. x e. A z e. D }
21	18 19 20	3sstr4g	|- ( ph -> U_ y e. ran ( x e. A |-> B ) C C_ U_ x e. A D )