Metamath Proof Explorer

Theorem neitx

Description: The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018)

Ref Expression
Hypotheses neitx.x 
|- X = U. J
neitx.y 
|- Y = U. K
Assertion neitx 
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) )

Proof

Step Hyp Ref Expression
1 neitx.x 
 |-  X = U. J
2 neitx.y 
 |-  Y = U. K
3 1 neii1 
 |-  ( ( J e. Top /\ A e. ( ( nei ` J ) ` C ) ) -> A C_ X )
4 3 ad2ant2r 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> A C_ X )
5 2 neii1 
 |-  ( ( K e. Top /\ B e. ( ( nei ` K ) ` D ) ) -> B C_ Y )
6 5 ad2ant2l 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> B C_ Y )
7 xpss12 
 |-  ( ( A C_ X /\ B C_ Y ) -> ( A X. B ) C_ ( X X. Y ) )
8 4 6 7 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) C_ ( X X. Y ) )
9 1 2 txuni 
 |-  ( ( J e. Top /\ K e. Top ) -> ( X X. Y ) = U. ( J tX K ) )
10 9 adantr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( X X. Y ) = U. ( J tX K ) )
11 8 10 sseqtrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) C_ U. ( J tX K ) )
12 simp-5l 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> ( J e. Top /\ K e. Top ) )
13 simp-4r 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> a e. J )
14 simplr 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> b e. K )
15 txopn 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( a e. J /\ b e. K ) ) -> ( a X. b ) e. ( J tX K ) )
16 12 13 14 15 syl12anc 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> ( a X. b ) e. ( J tX K ) )
17 simpr1l 
 |-  ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( ( C C_ a /\ a C_ A ) /\ b e. K /\ ( D C_ b /\ b C_ B ) ) ) -> C C_ a )
18 17 3anassrs 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> C C_ a )
19 simprl 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> D C_ b )
20 xpss12 
 |-  ( ( C C_ a /\ D C_ b ) -> ( C X. D ) C_ ( a X. b ) )
21 18 19 20 syl2anc 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> ( C X. D ) C_ ( a X. b ) )
22 simpr1r 
 |-  ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( ( C C_ a /\ a C_ A ) /\ b e. K /\ ( D C_ b /\ b C_ B ) ) ) -> a C_ A )
23 22 3anassrs 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> a C_ A )
24 simprr 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> b C_ B )
25 xpss12 
 |-  ( ( a C_ A /\ b C_ B ) -> ( a X. b ) C_ ( A X. B ) )
26 23 24 25 syl2anc 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> ( a X. b ) C_ ( A X. B ) )
27 sseq2 
 |-  ( c = ( a X. b ) -> ( ( C X. D ) C_ c <-> ( C X. D ) C_ ( a X. b ) ) )
28 sseq1 
 |-  ( c = ( a X. b ) -> ( c C_ ( A X. B ) <-> ( a X. b ) C_ ( A X. B ) ) )
29 27 28 anbi12d 
 |-  ( c = ( a X. b ) -> ( ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) <-> ( ( C X. D ) C_ ( a X. b ) /\ ( a X. b ) C_ ( A X. B ) ) ) )
30 29 rspcev 
 |-  ( ( ( a X. b ) e. ( J tX K ) /\ ( ( C X. D ) C_ ( a X. b ) /\ ( a X. b ) C_ ( A X. B ) ) ) -> E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) )
31 16 21 26 30 syl12anc 
 |-  ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) )
32 neii2 
 |-  ( ( K e. Top /\ B e. ( ( nei ` K ) ` D ) ) -> E. b e. K ( D C_ b /\ b C_ B ) )
33 32 ad2ant2l 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> E. b e. K ( D C_ b /\ b C_ B ) )
34 33 ad2antrr 
 |-  ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) -> E. b e. K ( D C_ b /\ b C_ B ) )
35 31 34 r19.29a 
 |-  ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) -> E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) )
36 neii2 
 |-  ( ( J e. Top /\ A e. ( ( nei ` J ) ` C ) ) -> E. a e. J ( C C_ a /\ a C_ A ) )
37 36 ad2ant2r 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> E. a e. J ( C C_ a /\ a C_ A ) )
38 35 37 r19.29a 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) )
39 txtop 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J tX K ) e. Top )
40 39 adantr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( J tX K ) e. Top )
41 1 neiss2 
 |-  ( ( J e. Top /\ A e. ( ( nei ` J ) ` C ) ) -> C C_ X )
42 41 ad2ant2r 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> C C_ X )
43 2 neiss2 
 |-  ( ( K e. Top /\ B e. ( ( nei ` K ) ` D ) ) -> D C_ Y )
44 43 ad2ant2l 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> D C_ Y )
45 xpss12 
 |-  ( ( C C_ X /\ D C_ Y ) -> ( C X. D ) C_ ( X X. Y ) )
46 42 44 45 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( C X. D ) C_ ( X X. Y ) )
47 46 10 sseqtrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( C X. D ) C_ U. ( J tX K ) )
48 eqid 
 |-  U. ( J tX K ) = U. ( J tX K )
49 48 isnei 
 |-  ( ( ( J tX K ) e. Top /\ ( C X. D ) C_ U. ( J tX K ) ) -> ( ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) <-> ( ( A X. B ) C_ U. ( J tX K ) /\ E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) ) ) )
50 40 47 49 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) <-> ( ( A X. B ) C_ U. ( J tX K ) /\ E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) ) ) )
51 11 38 50 mpbir2and 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) )