Metamath Proof Explorer


Theorem disjiun

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 DisjxABCADACD=xCBxDB=

Proof

Step Hyp Ref Expression
1 df-disj DisjxABy*xAyB
2 elin yxCBxDByxCByxDB
3 eliun yxCBxCyB
4 eliun yxDBxDyB
5 3 4 anbi12i yxCByxDBxCyBxDyB
6 2 5 bitri yxCBxDBxCyBxDyB
7 nfv zyB
8 7 rmo2 *xAyBzxAyBx=z
9 an4 CADAxCyBxDyBCAxCyBDAxDyB
10 ssralv CAxAyBx=zxCyBx=z
11 10 impcom xAyBx=zCAxCyBx=z
12 r19.29 xCyBx=zxCyBxCyBx=zyB
13 id yBx=zyBx=z
14 13 imp yBx=zyBx=z
15 14 eleq1d yBx=zyBxCzC
16 15 biimpcd xCyBx=zyBzC
17 16 rexlimiv xCyBx=zyBzC
18 12 17 syl xCyBx=zxCyBzC
19 18 ex xCyBx=zxCyBzC
20 11 19 syl xAyBx=zCAxCyBzC
21 20 expimpd xAyBx=zCAxCyBzC
22 ssralv DAxAyBx=zxDyBx=z
23 22 impcom xAyBx=zDAxDyBx=z
24 r19.29 xDyBx=zxDyBxDyBx=zyB
25 14 eleq1d yBx=zyBxDzD
26 25 biimpcd xDyBx=zyBzD
27 26 rexlimiv xDyBx=zyBzD
28 24 27 syl xDyBx=zxDyBzD
29 28 ex xDyBx=zxDyBzD
30 23 29 syl xAyBx=zDAxDyBzD
31 30 expimpd xAyBx=zDAxDyBzD
32 21 31 anim12d xAyBx=zCAxCyBDAxDyBzCzD
33 inelcm zCzDCD
34 32 33 syl6 xAyBx=zCAxCyBDAxDyBCD
35 34 exlimiv zxAyBx=zCAxCyBDAxDyBCD
36 9 35 syl5bi zxAyBx=zCADAxCyBxDyBCD
37 36 expd zxAyBx=zCADAxCyBxDyBCD
38 8 37 sylbi *xAyBCADAxCyBxDyBCD
39 38 impcom CADA*xAyBxCyBxDyBCD
40 6 39 syl5bi CADA*xAyByxCBxDBCD
41 40 necon2bd CADA*xAyBCD=¬yxCBxDB
42 41 impancom CADACD=*xAyB¬yxCBxDB
43 42 3impa CADACD=*xAyB¬yxCBxDB
44 43 alimdv CADACD=y*xAyBy¬yxCBxDB
45 1 44 syl5bi CADACD=DisjxABy¬yxCBxDB
46 45 impcom DisjxABCADACD=y¬yxCBxDB
47 eq0 xCBxDB=y¬yxCBxDB
48 46 47 sylibr DisjxABCADACD=xCBxDB=