Metamath Proof Explorer

Theorem txindis

Description: The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion txindis 
|- ( { (/) , A } tX { (/) , B } ) = { (/) , ( A X. B ) }

Proof

Step Hyp Ref Expression
1 neq0 
 |-  ( -. x = (/) <-> E. y y e. x )
2 indistop 
 |-  { (/) , A } e. Top
3 indistop 
 |-  { (/) , B } e. Top
4 eltx 
 |-  ( ( { (/) , A } e. Top /\ { (/) , B } e. Top ) -> ( x e. ( { (/) , A } tX { (/) , B } ) <-> A. y e. x E. z e. { (/) , A } E. w e. { (/) , B } ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) )
5 2 3 4 mp2an 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) <-> A. y e. x E. z e. { (/) , A } E. w e. { (/) , B } ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) )
6 rsp 
 |-  ( A. y e. x E. z e. { (/) , A } E. w e. { (/) , B } ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) -> ( y e. x -> E. z e. { (/) , A } E. w e. { (/) , B } ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) )
7 5 6 sylbi 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> ( y e. x -> E. z e. { (/) , A } E. w e. { (/) , B } ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) )
8 elssuni 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> x C_ U. ( { (/) , A } tX { (/) , B } ) )
9 indisuni 
 |-  ( _I ` A ) = U. { (/) , A }
10 indisuni 
 |-  ( _I ` B ) = U. { (/) , B }
11 2 3 9 10 txunii 
 |-  ( ( _I ` A ) X. ( _I ` B ) ) = U. ( { (/) , A } tX { (/) , B } )
12 8 11 sseqtrrdi 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> x C_ ( ( _I ` A ) X. ( _I ` B ) ) )
13 12 ad2antrr 
 |-  ( ( ( x e. ( { (/) , A } tX { (/) , B } ) /\ ( z e. { (/) , A } /\ w e. { (/) , B } ) ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> x C_ ( ( _I ` A ) X. ( _I ` B ) ) )
14 ne0i 
 |-  ( y e. ( z X. w ) -> ( z X. w ) =/= (/) )
15 14 ad2antrl 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( z X. w ) =/= (/) )
16 xpnz 
 |-  ( ( z =/= (/) /\ w =/= (/) ) <-> ( z X. w ) =/= (/) )
17 15 16 sylibr 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( z =/= (/) /\ w =/= (/) ) )
18 17 simpld 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> z =/= (/) )
19 18 neneqd 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> -. z = (/) )
20 simpll 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> z e. { (/) , A } )
21 indislem 
 |-  { (/) , ( _I ` A ) } = { (/) , A }
22 20 21 eleqtrrdi 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> z e. { (/) , ( _I ` A ) } )
23 elpri 
 |-  ( z e. { (/) , ( _I ` A ) } -> ( z = (/) \/ z = ( _I ` A ) ) )
24 22 23 syl 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( z = (/) \/ z = ( _I ` A ) ) )
25 24 ord 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( -. z = (/) -> z = ( _I ` A ) ) )
26 19 25 mpd 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> z = ( _I ` A ) )
27 17 simprd 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> w =/= (/) )
28 27 neneqd 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> -. w = (/) )
29 simplr 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> w e. { (/) , B } )
30 indislem 
 |-  { (/) , ( _I ` B ) } = { (/) , B }
31 29 30 eleqtrrdi 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> w e. { (/) , ( _I ` B ) } )
32 elpri 
 |-  ( w e. { (/) , ( _I ` B ) } -> ( w = (/) \/ w = ( _I ` B ) ) )
33 31 32 syl 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( w = (/) \/ w = ( _I ` B ) ) )
34 33 ord 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( -. w = (/) -> w = ( _I ` B ) ) )
35 28 34 mpd 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> w = ( _I ` B ) )
36 26 35 xpeq12d 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( z X. w ) = ( ( _I ` A ) X. ( _I ` B ) ) )
37 simprr 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( z X. w ) C_ x )
38 36 37 eqsstrrd 
 |-  ( ( ( z e. { (/) , A } /\ w e. { (/) , B } ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( ( _I ` A ) X. ( _I ` B ) ) C_ x )
39 38 adantll 
 |-  ( ( ( x e. ( { (/) , A } tX { (/) , B } ) /\ ( z e. { (/) , A } /\ w e. { (/) , B } ) ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> ( ( _I ` A ) X. ( _I ` B ) ) C_ x )
40 13 39 eqssd 
 |-  ( ( ( x e. ( { (/) , A } tX { (/) , B } ) /\ ( z e. { (/) , A } /\ w e. { (/) , B } ) ) /\ ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) -> x = ( ( _I ` A ) X. ( _I ` B ) ) )
41 40 ex 
 |-  ( ( x e. ( { (/) , A } tX { (/) , B } ) /\ ( z e. { (/) , A } /\ w e. { (/) , B } ) ) -> ( ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) -> x = ( ( _I ` A ) X. ( _I ` B ) ) ) )
42 41 rexlimdvva 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> ( E. z e. { (/) , A } E. w e. { (/) , B } ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) -> x = ( ( _I ` A ) X. ( _I ` B ) ) ) )
43 7 42 syld 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> ( y e. x -> x = ( ( _I ` A ) X. ( _I ` B ) ) ) )
44 43 exlimdv 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> ( E. y y e. x -> x = ( ( _I ` A ) X. ( _I ` B ) ) ) )
45 1 44 syl5bi 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> ( -. x = (/) -> x = ( ( _I ` A ) X. ( _I ` B ) ) ) )
46 45 orrd 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> ( x = (/) \/ x = ( ( _I ` A ) X. ( _I ` B ) ) ) )
47 vex 
 |-  x e. _V
48 47 elpr 
 |-  ( x e. { (/) , ( ( _I ` A ) X. ( _I ` B ) ) } <-> ( x = (/) \/ x = ( ( _I ` A ) X. ( _I ` B ) ) ) )
49 46 48 sylibr 
 |-  ( x e. ( { (/) , A } tX { (/) , B } ) -> x e. { (/) , ( ( _I ` A ) X. ( _I ` B ) ) } )
50 49 ssriv 
 |-  ( { (/) , A } tX { (/) , B } ) C_ { (/) , ( ( _I ` A ) X. ( _I ` B ) ) }
51 9 toptopon 
 |-  ( { (/) , A } e. Top <-> { (/) , A } e. ( TopOn ` ( _I ` A ) ) )
52 2 51 mpbi 
 |-  { (/) , A } e. ( TopOn ` ( _I ` A ) )
53 10 toptopon 
 |-  ( { (/) , B } e. Top <-> { (/) , B } e. ( TopOn ` ( _I ` B ) ) )
54 3 53 mpbi 
 |-  { (/) , B } e. ( TopOn ` ( _I ` B ) )
55 txtopon 
 |-  ( ( { (/) , A } e. ( TopOn ` ( _I ` A ) ) /\ { (/) , B } e. ( TopOn ` ( _I ` B ) ) ) -> ( { (/) , A } tX { (/) , B } ) e. ( TopOn ` ( ( _I ` A ) X. ( _I ` B ) ) ) )
56 52 54 55 mp2an 
 |-  ( { (/) , A } tX { (/) , B } ) e. ( TopOn ` ( ( _I ` A ) X. ( _I ` B ) ) )
57 topgele 
 |-  ( ( { (/) , A } tX { (/) , B } ) e. ( TopOn ` ( ( _I ` A ) X. ( _I ` B ) ) ) -> ( { (/) , ( ( _I ` A ) X. ( _I ` B ) ) } C_ ( { (/) , A } tX { (/) , B } ) /\ ( { (/) , A } tX { (/) , B } ) C_ ~P ( ( _I ` A ) X. ( _I ` B ) ) ) )
58 56 57 ax-mp 
 |-  ( { (/) , ( ( _I ` A ) X. ( _I ` B ) ) } C_ ( { (/) , A } tX { (/) , B } ) /\ ( { (/) , A } tX { (/) , B } ) C_ ~P ( ( _I ` A ) X. ( _I ` B ) ) )
59 58 simpli 
 |-  { (/) , ( ( _I ` A ) X. ( _I ` B ) ) } C_ ( { (/) , A } tX { (/) , B } )
60 50 59 eqssi 
 |-  ( { (/) , A } tX { (/) , B } ) = { (/) , ( ( _I ` A ) X. ( _I ` B ) ) }
61 txindislem 
 |-  ( ( _I ` A ) X. ( _I ` B ) ) = ( _I ` ( A X. B ) )
62 61 preq2i 
 |-  { (/) , ( ( _I ` A ) X. ( _I ` B ) ) } = { (/) , ( _I ` ( A X. B ) ) }
63 indislem 
 |-  { (/) , ( _I ` ( A X. B ) ) } = { (/) , ( A X. B ) }
64 60 62 63 3eqtri 
 |-  ( { (/) , A } tX { (/) , B } ) = { (/) , ( A X. B ) }