This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑗 ) }