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

Metamath Proof Explorer

Theorem ptopn2

Description: A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypotheses ptopn2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ptopn2.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
ptopn2.o ⊢ ( 𝜑 → 𝑂 ∈ ( 𝐹 ‘ 𝑌 ) )
Assertion ptopn2 ( 𝜑 → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ∏t ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ptopn2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 ptopn2.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
3 ptopn2.o ⊢ ( 𝜑 → 𝑂 ∈ ( 𝐹 ‘ 𝑌 ) )
4 snfi ⊢ { 𝑌 } ∈ Fin
5 4 a1i ⊢ ( 𝜑 → { 𝑌 } ∈ Fin )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑂 ∈ ( 𝐹 ‘ 𝑌 ) )
7 fveq2 ⊢ ( 𝑘 = 𝑌 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑌 ) )
8 7 eleq2d ⊢ ( 𝑘 = 𝑌 → ( 𝑂 ∈ ( 𝐹 ‘ 𝑘 ) ↔ 𝑂 ∈ ( 𝐹 ‘ 𝑌 ) ) )
9 6 8 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑘 = 𝑌 → 𝑂 ∈ ( 𝐹 ‘ 𝑘 ) ) )
10 9 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑘 = 𝑌 ) → 𝑂 ∈ ( 𝐹 ‘ 𝑘 ) )
11 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
12 eqid ⊢ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
13 12 topopn ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ Top → ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
14 11 13 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
15 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ¬ 𝑘 = 𝑌 ) → ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
16 10 15 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 𝐹 ‘ 𝑘 ) )
17 eldifn ⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑌 } ) → ¬ 𝑘 ∈ { 𝑌 } )
18 velsn ⊢ ( 𝑘 ∈ { 𝑌 } ↔ 𝑘 = 𝑌 )
19 17 18 sylnib ⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑌 } ) → ¬ 𝑘 = 𝑌 )
20 19 iffalsed ⊢ ( 𝑘 ∈ ( 𝐴 ∖ { 𝑌 } ) → if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) = ∪ ( 𝐹 ‘ 𝑘 ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { 𝑌 } ) ) → if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) = ∪ ( 𝐹 ‘ 𝑘 ) )
22 1 2 5 16 21 ptopn ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑌 , 𝑂 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ∏t ‘ 𝐹 ) )