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	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
	istgp.2	⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion	istgp	⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		istgp.1	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2		istgp.2	⊢ 𝐼 = ( invg ‘ 𝐺 )
3		elin	⊢ ( 𝐺 ∈ ( Grp ∩ TopMnd ) ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ) )
4	3	anbi1i	⊢ ( ( 𝐺 ∈ ( Grp ∩ TopMnd ) ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ) ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
5		fvexd	⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) ∈ V )
6		simpl	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → 𝑓 = 𝐺 )
7	6	fveq2d	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( invg ‘ 𝑓 ) = ( invg ‘ 𝐺 ) )
8	7 2	eqtr4di	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( invg ‘ 𝑓 ) = 𝐼 )
9		id	⊢ ( 𝑗 = ( TopOpen ‘ 𝑓 ) → 𝑗 = ( TopOpen ‘ 𝑓 ) )
10		fveq2	⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) = ( TopOpen ‘ 𝐺 ) )
11	10 1	eqtr4di	⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) = 𝐽 )
12	9 11	sylan9eqr	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → 𝑗 = 𝐽 )
13	12 12	oveq12d	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( 𝑗 Cn 𝑗 ) = ( 𝐽 Cn 𝐽 ) )
14	8 13	eleq12d	⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) ↔ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
15	5 14	sbcied	⊢ ( 𝑓 = 𝐺 → ( [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) ↔ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
16		df-tgp	⊢ TopGrp = { 𝑓 ∈ ( Grp ∩ TopMnd ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) }
17	15 16	elrab2	⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ ( Grp ∩ TopMnd ) ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
18		df-3an	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ) ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
19	4 17 18	3bitr4i	⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )