Metamath Proof Explorer

Theorem iinopn

Description: The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Assertion iinopn ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 simpr3 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 )
2 dfiin2g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
3 1 2 syl ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
4 simpl ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → 𝐽 ∈ Top )
5 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6 5 rnmpt ⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
7 5 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐽 )
8 1 7 sylib ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐽 )
9 8 frnd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐽 )
10 6 9 eqsstrrid ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐽 )
11 8 fdmd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
12 simpr2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → 𝐴 ≠ ∅ )
13 11 12 eqnetrd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ )
14 dm0rn0 ⊢ ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∅ ↔ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∅ )
15 6 eqeq1i ⊢ ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∅ ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = ∅ )
16 14 15 bitri ⊢ ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∅ ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = ∅ )
17 16 necon3bii ⊢ ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ )
18 13 17 sylib ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ )
19 simpr1 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → 𝐴 ∈ Fin )
20 abrexfi ⊢ ( 𝐴 ∈ Fin → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ Fin )
21 19 20 syl ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ Fin )
22 fiinopn ⊢ ( 𝐽 ∈ Top → ( ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐽 ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ Fin ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝐽 ) )
23 22 imp ⊢ ( ( 𝐽 ∈ Top ∧ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐽 ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ Fin ) ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝐽 )
24 4 10 18 21 23 syl13anc ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝐽 )
25 3 24 eqeltrd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 )