This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chintcli

Description: The intersection of a nonempty set of closed subspaces is a closed subspace. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis chintcl.1 ⊢ ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ )
Assertion chintcli ∩ 𝐴 ∈ Cℋ

Proof

Step Hyp Ref Expression
1 chintcl.1 ⊢ ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ )
2 1 simpli ⊢ 𝐴 ⊆ Cℋ
3 chsssh ⊢ Cℋ ⊆ Sℋ
4 2 3 sstri ⊢ 𝐴 ⊆ Sℋ
5 1 simpri ⊢ 𝐴 ≠ ∅
6 4 5 pm3.2i ⊢ ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ )
7 6 shintcli ⊢ ∩ 𝐴 ∈ Sℋ
8 2 sseli ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ Cℋ )
9 vex ⊢ 𝑥 ∈ V
10 9 chlimi ⊢ ( ( 𝑦 ∈ Cℋ ∧ 𝑓 : ℕ ⟶ 𝑦 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝑦 )
11 10 3exp ⊢ ( 𝑦 ∈ Cℋ → ( 𝑓 : ℕ ⟶ 𝑦 → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝑦 ) ) )
12 11 com3r ⊢ ( 𝑓 ⇝𝑣 𝑥 → ( 𝑦 ∈ Cℋ → ( 𝑓 : ℕ ⟶ 𝑦 → 𝑥 ∈ 𝑦 ) ) )
13 8 12 syl5 ⊢ ( 𝑓 ⇝𝑣 𝑥 → ( 𝑦 ∈ 𝐴 → ( 𝑓 : ℕ ⟶ 𝑦 → 𝑥 ∈ 𝑦 ) ) )
14 13 imp ⊢ ( ( 𝑓 ⇝𝑣 𝑥 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 : ℕ ⟶ 𝑦 → 𝑥 ∈ 𝑦 ) )
15 14 ralimdva ⊢ ( 𝑓 ⇝𝑣 𝑥 → ( ∀ 𝑦 ∈ 𝐴 𝑓 : ℕ ⟶ 𝑦 → ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) )
16 5 fint ⊢ ( 𝑓 : ℕ ⟶ ∩ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 𝑓 : ℕ ⟶ 𝑦 )
17 9 elint2 ⊢ ( 𝑥 ∈ ∩ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
18 15 16 17 3imtr4g ⊢ ( 𝑓 ⇝𝑣 𝑥 → ( 𝑓 : ℕ ⟶ ∩ 𝐴 → 𝑥 ∈ ∩ 𝐴 ) )
19 18 impcom ⊢ ( ( 𝑓 : ℕ ⟶ ∩ 𝐴 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ∩ 𝐴 )
20 19 gen2 ⊢ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ ∩ 𝐴 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ∩ 𝐴 )
21 isch2 ⊢ ( ∩ 𝐴 ∈ Cℋ ↔ ( ∩ 𝐴 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ ∩ 𝐴 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ∩ 𝐴 ) ) )
22 7 20 21 mpbir2an ⊢ ∩ 𝐴 ∈ Cℋ