Description: A variant of onovuni with indexed unions. (Contributed by Eric Schmidt, 26-May-2009) (Proof shortened by Mario Carneiro, 5-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | onovuni.1 | |
|
onovuni.2 | |
||
Assertion | onoviun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onovuni.1 | |
|
2 | onovuni.2 | |
|
3 | dfiun3g | |
|
4 | 3 | 3ad2ant2 | |
5 | 4 | oveq2d | |
6 | simp1 | |
|
7 | mptexg | |
|
8 | rnexg | |
|
9 | 6 7 8 | 3syl | |
10 | simp2 | |
|
11 | eqid | |
|
12 | 11 | fmpt | |
13 | 10 12 | sylib | |
14 | 13 | frnd | |
15 | dmmptg | |
|
16 | 15 | 3ad2ant2 | |
17 | simp3 | |
|
18 | 16 17 | eqnetrd | |
19 | dm0rn0 | |
|
20 | 19 | necon3bii | |
21 | 18 20 | sylib | |
22 | 1 2 | onovuni | |
23 | 9 14 21 22 | syl3anc | |
24 | oveq2 | |
|
25 | 24 | eleq2d | |
26 | 11 25 | rexrnmptw | |
27 | 26 | 3ad2ant2 | |
28 | eliun | |
|
29 | eliun | |
|
30 | 27 28 29 | 3bitr4g | |
31 | 30 | eqrdv | |
32 | 5 23 31 | 3eqtrd | |