Metamath Proof Explorer

Theorem fiinopn

Description: The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012)

Ref Expression
Assertion fiinopn ( 𝐽 ∈ Top → ( ( 𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ∩ 𝐴 ∈ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 elpwg ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∈ 𝒫 𝐽 ↔ 𝐴 ⊆ 𝐽 ) )
2 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝐽 ↔ 𝐴 ⊆ 𝐽 ) )
3 neeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
4 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ Fin ↔ 𝐴 ∈ Fin ) )
5 2 3 4 3anbi123d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) ↔ ( 𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) )
6 inteq ⊢ ( 𝑥 = 𝐴 → ∩ 𝑥 = ∩ 𝐴 )
7 6 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ∩ 𝑥 ∈ 𝐽 ↔ ∩ 𝐴 ∈ 𝐽 ) )
8 7 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐽 ∈ Top → ∩ 𝑥 ∈ 𝐽 ) ↔ ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) )
9 5 8 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ( 𝐽 ∈ Top → ∩ 𝑥 ∈ 𝐽 ) ) ↔ ( ( 𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) ) )
10 sp ⊢ ( ∀ 𝑥 ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐽 ) → ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐽 ) )
11 10 adantl ⊢ ( ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) ∧ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐽 ) ) → ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐽 ) )
12 istop2g ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) ∧ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐽 ) ) ) )
13 12 ibi ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) ∧ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ∩ 𝑥 ∈ 𝐽 ) ) )
14 11 13 syl11 ⊢ ( ( 𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → ( 𝐽 ∈ Top → ∩ 𝑥 ∈ 𝐽 ) )
15 9 14 vtoclg ⊢ ( 𝐴 ∈ 𝒫 𝐽 → ( ( 𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) )
16 15 com12 ⊢ ( ( 𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ( 𝐴 ∈ 𝒫 𝐽 → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) )
17 16 3exp ⊢ ( 𝐴 ⊆ 𝐽 → ( 𝐴 ≠ ∅ → ( 𝐴 ∈ Fin → ( 𝐴 ∈ 𝒫 𝐽 → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) ) ) )
18 17 com3r ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ⊆ 𝐽 → ( 𝐴 ≠ ∅ → ( 𝐴 ∈ 𝒫 𝐽 → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) ) ) )
19 18 com4r ⊢ ( 𝐴 ∈ 𝒫 𝐽 → ( 𝐴 ∈ Fin → ( 𝐴 ⊆ 𝐽 → ( 𝐴 ≠ ∅ → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) ) ) )
20 1 19 syl6bir ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ⊆ 𝐽 → ( 𝐴 ∈ Fin → ( 𝐴 ⊆ 𝐽 → ( 𝐴 ≠ ∅ → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) ) ) ) )
21 20 pm2.43a ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ⊆ 𝐽 → ( 𝐴 ⊆ 𝐽 → ( 𝐴 ≠ ∅ → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) ) ) )
22 21 com4l ⊢ ( 𝐴 ⊆ 𝐽 → ( 𝐴 ⊆ 𝐽 → ( 𝐴 ≠ ∅ → ( 𝐴 ∈ Fin → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) ) ) )
23 22 pm2.43i ⊢ ( 𝐴 ⊆ 𝐽 → ( 𝐴 ≠ ∅ → ( 𝐴 ∈ Fin → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) ) ) )
24 23 3imp ⊢ ( ( 𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ( 𝐽 ∈ Top → ∩ 𝐴 ∈ 𝐽 ) )
25 24 com12 ⊢ ( 𝐽 ∈ Top → ( ( 𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ∩ 𝐴 ∈ 𝐽 ) )