Metamath Proof Explorer

Theorem ptbasin2

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypothesis ptbas.1 ⊢ B = x | ∃ g g Fn A ∧ ∀ y ∈ A g ⁡ y ∈ F ⁡ y ∧ ∃ z ∈ Fin ∀ y ∈ A ∖ z g ⁡ y = ⋃ F ⁡ y ∧ x = ⨉ y ∈ A g ⁡ y
Assertion ptbasin2 ⊢ A ∈ V ∧ F : A ⟶ Top → fi ⁡ B = B

Proof

Step Hyp Ref Expression
1 ptbas.1 ⊢ B = x | ∃ g g Fn A ∧ ∀ y ∈ A g ⁡ y ∈ F ⁡ y ∧ ∃ z ∈ Fin ∀ y ∈ A ∖ z g ⁡ y = ⋃ F ⁡ y ∧ x = ⨉ y ∈ A g ⁡ y
2 1 ptbasin ⊢ A ∈ V ∧ F : A ⟶ Top ∧ u ∈ B ∧ v ∈ B → u ∩ v ∈ B
3 2 ralrimivva ⊢ A ∈ V ∧ F : A ⟶ Top → ∀ u ∈ B ∀ v ∈ B u ∩ v ∈ B
4 1 ptuni2 ⊢ A ∈ V ∧ F : A ⟶ Top → ⨉ k ∈ A ⋃ F ⁡ k = ⋃ B
5 ixpexg ⊢ ∀ k ∈ A ⋃ F ⁡ k ∈ V → ⨉ k ∈ A ⋃ F ⁡ k ∈ V
6 fvex ⊢ F ⁡ k ∈ V
7 6 uniex ⊢ ⋃ F ⁡ k ∈ V
8 7 a1i ⊢ k ∈ A → ⋃ F ⁡ k ∈ V
9 5 8 mprg ⊢ ⨉ k ∈ A ⋃ F ⁡ k ∈ V
10 4 9 eqeltrrdi ⊢ A ∈ V ∧ F : A ⟶ Top → ⋃ B ∈ V
11 uniexb ⊢ B ∈ V ↔ ⋃ B ∈ V
12 10 11 sylibr ⊢ A ∈ V ∧ F : A ⟶ Top → B ∈ V
13 inficl ⊢ B ∈ V → ∀ u ∈ B ∀ v ∈ B u ∩ v ∈ B ↔ fi ⁡ B = B
14 12 13 syl ⊢ A ∈ V ∧ F : A ⟶ Top → ∀ u ∈ B ∀ v ∈ B u ∩ v ∈ B ↔ fi ⁡ B = B
15 3 14 mpbid ⊢ A ∈ V ∧ F : A ⟶ Top → fi ⁡ B = B