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 
|- ( ph -> A e. V )
ptopn2.f 
|- ( ph -> F : A --> Top )
ptopn2.o 
|- ( ph -> O e. ( F ` Y ) )
Assertion ptopn2 
|- ( ph -> X_ k e. A if ( k = Y , O , U. ( F ` k ) ) e. ( Xt_ ` F ) )

Proof

Step Hyp Ref Expression
1 ptopn2.a 
 |-  ( ph -> A e. V )
2 ptopn2.f 
 |-  ( ph -> F : A --> Top )
3 ptopn2.o 
 |-  ( ph -> O e. ( F ` Y ) )
4 snfi 
 |-  { Y } e. Fin
5 4 a1i 
 |-  ( ph -> { Y } e. Fin )
6 3 adantr 
 |-  ( ( ph /\ k e. A ) -> O e. ( F ` Y ) )
7 fveq2 
 |-  ( k = Y -> ( F ` k ) = ( F ` Y ) )
8 7 eleq2d 
 |-  ( k = Y -> ( O e. ( F ` k ) <-> O e. ( F ` Y ) ) )
9 6 8 syl5ibrcom 
 |-  ( ( ph /\ k e. A ) -> ( k = Y -> O e. ( F ` k ) ) )
10 9 imp 
 |-  ( ( ( ph /\ k e. A ) /\ k = Y ) -> O e. ( F ` k ) )
11 2 ffvelcdmda 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. Top )
12 eqid 
 |-  U. ( F ` k ) = U. ( F ` k )
13 12 topopn 
 |-  ( ( F ` k ) e. Top -> U. ( F ` k ) e. ( F ` k ) )
14 11 13 syl 
 |-  ( ( ph /\ k e. A ) -> U. ( F ` k ) e. ( F ` k ) )
15 14 adantr 
 |-  ( ( ( ph /\ k e. A ) /\ -. k = Y ) -> U. ( F ` k ) e. ( F ` k ) )
16 10 15 ifclda 
 |-  ( ( ph /\ k e. A ) -> if ( k = Y , O , U. ( F ` k ) ) e. ( F ` k ) )
17 eldifn 
 |-  ( k e. ( A \ { Y } ) -> -. k e. { Y } )
18 velsn 
 |-  ( k e. { Y } <-> k = Y )
19 17 18 sylnib 
 |-  ( k e. ( A \ { Y } ) -> -. k = Y )
20 19 iffalsed 
 |-  ( k e. ( A \ { Y } ) -> if ( k = Y , O , U. ( F ` k ) ) = U. ( F ` k ) )
21 20 adantl 
 |-  ( ( ph /\ k e. ( A \ { Y } ) ) -> if ( k = Y , O , U. ( F ` k ) ) = U. ( F ` k ) )
22 1 2 5 16 21 ptopn 
 |-  ( ph -> X_ k e. A if ( k = Y , O , U. ( F ` k ) ) e. ( Xt_ ` F ) )