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 ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) = { ∅ , ( 𝐴 × 𝐵 ) }

Proof

Step Hyp Ref Expression
1 neq0 ⊢ ( ¬ 𝑥 = ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
2 indistop ⊢ { ∅ , 𝐴 } ∈ Top
3 indistop ⊢ { ∅ , 𝐵 } ∈ Top
4 eltx ⊢ ( ( { ∅ , 𝐴 } ∈ Top ∧ { ∅ , 𝐵 } ∈ Top ) → ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ { ∅ , 𝐴 } ∃ 𝑤 ∈ { ∅ , 𝐵 } ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
5 2 3 4 mp2an ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ { ∅ , 𝐴 } ∃ 𝑤 ∈ { ∅ , 𝐵 } ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) )
6 rsp ⊢ ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ { ∅ , 𝐴 } ∃ 𝑤 ∈ { ∅ , 𝐵 } ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) → ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ∈ { ∅ , 𝐴 } ∃ 𝑤 ∈ { ∅ , 𝐵 } ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
7 5 6 sylbi ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ∈ { ∅ , 𝐴 } ∃ 𝑤 ∈ { ∅ , 𝐵 } ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) )
8 elssuni ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → 𝑥 ⊆ ∪ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) )
9 indisuni ⊢ ( I ‘ 𝐴 ) = ∪ { ∅ , 𝐴 }
10 indisuni ⊢ ( I ‘ 𝐵 ) = ∪ { ∅ , 𝐵 }
11 2 3 9 10 txunii ⊢ ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) = ∪ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } )
12 8 11 sseqtrrdi ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → 𝑥 ⊆ ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) )
13 12 ad2antrr ⊢ ( ( ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∧ ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑥 ⊆ ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) )
14 ne0i ⊢ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) → ( 𝑧 × 𝑤 ) ≠ ∅ )
15 14 ad2antrl ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( 𝑧 × 𝑤 ) ≠ ∅ )
16 xpnz ⊢ ( ( 𝑧 ≠ ∅ ∧ 𝑤 ≠ ∅ ) ↔ ( 𝑧 × 𝑤 ) ≠ ∅ )
17 15 16 sylibr ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( 𝑧 ≠ ∅ ∧ 𝑤 ≠ ∅ ) )
18 17 simpld ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑧 ≠ ∅ )
19 18 neneqd ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ¬ 𝑧 = ∅ )
20 simpll ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑧 ∈ { ∅ , 𝐴 } )
21 indislem ⊢ { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 }
22 20 21 eleqtrrdi ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑧 ∈ { ∅ , ( I ‘ 𝐴 ) } )
23 elpri ⊢ ( 𝑧 ∈ { ∅ , ( I ‘ 𝐴 ) } → ( 𝑧 = ∅ ∨ 𝑧 = ( I ‘ 𝐴 ) ) )
24 22 23 syl ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( 𝑧 = ∅ ∨ 𝑧 = ( I ‘ 𝐴 ) ) )
25 24 ord ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( ¬ 𝑧 = ∅ → 𝑧 = ( I ‘ 𝐴 ) ) )
26 19 25 mpd ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑧 = ( I ‘ 𝐴 ) )
27 17 simprd ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑤 ≠ ∅ )
28 27 neneqd ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ¬ 𝑤 = ∅ )
29 simplr ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑤 ∈ { ∅ , 𝐵 } )
30 indislem ⊢ { ∅ , ( I ‘ 𝐵 ) } = { ∅ , 𝐵 }
31 29 30 eleqtrrdi ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑤 ∈ { ∅ , ( I ‘ 𝐵 ) } )
32 elpri ⊢ ( 𝑤 ∈ { ∅ , ( I ‘ 𝐵 ) } → ( 𝑤 = ∅ ∨ 𝑤 = ( I ‘ 𝐵 ) ) )
33 31 32 syl ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( 𝑤 = ∅ ∨ 𝑤 = ( I ‘ 𝐵 ) ) )
34 33 ord ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( ¬ 𝑤 = ∅ → 𝑤 = ( I ‘ 𝐵 ) ) )
35 28 34 mpd ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑤 = ( I ‘ 𝐵 ) )
36 26 35 xpeq12d ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( 𝑧 × 𝑤 ) = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) )
37 simprr ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( 𝑧 × 𝑤 ) ⊆ 𝑥 )
38 36 37 eqsstrrd ⊢ ( ( ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ⊆ 𝑥 )
39 38 adantll ⊢ ( ( ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∧ ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ⊆ 𝑥 )
40 13 39 eqssd ⊢ ( ( ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∧ ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ) ∧ ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) → 𝑥 = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) )
41 40 ex ⊢ ( ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∧ ( 𝑧 ∈ { ∅ , 𝐴 } ∧ 𝑤 ∈ { ∅ , 𝐵 } ) ) → ( ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) → 𝑥 = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
42 41 rexlimdvva ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → ( ∃ 𝑧 ∈ { ∅ , 𝐴 } ∃ 𝑤 ∈ { ∅ , 𝐵 } ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) → 𝑥 = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
43 7 42 syld ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → ( 𝑦 ∈ 𝑥 → 𝑥 = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
44 43 exlimdv ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → ( ∃ 𝑦 𝑦 ∈ 𝑥 → 𝑥 = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
45 1 44 biimtrid ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → ( ¬ 𝑥 = ∅ → 𝑥 = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
46 45 orrd ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → ( 𝑥 = ∅ ∨ 𝑥 = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
47 vex ⊢ 𝑥 ∈ V
48 47 elpr ⊢ ( 𝑥 ∈ { ∅ , ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) } ↔ ( 𝑥 = ∅ ∨ 𝑥 = ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
49 46 48 sylibr ⊢ ( 𝑥 ∈ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) → 𝑥 ∈ { ∅ , ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) } )
50 49 ssriv ⊢ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ⊆ { ∅ , ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) }
51 9 toptopon ⊢ ( { ∅ , 𝐴 } ∈ Top ↔ { ∅ , 𝐴 } ∈ ( TopOn ‘ ( I ‘ 𝐴 ) ) )
52 2 51 mpbi ⊢ { ∅ , 𝐴 } ∈ ( TopOn ‘ ( I ‘ 𝐴 ) )
53 10 toptopon ⊢ ( { ∅ , 𝐵 } ∈ Top ↔ { ∅ , 𝐵 } ∈ ( TopOn ‘ ( I ‘ 𝐵 ) ) )
54 3 53 mpbi ⊢ { ∅ , 𝐵 } ∈ ( TopOn ‘ ( I ‘ 𝐵 ) )
55 txtopon ⊢ ( ( { ∅ , 𝐴 } ∈ ( TopOn ‘ ( I ‘ 𝐴 ) ) ∧ { ∅ , 𝐵 } ∈ ( TopOn ‘ ( I ‘ 𝐵 ) ) ) → ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∈ ( TopOn ‘ ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
56 52 54 55 mp2an ⊢ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∈ ( TopOn ‘ ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) )
57 topgele ⊢ ( ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∈ ( TopOn ‘ ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) → ( { ∅ , ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) } ⊆ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∧ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ⊆ 𝒫 ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) ) )
58 56 57 ax-mp ⊢ ( { ∅ , ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) } ⊆ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ∧ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) ⊆ 𝒫 ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) )
59 58 simpli ⊢ { ∅ , ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) } ⊆ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } )
60 50 59 eqssi ⊢ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) = { ∅ , ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) }
61 txindislem ⊢ ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) = ( I ‘ ( 𝐴 × 𝐵 ) )
62 61 preq2i ⊢ { ∅ , ( ( I ‘ 𝐴 ) × ( I ‘ 𝐵 ) ) } = { ∅ , ( I ‘ ( 𝐴 × 𝐵 ) ) }
63 indislem ⊢ { ∅ , ( I ‘ ( 𝐴 × 𝐵 ) ) } = { ∅ , ( 𝐴 × 𝐵 ) }
64 60 62 63 3eqtri ⊢ ( { ∅ , 𝐴 } ×t { ∅ , 𝐵 } ) = { ∅ , ( 𝐴 × 𝐵 ) }