Metamath Proof Explorer

Theorem ptbasid

Description: The base set of the product topology is a basic open set. (Contributed by Mario Carneiro, 3-Feb-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 ptbasid ⊢ A ∈ V ∧ F : A ⟶ Top → ⨉ k ∈ A ⋃ F ⁡ k ∈ 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 simpl ⊢ A ∈ V ∧ F : A ⟶ Top → A ∈ V
3 0fin ⊢ ∅ ∈ Fin
4 3 a1i ⊢ A ∈ V ∧ F : A ⟶ Top → ∅ ∈ Fin
5 ffvelrn ⊢ F : A ⟶ Top ∧ k ∈ A → F ⁡ k ∈ Top
6 5 adantll ⊢ A ∈ V ∧ F : A ⟶ Top ∧ k ∈ A → F ⁡ k ∈ Top
7 eqid ⊢ ⋃ F ⁡ k = ⋃ F ⁡ k
8 7 topopn ⊢ F ⁡ k ∈ Top → ⋃ F ⁡ k ∈ F ⁡ k
9 6 8 syl ⊢ A ∈ V ∧ F : A ⟶ Top ∧ k ∈ A → ⋃ F ⁡ k ∈ F ⁡ k
10 eqidd ⊢ A ∈ V ∧ F : A ⟶ Top ∧ k ∈ A ∖ ∅ → ⋃ F ⁡ k = ⋃ F ⁡ k
11 1 2 4 9 10 elptr2 ⊢ A ∈ V ∧ F : A ⟶ Top → ⨉ k ∈ A ⋃ F ⁡ k ∈ B