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 | |
|
acunirnmpt.1 | |
||
acunirnmpt.2 | |
||
Assertion | acunirnmpt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | acunirnmpt.0 | |
|
2 | acunirnmpt.1 | |
|
3 | acunirnmpt.2 | |
|
4 | simpr | |
|
5 | simplll | |
|
6 | simplr | |
|
7 | 5 6 2 | syl2anc | |
8 | 4 7 | eqnetrd | |
9 | 3 | eleq2i | |
10 | vex | |
|
11 | eqid | |
|
12 | 11 | elrnmpt | |
13 | 10 12 | ax-mp | |
14 | 9 13 | bitri | |
15 | 14 | biimpi | |
16 | 15 | adantl | |
17 | 8 16 | r19.29a | |
18 | 17 | ralrimiva | |
19 | mptexg | |
|
20 | rnexg | |
|
21 | 1 19 20 | 3syl | |
22 | 3 21 | eqeltrid | |
23 | raleq | |
|
24 | id | |
|
25 | unieq | |
|
26 | 24 25 | feq23d | |
27 | raleq | |
|
28 | 26 27 | anbi12d | |
29 | 28 | exbidv | |
30 | 23 29 | imbi12d | |
31 | vex | |
|
32 | 31 | ac5b | |
33 | 30 32 | vtoclg | |
34 | 22 33 | syl | |
35 | 18 34 | mpd | |
36 | 16 | adantr | |
37 | simpllr | |
|
38 | simpr | |
|
39 | 37 38 | eleqtrd | |
40 | 39 | ex | |
41 | 40 | reximdva | |
42 | 36 41 | mpd | |
43 | 42 | ex | |
44 | 43 | ralimdva | |
45 | 44 | anim2d | |
46 | 45 | eximdv | |
47 | 35 46 | mpd | |