This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi 
 |-  ( ph -> ( E. y ( y e. ran ( x e. A |-> B ) /\ z e. C ) -> E. x e. A z e. D ) )
17 3 16 biimtrid 
 |-  ( 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 )