Metamath Proof Explorer


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:AontoBB=xAFx

Proof

Step Hyp Ref Expression
1 uniiun B=yBy
2 foelcdmi F:AontoByBxAFx=y
3 eqimss2 Fx=yyFx
4 3 reximi xAFx=yxAyFx
5 2 4 syl F:AontoByBxAyFx
6 5 ralrimiva F:AontoByBxAyFx
7 iunss2 yBxAyFxyByxAFx
8 6 7 syl F:AontoByByxAFx
9 fof F:AontoBF:AB
10 9 ffvelcdmda F:AontoBxAFxB
11 ssidd F:AontoBxAFxFx
12 sseq2 y=FxFxyFxFx
13 12 rspcev FxBFxFxyBFxy
14 10 11 13 syl2anc F:AontoBxAyBFxy
15 14 ralrimiva F:AontoBxAyBFxy
16 iunss2 xAyBFxyxAFxyBy
17 15 16 syl F:AontoBxAFxyBy
18 8 17 eqssd F:AontoByBy=xAFx
19 1 18 eqtrid F:AontoBB=xAFx