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 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ 𝐽 )