Metamath Proof Explorer

Theorem indistgp

Description: Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses distgp.1 ⊢ B = Base G
distgp.2 ⊢ J = TopOpen ⁡ G
Assertion indistgp ⊢ G ∈ Grp ∧ J = ∅ B → G ∈ TopGrp

Proof

Step Hyp Ref Expression
1 distgp.1 ⊢ B = Base G
2 distgp.2 ⊢ J = TopOpen ⁡ G
3 simpl ⊢ G ∈ Grp ∧ J = ∅ B → G ∈ Grp
4 simpr ⊢ G ∈ Grp ∧ J = ∅ B → J = ∅ B
5 1 fvexi ⊢ B ∈ V
6 indistopon ⊢ B ∈ V → ∅ B ∈ TopOn ⁡ B
7 5 6 ax-mp ⊢ ∅ B ∈ TopOn ⁡ B
8 4 7 eqeltrdi ⊢ G ∈ Grp ∧ J = ∅ B → J ∈ TopOn ⁡ B
9 1 2 istps ⊢ G ∈ TopSp ↔ J ∈ TopOn ⁡ B
10 8 9 sylibr ⊢ G ∈ Grp ∧ J = ∅ B → G ∈ TopSp
11 eqid ⊢ - G = - G
12 1 11 grpsubf ⊢ G ∈ Grp → - G : B × B ⟶ B
13 12 adantr ⊢ G ∈ Grp ∧ J = ∅ B → - G : B × B ⟶ B
14 5 5 xpex ⊢ B × B ∈ V
15 5 14 elmap ⊢ - G ∈ B B × B ↔ - G : B × B ⟶ B
16 13 15 sylibr ⊢ G ∈ Grp ∧ J = ∅ B → - G ∈ B B × B
17 4 oveq2d ⊢ G ∈ Grp ∧ J = ∅ B → J × t J Cn J = J × t J Cn ∅ B
18 txtopon ⊢ J ∈ TopOn ⁡ B ∧ J ∈ TopOn ⁡ B → J × t J ∈ TopOn ⁡ B × B
19 8 8 18 syl2anc ⊢ G ∈ Grp ∧ J = ∅ B → J × t J ∈ TopOn ⁡ B × B
20 cnindis ⊢ J × t J ∈ TopOn ⁡ B × B ∧ B ∈ V → J × t J Cn ∅ B = B B × B
21 19 5 20 sylancl ⊢ G ∈ Grp ∧ J = ∅ B → J × t J Cn ∅ B = B B × B
22 17 21 eqtrd ⊢ G ∈ Grp ∧ J = ∅ B → J × t J Cn J = B B × B
23 16 22 eleqtrrd ⊢ G ∈ Grp ∧ J = ∅ B → - G ∈ J × t J Cn J
24 2 11 istgp2 ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopSp ∧ - G ∈ J × t J Cn J
25 3 10 23 24 syl3anbrc ⊢ G ∈ Grp ∧ J = ∅ B → G ∈ TopGrp