Metamath Proof Explorer

Theorem istgp

Description: The predicate "is a topological group". Definition 1 of BourbakiTop1 p. III.1. (Contributed by FL, 18-Apr-2010) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses istgp.1 ⊢ J = TopOpen ⁡ G
istgp.2 ⊢ I = inv g ⁡ G
Assertion istgp ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopMnd ∧ I ∈ J Cn J

Proof

Step Hyp Ref Expression
1 istgp.1 ⊢ J = TopOpen ⁡ G
2 istgp.2 ⊢ I = inv g ⁡ G
3 elin ⊢ G ∈ Grp ∩ TopMnd ↔ G ∈ Grp ∧ G ∈ TopMnd
4 3 anbi1i ⊢ G ∈ Grp ∩ TopMnd ∧ I ∈ J Cn J ↔ G ∈ Grp ∧ G ∈ TopMnd ∧ I ∈ J Cn J
5 fvexd ⊢ f = G → TopOpen ⁡ f ∈ V
6 simpl ⊢ f = G ∧ j = TopOpen ⁡ f → f = G
7 6 fveq2d ⊢ f = G ∧ j = TopOpen ⁡ f → inv g ⁡ f = inv g ⁡ G
8 7 2 eqtr4di ⊢ f = G ∧ j = TopOpen ⁡ f → inv g ⁡ f = I
9 id ⊢ j = TopOpen ⁡ f → j = TopOpen ⁡ f
10 fveq2 ⊢ f = G → TopOpen ⁡ f = TopOpen ⁡ G
11 10 1 eqtr4di ⊢ f = G → TopOpen ⁡ f = J
12 9 11 sylan9eqr ⊢ f = G ∧ j = TopOpen ⁡ f → j = J
13 12 12 oveq12d ⊢ f = G ∧ j = TopOpen ⁡ f → j Cn j = J Cn J
14 8 13 eleq12d ⊢ f = G ∧ j = TopOpen ⁡ f → inv g ⁡ f ∈ j Cn j ↔ I ∈ J Cn J
15 5 14 sbcied ⊢ f = G → [˙ TopOpen ⁡ f / j]˙ inv g ⁡ f ∈ j Cn j ↔ I ∈ J Cn J
16 df-tgp ⊢ TopGrp = f ∈ Grp ∩ TopMnd | [˙ TopOpen ⁡ f / j]˙ inv g ⁡ f ∈ j Cn j
17 15 16 elrab2 ⊢ G ∈ TopGrp ↔ G ∈ Grp ∩ TopMnd ∧ I ∈ J Cn J
18 df-3an ⊢ G ∈ Grp ∧ G ∈ TopMnd ∧ I ∈ J Cn J ↔ G ∈ Grp ∧ G ∈ TopMnd ∧ I ∈ J Cn J
19 4 17 18 3bitr4i ⊢ G ∈ TopGrp ↔ G ∈ Grp ∧ G ∈ TopMnd ∧ I ∈ J Cn J