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

Metamath Proof Explorer

Theorem iunrdx

Description: Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017)

Ref Expression
Hypotheses iunrdx.1 
|- ( ph -> F : A -onto-> C )
iunrdx.2 
|- ( ( ph /\ y = ( F ` x ) ) -> D = B )
Assertion iunrdx 
|- ( ph -> U_ x e. A B = U_ y e. C D )

Proof

Step Hyp Ref Expression
1 iunrdx.1 
 |-  ( ph -> F : A -onto-> C )
2 iunrdx.2 
 |-  ( ( ph /\ y = ( F ` x ) ) -> D = B )
3 fof 
 |-  ( F : A -onto-> C -> F : A --> C )
4 1 3 syl 
 |-  ( ph -> F : A --> C )
5 4 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. C )
6 foelrn 
 |-  ( ( F : A -onto-> C /\ y e. C ) -> E. x e. A y = ( F ` x ) )
7 1 6 sylan 
 |-  ( ( ph /\ y e. C ) -> E. x e. A y = ( F ` x ) )
8 2 eleq2d 
 |-  ( ( ph /\ y = ( F ` x ) ) -> ( z e. D <-> z e. B ) )
9 5 7 8 rexxfrd 
 |-  ( ph -> ( E. y e. C z e. D <-> E. x e. A z e. B ) )
10 9 bicomd 
 |-  ( ph -> ( E. x e. A z e. B <-> E. y e. C z e. D ) )
11 10 abbidv 
 |-  ( ph -> { z | E. x e. A z e. B } = { z | E. y e. C z e. D } )
12 df-iun 
 |-  U_ x e. A B = { z | E. x e. A z e. B }
13 df-iun 
 |-  U_ y e. C D = { z | E. y e. C z e. D }
14 11 12 13 3eqtr4g 
 |-  ( ph -> U_ x e. A B = U_ y e. C D )