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ℋ