Definition df-tgp

Description: Define the class of all topological groups. A topological group is a group whose operation and inverse function are continuous. (Contributed by FL, 18-Apr-2010)

	Ref	Expression
Assertion	df-tgp	⊢ TopGrp = { 𝑓 ∈ ( Grp ∩ TopMnd ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctgp	⊢ TopGrp
1		vf	⊢ 𝑓
2		cgrp	⊢ Grp
3		ctmd	⊢ TopMnd
4	2 3	cin	⊢ ( Grp ∩ TopMnd )
5		ctopn	⊢ TopOpen
6	1	cv	⊢ 𝑓
7	6 5	cfv	⊢ ( TopOpen ‘ 𝑓 )
8		vj	⊢ 𝑗
9		cminusg	⊢ invg
10	6 9	cfv	⊢ ( invg ‘ 𝑓 )
11	8	cv	⊢ 𝑗
12		ccn	⊢ Cn
13	11 11 12	co	⊢ ( 𝑗 Cn 𝑗 )
14	10 13	wcel	⊢ ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 )
15	14 8 7	wsbc	⊢ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 )
16	15 1 4	crab	⊢ { 𝑓 ∈ ( Grp ∩ TopMnd ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) }
17	0 16	wceq	⊢ TopGrp = { 𝑓 ∈ ( Grp ∩ TopMnd ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) }