Metamath Proof Explorer


Theorem acunirnmpt

Description: Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019)

Ref Expression
Hypotheses acunirnmpt.0 φAV
acunirnmpt.1 φjAB
acunirnmpt.2 C=ranjAB
Assertion acunirnmpt φff:CCyCjAfyB

Proof

Step Hyp Ref Expression
1 acunirnmpt.0 φAV
2 acunirnmpt.1 φjAB
3 acunirnmpt.2 C=ranjAB
4 simpr φyCjAy=By=B
5 simplll φyCjAy=Bφ
6 simplr φyCjAy=BjA
7 5 6 2 syl2anc φyCjAy=BB
8 4 7 eqnetrd φyCjAy=By
9 3 eleq2i yCyranjAB
10 vex yV
11 eqid jAB=jAB
12 11 elrnmpt yVyranjABjAy=B
13 10 12 ax-mp yranjABjAy=B
14 9 13 bitri yCjAy=B
15 14 biimpi yCjAy=B
16 15 adantl φyCjAy=B
17 8 16 r19.29a φyCy
18 17 ralrimiva φyCy
19 mptexg AVjABV
20 rnexg jABVranjABV
21 1 19 20 3syl φranjABV
22 3 21 eqeltrid φCV
23 raleq c=CycyyCy
24 id c=Cc=C
25 unieq c=Cc=C
26 24 25 feq23d c=Cf:ccf:CC
27 raleq c=CycfyyyCfyy
28 26 27 anbi12d c=Cf:ccycfyyf:CCyCfyy
29 28 exbidv c=Cff:ccycfyyff:CCyCfyy
30 23 29 imbi12d c=Cycyff:ccycfyyyCyff:CCyCfyy
31 vex cV
32 31 ac5b ycyff:ccycfyy
33 30 32 vtoclg CVyCyff:CCyCfyy
34 22 33 syl φyCyff:CCyCfyy
35 18 34 mpd φff:CCyCfyy
36 16 adantr φyCfyyjAy=B
37 simpllr φyCfyyjAy=Bfyy
38 simpr φyCfyyjAy=By=B
39 37 38 eleqtrd φyCfyyjAy=BfyB
40 39 ex φyCfyyjAy=BfyB
41 40 reximdva φyCfyyjAy=BjAfyB
42 36 41 mpd φyCfyyjAfyB
43 42 ex φyCfyyjAfyB
44 43 ralimdva φyCfyyyCjAfyB
45 44 anim2d φf:CCyCfyyf:CCyCjAfyB
46 45 eximdv φff:CCyCfyyff:CCyCjAfyB
47 35 46 mpd φff:CCyCjAfyB