Metamath Proof Explorer


Theorem ptpjpre2

Description: The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypotheses ptbas.1
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
ptbasfi.2
|- X = X_ n e. A U. ( F ` n )
Assertion ptpjpre2
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) e. B )

Proof

Step Hyp Ref Expression
1 ptbas.1
 |-  B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
2 ptbasfi.2
 |-  X = X_ n e. A U. ( F ` n )
3 2 ptpjpre1
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) = X_ n e. A if ( n = I , U , U. ( F ` n ) ) )
4 simpll
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> A e. V )
5 snfi
 |-  { I } e. Fin
6 5 a1i
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> { I } e. Fin )
7 simprr
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> U e. ( F ` I ) )
8 7 ad2antrr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ n = I ) -> U e. ( F ` I ) )
9 simpr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ n = I ) -> n = I )
10 9 fveq2d
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ n = I ) -> ( F ` n ) = ( F ` I ) )
11 8 10 eleqtrrd
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ n = I ) -> U e. ( F ` n ) )
12 simplr
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> F : A --> Top )
13 12 ffvelrnda
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) -> ( F ` n ) e. Top )
14 eqid
 |-  U. ( F ` n ) = U. ( F ` n )
15 14 topopn
 |-  ( ( F ` n ) e. Top -> U. ( F ` n ) e. ( F ` n ) )
16 13 15 syl
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) -> U. ( F ` n ) e. ( F ` n ) )
17 16 adantr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ -. n = I ) -> U. ( F ` n ) e. ( F ` n ) )
18 11 17 ifclda
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) -> if ( n = I , U , U. ( F ` n ) ) e. ( F ` n ) )
19 eldifsni
 |-  ( n e. ( A \ { I } ) -> n =/= I )
20 19 neneqd
 |-  ( n e. ( A \ { I } ) -> -. n = I )
21 20 adantl
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. ( A \ { I } ) ) -> -. n = I )
22 21 iffalsed
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. ( A \ { I } ) ) -> if ( n = I , U , U. ( F ` n ) ) = U. ( F ` n ) )
23 1 4 6 18 22 elptr2
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> X_ n e. A if ( n = I , U , U. ( F ` n ) ) e. B )
24 3 23 eqeltrd
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) e. B )