Metamath Proof Explorer

Theorem txbas

Description: The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis txval.1 
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )
Assertion txbas 
|- ( ( R e. TopBases /\ S e. TopBases ) -> B e. TopBases )

Proof

Step Hyp Ref Expression
1 txval.1 
 |-  B = ran ( x e. R , y e. S |-> ( x X. y ) )
2 xpeq1 
 |-  ( x = a -> ( x X. y ) = ( a X. y ) )
3 xpeq2 
 |-  ( y = b -> ( a X. y ) = ( a X. b ) )
4 2 3 cbvmpov 
 |-  ( x e. R , y e. S |-> ( x X. y ) ) = ( a e. R , b e. S |-> ( a X. b ) )
5 4 rnmpo 
 |-  ran ( x e. R , y e. S |-> ( x X. y ) ) = { u | E. a e. R E. b e. S u = ( a X. b ) }
6 1 5 eqtri 
 |-  B = { u | E. a e. R E. b e. S u = ( a X. b ) }
7 6 abeq2i 
 |-  ( u e. B <-> E. a e. R E. b e. S u = ( a X. b ) )
8 xpeq1 
 |-  ( x = c -> ( x X. y ) = ( c X. y ) )
9 xpeq2 
 |-  ( y = d -> ( c X. y ) = ( c X. d ) )
10 8 9 cbvmpov 
 |-  ( x e. R , y e. S |-> ( x X. y ) ) = ( c e. R , d e. S |-> ( c X. d ) )
11 10 rnmpo 
 |-  ran ( x e. R , y e. S |-> ( x X. y ) ) = { v | E. c e. R E. d e. S v = ( c X. d ) }
12 1 11 eqtri 
 |-  B = { v | E. c e. R E. d e. S v = ( c X. d ) }
13 12 abeq2i 
 |-  ( v e. B <-> E. c e. R E. d e. S v = ( c X. d ) )
14 7 13 anbi12i 
 |-  ( ( u e. B /\ v e. B ) <-> ( E. a e. R E. b e. S u = ( a X. b ) /\ E. c e. R E. d e. S v = ( c X. d ) ) )
15 reeanv 
 |-  ( E. a e. R E. c e. R ( E. b e. S u = ( a X. b ) /\ E. d e. S v = ( c X. d ) ) <-> ( E. a e. R E. b e. S u = ( a X. b ) /\ E. c e. R E. d e. S v = ( c X. d ) ) )
16 14 15 bitr4i 
 |-  ( ( u e. B /\ v e. B ) <-> E. a e. R E. c e. R ( E. b e. S u = ( a X. b ) /\ E. d e. S v = ( c X. d ) ) )
17 reeanv 
 |-  ( E. b e. S E. d e. S ( u = ( a X. b ) /\ v = ( c X. d ) ) <-> ( E. b e. S u = ( a X. b ) /\ E. d e. S v = ( c X. d ) ) )
18 basis2 
 |-  ( ( ( R e. TopBases /\ a e. R ) /\ ( c e. R /\ u e. ( a i^i c ) ) ) -> E. x e. R ( u e. x /\ x C_ ( a i^i c ) ) )
19 18 exp43 
 |-  ( R e. TopBases -> ( a e. R -> ( c e. R -> ( u e. ( a i^i c ) -> E. x e. R ( u e. x /\ x C_ ( a i^i c ) ) ) ) ) )
20 19 imp42 
 |-  ( ( ( R e. TopBases /\ ( a e. R /\ c e. R ) ) /\ u e. ( a i^i c ) ) -> E. x e. R ( u e. x /\ x C_ ( a i^i c ) ) )
21 basis2 
 |-  ( ( ( S e. TopBases /\ b e. S ) /\ ( d e. S /\ v e. ( b i^i d ) ) ) -> E. y e. S ( v e. y /\ y C_ ( b i^i d ) ) )
22 21 exp43 
 |-  ( S e. TopBases -> ( b e. S -> ( d e. S -> ( v e. ( b i^i d ) -> E. y e. S ( v e. y /\ y C_ ( b i^i d ) ) ) ) ) )
23 22 imp42 
 |-  ( ( ( S e. TopBases /\ ( b e. S /\ d e. S ) ) /\ v e. ( b i^i d ) ) -> E. y e. S ( v e. y /\ y C_ ( b i^i d ) ) )
24 reeanv 
 |-  ( E. x e. R E. y e. S ( ( u e. x /\ x C_ ( a i^i c ) ) /\ ( v e. y /\ y C_ ( b i^i d ) ) ) <-> ( E. x e. R ( u e. x /\ x C_ ( a i^i c ) ) /\ E. y e. S ( v e. y /\ y C_ ( b i^i d ) ) ) )
25 opelxpi 
 |-  ( ( u e. x /\ v e. y ) -> <. u , v >. e. ( x X. y ) )
26 xpss12 
 |-  ( ( x C_ ( a i^i c ) /\ y C_ ( b i^i d ) ) -> ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) )
27 25 26 anim12i 
 |-  ( ( ( u e. x /\ v e. y ) /\ ( x C_ ( a i^i c ) /\ y C_ ( b i^i d ) ) ) -> ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
28 27 an4s 
 |-  ( ( ( u e. x /\ x C_ ( a i^i c ) ) /\ ( v e. y /\ y C_ ( b i^i d ) ) ) -> ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
29 28 reximi 
 |-  ( E. y e. S ( ( u e. x /\ x C_ ( a i^i c ) ) /\ ( v e. y /\ y C_ ( b i^i d ) ) ) -> E. y e. S ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
30 29 reximi 
 |-  ( E. x e. R E. y e. S ( ( u e. x /\ x C_ ( a i^i c ) ) /\ ( v e. y /\ y C_ ( b i^i d ) ) ) -> E. x e. R E. y e. S ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
31 24 30 sylbir 
 |-  ( ( E. x e. R ( u e. x /\ x C_ ( a i^i c ) ) /\ E. y e. S ( v e. y /\ y C_ ( b i^i d ) ) ) -> E. x e. R E. y e. S ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
32 20 23 31 syl2an 
 |-  ( ( ( ( R e. TopBases /\ ( a e. R /\ c e. R ) ) /\ u e. ( a i^i c ) ) /\ ( ( S e. TopBases /\ ( b e. S /\ d e. S ) ) /\ v e. ( b i^i d ) ) ) -> E. x e. R E. y e. S ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
33 32 an4s 
 |-  ( ( ( ( R e. TopBases /\ ( a e. R /\ c e. R ) ) /\ ( S e. TopBases /\ ( b e. S /\ d e. S ) ) ) /\ ( u e. ( a i^i c ) /\ v e. ( b i^i d ) ) ) -> E. x e. R E. y e. S ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
34 33 ralrimivva 
 |-  ( ( ( R e. TopBases /\ ( a e. R /\ c e. R ) ) /\ ( S e. TopBases /\ ( b e. S /\ d e. S ) ) ) -> A. u e. ( a i^i c ) A. v e. ( b i^i d ) E. x e. R E. y e. S ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
35 eleq1 
 |-  ( p = <. u , v >. -> ( p e. ( x X. y ) <-> <. u , v >. e. ( x X. y ) ) )
36 35 anbi1d 
 |-  ( p = <. u , v >. -> ( ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
37 36 2rexbidv 
 |-  ( p = <. u , v >. -> ( E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> E. x e. R E. y e. S ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
38 37 ralxp 
 |-  ( A. p e. ( ( a i^i c ) X. ( b i^i d ) ) E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> A. u e. ( a i^i c ) A. v e. ( b i^i d ) E. x e. R E. y e. S ( <. u , v >. e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
39 34 38 sylibr 
 |-  ( ( ( R e. TopBases /\ ( a e. R /\ c e. R ) ) /\ ( S e. TopBases /\ ( b e. S /\ d e. S ) ) ) -> A. p e. ( ( a i^i c ) X. ( b i^i d ) ) E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
40 39 an4s 
 |-  ( ( ( R e. TopBases /\ S e. TopBases ) /\ ( ( a e. R /\ c e. R ) /\ ( b e. S /\ d e. S ) ) ) -> A. p e. ( ( a i^i c ) X. ( b i^i d ) ) E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
41 40 anassrs 
 |-  ( ( ( ( R e. TopBases /\ S e. TopBases ) /\ ( a e. R /\ c e. R ) ) /\ ( b e. S /\ d e. S ) ) -> A. p e. ( ( a i^i c ) X. ( b i^i d ) ) E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
42 ineq12 
 |-  ( ( u = ( a X. b ) /\ v = ( c X. d ) ) -> ( u i^i v ) = ( ( a X. b ) i^i ( c X. d ) ) )
43 inxp 
 |-  ( ( a X. b ) i^i ( c X. d ) ) = ( ( a i^i c ) X. ( b i^i d ) )
44 42 43 eqtrdi 
 |-  ( ( u = ( a X. b ) /\ v = ( c X. d ) ) -> ( u i^i v ) = ( ( a i^i c ) X. ( b i^i d ) ) )
45 44 sseq2d 
 |-  ( ( u = ( a X. b ) /\ v = ( c X. d ) ) -> ( t C_ ( u i^i v ) <-> t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
46 45 anbi2d 
 |-  ( ( u = ( a X. b ) /\ v = ( c X. d ) ) -> ( ( p e. t /\ t C_ ( u i^i v ) ) <-> ( p e. t /\ t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
47 46 rexbidv 
 |-  ( ( u = ( a X. b ) /\ v = ( c X. d ) ) -> ( E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) <-> E. t e. B ( p e. t /\ t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
48 1 rexeqi 
 |-  ( E. t e. B ( p e. t /\ t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> E. t e. ran ( x e. R , y e. S |-> ( x X. y ) ) ( p e. t /\ t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
49 fvex 
 |-  ( 1st ` z ) e. _V
50 fvex 
 |-  ( 2nd ` z ) e. _V
51 49 50 xpex 
 |-  ( ( 1st ` z ) X. ( 2nd ` z ) ) e. _V
52 51 rgenw 
 |-  A. z e. ( R X. S ) ( ( 1st ` z ) X. ( 2nd ` z ) ) e. _V
53 vex 
 |-  x e. _V
54 vex 
 |-  y e. _V
55 53 54 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
56 53 54 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
57 55 56 xpeq12d 
 |-  ( z = <. x , y >. -> ( ( 1st ` z ) X. ( 2nd ` z ) ) = ( x X. y ) )
58 57 mpompt 
 |-  ( z e. ( R X. S ) |-> ( ( 1st ` z ) X. ( 2nd ` z ) ) ) = ( x e. R , y e. S |-> ( x X. y ) )
59 58 eqcomi 
 |-  ( x e. R , y e. S |-> ( x X. y ) ) = ( z e. ( R X. S ) |-> ( ( 1st ` z ) X. ( 2nd ` z ) ) )
60 eleq2 
 |-  ( t = ( ( 1st ` z ) X. ( 2nd ` z ) ) -> ( p e. t <-> p e. ( ( 1st ` z ) X. ( 2nd ` z ) ) ) )
61 sseq1 
 |-  ( t = ( ( 1st ` z ) X. ( 2nd ` z ) ) -> ( t C_ ( ( a i^i c ) X. ( b i^i d ) ) <-> ( ( 1st ` z ) X. ( 2nd ` z ) ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
62 60 61 anbi12d 
 |-  ( t = ( ( 1st ` z ) X. ( 2nd ` z ) ) -> ( ( p e. t /\ t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> ( p e. ( ( 1st ` z ) X. ( 2nd ` z ) ) /\ ( ( 1st ` z ) X. ( 2nd ` z ) ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
63 59 62 rexrnmptw 
 |-  ( A. z e. ( R X. S ) ( ( 1st ` z ) X. ( 2nd ` z ) ) e. _V -> ( E. t e. ran ( x e. R , y e. S |-> ( x X. y ) ) ( p e. t /\ t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> E. z e. ( R X. S ) ( p e. ( ( 1st ` z ) X. ( 2nd ` z ) ) /\ ( ( 1st ` z ) X. ( 2nd ` z ) ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
64 52 63 ax-mp 
 |-  ( E. t e. ran ( x e. R , y e. S |-> ( x X. y ) ) ( p e. t /\ t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> E. z e. ( R X. S ) ( p e. ( ( 1st ` z ) X. ( 2nd ` z ) ) /\ ( ( 1st ` z ) X. ( 2nd ` z ) ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
65 57 eleq2d 
 |-  ( z = <. x , y >. -> ( p e. ( ( 1st ` z ) X. ( 2nd ` z ) ) <-> p e. ( x X. y ) ) )
66 57 sseq1d 
 |-  ( z = <. x , y >. -> ( ( ( 1st ` z ) X. ( 2nd ` z ) ) C_ ( ( a i^i c ) X. ( b i^i d ) ) <-> ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
67 65 66 anbi12d 
 |-  ( z = <. x , y >. -> ( ( p e. ( ( 1st ` z ) X. ( 2nd ` z ) ) /\ ( ( 1st ` z ) X. ( 2nd ` z ) ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
68 67 rexxp 
 |-  ( E. z e. ( R X. S ) ( p e. ( ( 1st ` z ) X. ( 2nd ` z ) ) /\ ( ( 1st ` z ) X. ( 2nd ` z ) ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
69 48 64 68 3bitri 
 |-  ( E. t e. B ( p e. t /\ t C_ ( ( a i^i c ) X. ( b i^i d ) ) ) <-> E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) )
70 47 69 bitrdi 
 |-  ( ( u = ( a X. b ) /\ v = ( c X. d ) ) -> ( E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) <-> E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
71 44 70 raleqbidv 
 |-  ( ( u = ( a X. b ) /\ v = ( c X. d ) ) -> ( A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) <-> A. p e. ( ( a i^i c ) X. ( b i^i d ) ) E. x e. R E. y e. S ( p e. ( x X. y ) /\ ( x X. y ) C_ ( ( a i^i c ) X. ( b i^i d ) ) ) ) )
72 41 71 syl5ibrcom 
 |-  ( ( ( ( R e. TopBases /\ S e. TopBases ) /\ ( a e. R /\ c e. R ) ) /\ ( b e. S /\ d e. S ) ) -> ( ( u = ( a X. b ) /\ v = ( c X. d ) ) -> A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) ) )
73 72 rexlimdvva 
 |-  ( ( ( R e. TopBases /\ S e. TopBases ) /\ ( a e. R /\ c e. R ) ) -> ( E. b e. S E. d e. S ( u = ( a X. b ) /\ v = ( c X. d ) ) -> A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) ) )
74 17 73 syl5bir 
 |-  ( ( ( R e. TopBases /\ S e. TopBases ) /\ ( a e. R /\ c e. R ) ) -> ( ( E. b e. S u = ( a X. b ) /\ E. d e. S v = ( c X. d ) ) -> A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) ) )
75 74 rexlimdvva 
 |-  ( ( R e. TopBases /\ S e. TopBases ) -> ( E. a e. R E. c e. R ( E. b e. S u = ( a X. b ) /\ E. d e. S v = ( c X. d ) ) -> A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) ) )
76 16 75 syl5bi 
 |-  ( ( R e. TopBases /\ S e. TopBases ) -> ( ( u e. B /\ v e. B ) -> A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) ) )
77 76 ralrimivv 
 |-  ( ( R e. TopBases /\ S e. TopBases ) -> A. u e. B A. v e. B A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) )
78 1 txbasex 
 |-  ( ( R e. TopBases /\ S e. TopBases ) -> B e. _V )
79 isbasis2g 
 |-  ( B e. _V -> ( B e. TopBases <-> A. u e. B A. v e. B A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) ) )
80 78 79 syl 
 |-  ( ( R e. TopBases /\ S e. TopBases ) -> ( B e. TopBases <-> A. u e. B A. v e. B A. p e. ( u i^i v ) E. t e. B ( p e. t /\ t C_ ( u i^i v ) ) ) )
81 77 80 mpbird 
 |-  ( ( R e. TopBases /\ S e. TopBases ) -> B e. TopBases )