Theorem founiiun

Description: Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	founiiun	|- ( F : A -onto-> B -> U. B = U_ x e. A ( F ` x ) )

Proof

Step	Hyp	Ref	Expression
1		uniiun	|- U. B = U_ y e. B y
2		foelrni	|- ( ( F : A -onto-> B /\ y e. B ) -> E. x e. A ( F ` x ) = y )
3		eqimss2	|- ( ( F ` x ) = y -> y C_ ( F ` x ) )
4	3	reximi	|- ( E. x e. A ( F ` x ) = y -> E. x e. A y C_ ( F ` x ) )
5	2 4	syl	|- ( ( F : A -onto-> B /\ y e. B ) -> E. x e. A y C_ ( F ` x ) )
6	5	ralrimiva	|- ( F : A -onto-> B -> A. y e. B E. x e. A y C_ ( F ` x ) )
7		iunss2	|- ( A. y e. B E. x e. A y C_ ( F ` x ) -> U_ y e. B y C_ U_ x e. A ( F ` x ) )
8	6 7	syl	|- ( F : A -onto-> B -> U_ y e. B y C_ U_ x e. A ( F ` x ) )
9		fof	|- ( F : A -onto-> B -> F : A --> B )
10	9	ffvelrnda	|- ( ( F : A -onto-> B /\ x e. A ) -> ( F ` x ) e. B )
11		ssidd	|- ( ( F : A -onto-> B /\ x e. A ) -> ( F ` x ) C_ ( F ` x ) )
12		sseq2	|- ( y = ( F ` x ) -> ( ( F ` x ) C_ y <-> ( F ` x ) C_ ( F ` x ) ) )
13	12	rspcev	|- ( ( ( F ` x ) e. B /\ ( F ` x ) C_ ( F ` x ) ) -> E. y e. B ( F ` x ) C_ y )
14	10 11 13	syl2anc	|- ( ( F : A -onto-> B /\ x e. A ) -> E. y e. B ( F ` x ) C_ y )
15	14	ralrimiva	|- ( F : A -onto-> B -> A. x e. A E. y e. B ( F ` x ) C_ y )
16		iunss2	|- ( A. x e. A E. y e. B ( F ` x ) C_ y -> U_ x e. A ( F ` x ) C_ U_ y e. B y )
17	15 16	syl	|- ( F : A -onto-> B -> U_ x e. A ( F ` x ) C_ U_ y e. B y )
18	8 17	eqssd	|- ( F : A -onto-> B -> U_ y e. B y = U_ x e. A ( F ` x ) )
19	1 18	syl5eq	|- ( F : A -onto-> B -> U. B = U_ x e. A ( F ` x ) )