Metamath Proof Explorer


Theorem clsun

Description: A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009)

Ref Expression
Hypothesis clsun.1 X = J
Assertion clsun J Top A X B X cls J A B = cls J A cls J B

Proof

Step Hyp Ref Expression
1 clsun.1 X = J
2 difundi X A B = X A X B
3 2 fveq2i int J X A B = int J X A X B
4 difss X A X
5 difss X B X
6 1 ntrin J Top X A X X B X int J X A X B = int J X A int J X B
7 4 5 6 mp3an23 J Top int J X A X B = int J X A int J X B
8 7 3ad2ant1 J Top A X B X int J X A X B = int J X A int J X B
9 3 8 syl5eq J Top A X B X int J X A B = int J X A int J X B
10 simp1 J Top A X B X J Top
11 unss A X B X A B X
12 11 biimpi A X B X A B X
13 12 3adant1 J Top A X B X A B X
14 1 ntrdif J Top A B X int J X A B = X cls J A B
15 10 13 14 syl2anc J Top A X B X int J X A B = X cls J A B
16 1 ntrdif J Top A X int J X A = X cls J A
17 16 3adant3 J Top A X B X int J X A = X cls J A
18 1 ntrdif J Top B X int J X B = X cls J B
19 18 3adant2 J Top A X B X int J X B = X cls J B
20 17 19 ineq12d J Top A X B X int J X A int J X B = X cls J A X cls J B
21 difundi X cls J A cls J B = X cls J A X cls J B
22 20 21 eqtr4di J Top A X B X int J X A int J X B = X cls J A cls J B
23 9 15 22 3eqtr3d J Top A X B X X cls J A B = X cls J A cls J B
24 23 difeq2d J Top A X B X X X cls J A B = X X cls J A cls J B
25 1 clscld J Top A B X cls J A B Clsd J
26 10 13 25 syl2anc J Top A X B X cls J A B Clsd J
27 1 cldss cls J A B Clsd J cls J A B X
28 26 27 syl J Top A X B X cls J A B X
29 dfss4 cls J A B X X X cls J A B = cls J A B
30 28 29 sylib J Top A X B X X X cls J A B = cls J A B
31 1 clsss3 J Top A X cls J A X
32 31 3adant3 J Top A X B X cls J A X
33 1 clsss3 J Top B X cls J B X
34 33 3adant2 J Top A X B X cls J B X
35 32 34 jca J Top A X B X cls J A X cls J B X
36 unss cls J A X cls J B X cls J A cls J B X
37 dfss4 cls J A cls J B X X X cls J A cls J B = cls J A cls J B
38 36 37 bitri cls J A X cls J B X X X cls J A cls J B = cls J A cls J B
39 35 38 sylib J Top A X B X X X cls J A cls J B = cls J A cls J B
40 24 30 39 3eqtr3d J Top A X B X cls J A B = cls J A cls J B