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 ⊢ 𝑋 = ∪ 𝐽
Assertion clsun ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 clsun.1 ⊢ 𝑋 = ∪ 𝐽
2 difundi ⊢ ( 𝑋 ∖ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑋 ∖ 𝐴 ) ∩ ( 𝑋 ∖ 𝐵 ) )
3 2 fveq2i ⊢ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝐴 ∪ 𝐵 ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( ( 𝑋 ∖ 𝐴 ) ∩ ( 𝑋 ∖ 𝐵 ) ) )
4 difss ⊢ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋
5 difss ⊢ ( 𝑋 ∖ 𝐵 ) ⊆ 𝑋
6 1 ntrin ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝐴 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝐵 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( ( 𝑋 ∖ 𝐴 ) ∩ ( 𝑋 ∖ 𝐵 ) ) ) = ( ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐵 ) ) ) )
7 4 5 6 mp3an23 ⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ( ( 𝑋 ∖ 𝐴 ) ∩ ( 𝑋 ∖ 𝐵 ) ) ) = ( ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐵 ) ) ) )
8 7 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( ( 𝑋 ∖ 𝐴 ) ∩ ( 𝑋 ∖ 𝐵 ) ) ) = ( ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐵 ) ) ) )
9 3 8 eqtrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝐴 ∪ 𝐵 ) ) ) = ( ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐵 ) ) ) )
10 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → 𝐽 ∈ Top )
11 unss ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
12 11 biimpi ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
13 12 3adant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
14 1 ntrdif ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
15 10 13 14 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
16 1 ntrdif ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
17 16 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
18 1 ntrdif ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐵 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) )
19 18 3adant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐵 ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) )
20 17 19 ineq12d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐵 ) ) ) = ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ) )
21 difundi ⊢ ( 𝑋 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ) = ( ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∩ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) )
22 20 21 eqtr4di ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐴 ) ) ∩ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝐵 ) ) ) = ( 𝑋 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ) )
23 9 15 22 3eqtr3d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝑋 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ) )
24 23 difeq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) = ( 𝑋 ∖ ( 𝑋 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ) ) )
25 1 clscld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ( Clsd ‘ 𝐽 ) )
26 10 13 25 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ( Clsd ‘ 𝐽 ) )
27 1 cldss ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑋 )
28 26 27 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑋 )
29 dfss4 ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) )
30 28 29 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) )
31 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 )
32 31 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 )
33 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ⊆ 𝑋 )
34 33 3adant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ⊆ 𝑋 )
35 32 34 jca ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ⊆ 𝑋 ) )
36 unss ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ⊆ 𝑋 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ 𝑋 )
37 dfss4 ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) )
38 36 37 bitri ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ⊆ 𝑋 ) ↔ ( 𝑋 ∖ ( 𝑋 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) )
39 35 38 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) )
40 24 30 39 3eqtr3d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ) )