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

Metamath Proof Explorer

Theorem riinopn

Description: A finite indexed relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis 1open.1 ⊢ 𝑋 = ∪ 𝐽
Assertion riinopn ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 1open.1 ⊢ 𝑋 = ∪ 𝐽
2 riin0 ⊢ ( 𝐴 = ∅ → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = 𝑋 )
3 2 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ∧ 𝐴 = ∅ ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = 𝑋 )
4 simpl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ∧ 𝐴 = ∅ ) → 𝐽 ∈ Top )
5 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
6 4 5 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ∧ 𝐴 = ∅ ) → 𝑋 ∈ 𝐽 )
7 3 6 eqeltrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ∧ 𝐴 = ∅ ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ 𝐽 )
8 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝐽 ) → 𝐵 ⊆ 𝑋 )
9 8 ex ⊢ ( 𝐽 ∈ Top → ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑋 ) )
10 9 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ) → ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑋 ) )
11 10 ralimdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑋 ) )
12 11 3impia ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑋 )
13 riinn0 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑋 ∧ 𝐴 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = ∩ 𝑥 ∈ 𝐴 𝐵 )
14 12 13 sylan ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ∧ 𝐴 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = ∩ 𝑥 ∈ 𝐴 𝐵 )
15 iinopn ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 )
16 15 3exp2 ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ Fin → ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) ) )
17 16 com34 ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ Fin → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 → ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ) ) )
18 17 3imp1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ∧ 𝐴 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 )
19 14 18 eqeltrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) ∧ 𝐴 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ 𝐽 )
20 7 19 pm2.61dane ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ 𝐽 )