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 CS
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