Description: A disjoint collection yields disjoint indexed unions for disjoint index sets. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by Mario Carneiro, 14-Nov-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | disjiun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-disj | |
|
2 | elin | |
|
3 | eliun | |
|
4 | eliun | |
|
5 | 3 4 | anbi12i | |
6 | 2 5 | bitri | |
7 | nfv | |
|
8 | 7 | rmo2 | |
9 | an4 | |
|
10 | ssralv | |
|
11 | 10 | impcom | |
12 | r19.29 | |
|
13 | id | |
|
14 | 13 | imp | |
15 | 14 | eleq1d | |
16 | 15 | biimpcd | |
17 | 16 | rexlimiv | |
18 | 12 17 | syl | |
19 | 18 | ex | |
20 | 11 19 | syl | |
21 | 20 | expimpd | |
22 | ssralv | |
|
23 | 22 | impcom | |
24 | r19.29 | |
|
25 | 14 | eleq1d | |
26 | 25 | biimpcd | |
27 | 26 | rexlimiv | |
28 | 24 27 | syl | |
29 | 28 | ex | |
30 | 23 29 | syl | |
31 | 30 | expimpd | |
32 | 21 31 | anim12d | |
33 | inelcm | |
|
34 | 32 33 | syl6 | |
35 | 34 | exlimiv | |
36 | 9 35 | syl5bi | |
37 | 36 | expd | |
38 | 8 37 | sylbi | |
39 | 38 | impcom | |
40 | 6 39 | syl5bi | |
41 | 40 | necon2bd | |
42 | 41 | impancom | |
43 | 42 | 3impa | |
44 | 43 | alimdv | |
45 | 1 44 | syl5bi | |
46 | 45 | impcom | |
47 | eq0 | |
|
48 | 46 47 | sylibr | |