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

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 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
Assertion ptbasid ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
2 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → 𝐴 ∈ 𝑉 )
3 0fi ⊢ ∅ ∈ Fin
4 3 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ∅ ∈ Fin )
5 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ Top ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
6 5 adantll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
7 eqid ⊢ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
8 7 topopn ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ Top → ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
9 6 8 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ 𝑘 ∈ 𝐴 ) → ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
10 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ 𝑘 ∈ ( 𝐴 ∖ ∅ ) ) → ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
11 1 2 4 9 10 elptr2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )