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 ffvelcdmda 
 |-  ( ( ( ( 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 )