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

Metamath Proof Explorer

Theorem hashrabrex

Description: The number of elements in a class abstraction with a restricted existential quantification. (Contributed by Alexander van der Vekens, 29-Jul-2018)

Ref Expression
Hypotheses hashrabrex.1 
|- ( ph -> Y e. Fin )
hashrabrex.2 
|- ( ( ph /\ y e. Y ) -> { x e. X | ps } e. Fin )
hashrabrex.3 
|- ( ph -> Disj_ y e. Y { x e. X | ps } )
Assertion hashrabrex 
|- ( ph -> ( # ` { x e. X | E. y e. Y ps } ) = sum_ y e. Y ( # ` { x e. X | ps } ) )

Proof

Step Hyp Ref Expression
1 hashrabrex.1 
 |-  ( ph -> Y e. Fin )
2 hashrabrex.2 
 |-  ( ( ph /\ y e. Y ) -> { x e. X | ps } e. Fin )
3 hashrabrex.3 
 |-  ( ph -> Disj_ y e. Y { x e. X | ps } )
4 iunrab 
 |-  U_ y e. Y { x e. X | ps } = { x e. X | E. y e. Y ps }
5 4 eqcomi 
 |-  { x e. X | E. y e. Y ps } = U_ y e. Y { x e. X | ps }
6 5 fveq2i 
 |-  ( # ` { x e. X | E. y e. Y ps } ) = ( # ` U_ y e. Y { x e. X | ps } )
7 1 2 3 hashiun 
 |-  ( ph -> ( # ` U_ y e. Y { x e. X | ps } ) = sum_ y e. Y ( # ` { x e. X | ps } ) )
8 6 7 eqtrid 
 |-  ( ph -> ( # ` { x e. X | E. y e. Y ps } ) = sum_ y e. Y ( # ` { x e. X | ps } ) )