Metamath Proof Explorer

Theorem iincld

Description: The indexed intersection of a collection B ( x ) of closed sets is closed. Theorem 6.1(2) of Munkres p. 93. (Contributed by NM, 5-Oct-2006) (Revised by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion iincld ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 1 cldss ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐵 ⊆ ∪ 𝐽 )
3 dfss4 ⊢ ( 𝐵 ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = 𝐵 )
4 2 3 sylib ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = 𝐵 )
5 4 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ∀ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = 𝐵 )
6 iineq2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = 𝐵 → ∩ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = ∩ 𝑥 ∈ 𝐴 𝐵 )
7 5 6 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ∩ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = ∩ 𝑥 ∈ 𝐴 𝐵 )
8 7 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = ∩ 𝑥 ∈ 𝐴 𝐵 )
9 iindif2 ⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = ( ∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ) )
10 9 adantr ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝐵 ) ) = ( ∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ) )
11 8 10 eqtr3d ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ( ∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ) )
12 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∃ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
13 cldrcl ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
14 13 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
15 12 14 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ Top )
16 1 cldopn ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ 𝐵 ) ∈ 𝐽 )
17 16 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ∀ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ∈ 𝐽 )
18 17 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∀ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ∈ 𝐽 )
19 iunopn ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ∈ 𝐽 ) → ∪ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ∈ 𝐽 )
20 15 18 19 syl2anc ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∪ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ∈ 𝐽 )
21 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ) ∈ ( Clsd ‘ 𝐽 ) )
22 15 20 21 syl2anc ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 ( ∪ 𝐽 ∖ 𝐵 ) ) ∈ ( Clsd ‘ 𝐽 ) )
23 11 22 eqeltrd ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) )