MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cldsubg Structured version   Unicode version
Theorem cldsubg 20482
Description: A subgroup of finite index is closed iff it is open. (Contributed by Mario Carneiro, 20-Sep-2015.)
Hypotheses
Ref Expression
subgntr.h |- J = ( TopOpen ` G )
cldsubg.1 |- R = ( G ~QG S )
cldsubg.2 |- X = ( Base ` G )
Assertion
Ref Expression
cldsubg |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. ( Clsd ` J ) <-> S e. J ) )
Proof of Theorem cldsubg
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl1 1000 . . . . . . . 8 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> G e. TopGrp )
2 subgntr.h . . . . . . . . 9 |- J = ( TopOpen ` G )
3 cldsubg.2 . . . . . . . . 9 |- X = ( Base ` G )
42, 3tgptopon 20454 . . . . . . . 8 |- ( G e. TopGrp -> J e. (TopOn ` X ) )
51, 4syl 16 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> J e. (TopOn ` X ) )
6 toponuni 19301 . . . . . . 7 |- ( J e. (TopOn ` X ) -> X = U. J )
75, 6syl 16 . . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> X = U. J )
87difeq1d 3606 . . . . 5 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X \ U. ( ( X /. R ) \ { S } ) ) = ( U. J \ U. ( ( X /. R ) \ { S } ) ) )
9 simpl2 1001 . . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. (SubGrp ` G ) )
10 unisng 4250 . . . . . . . . 9 |- ( S e. (SubGrp ` G ) -> U. { S } = S )
119, 10syl 16 . . . . . . . 8 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. { S } = S )
1211uneq2d 3643 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) u. U. { S } ) = ( U. ( ( X /. R ) \ { S } ) u. S ) )
13 uniun 4253 . . . . . . . 8 |- U. ( ( ( X /. R ) \ { S } ) u. { S } ) = ( U. ( ( X /. R ) \ { S } ) u. U. { S } )
14 undif1 3889 . . . . . . . . . . 11 |- ( ( ( X /. R ) \ { S } ) u. { S } ) = ( ( X /. R ) u. { S } )
15 cldsubg.1 . . . . . . . . . . . . . . . 16 |- R = ( G ~QG S )
16 eqid 2443 . . . . . . . . . . . . . . . 16 |- ( 0g ` G ) = ( 0g ` G )
173, 15, 16eqgid 16127 . . . . . . . . . . . . . . 15 |- ( S e. (SubGrp ` G ) -> [ ( 0g ` G ) ] R = S )
189, 17syl 16 . . . . . . . . . . . . . 14 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] R = S )
19 ovex 6309 . . . . . . . . . . . . . . . 16 |- ( G ~QG S ) e. _V
2015, 19eqeltri 2527 . . . . . . . . . . . . . . 15 |- R e. _V
21 tgpgrp 20450 . . . . . . . . . . . . . . . . 17 |- ( G e. TopGrp -> G e. Grp )
221, 21syl 16 . . . . . . . . . . . . . . . 16 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> G e. Grp )
233, 16grpidcl 15952 . . . . . . . . . . . . . . . 16 |- ( G e. Grp -> ( 0g ` G ) e. X )
2422, 23syl 16 . . . . . . . . . . . . . . 15 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( 0g ` G ) e. X )
25 ecelqsg 7368 . . . . . . . . . . . . . . 15 |- ( ( R e. _V /\ ( 0g ` G ) e. X ) -> [ ( 0g ` G ) ] R e. ( X /. R ) )
2620, 24, 25sylancr 663 . . . . . . . . . . . . . 14 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] R e. ( X /. R ) )
2718, 26eqeltrrd 2532 . . . . . . . . . . . . 13 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. ( X /. R ) )
2827snssd 4160 . . . . . . . . . . . 12 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> { S } C_ ( X /. R ) )
29 ssequn2 3662 . . . . . . . . . . . 12 |- ( { S } C_ ( X /. R ) <-> ( ( X /. R ) u. { S } ) = ( X /. R ) )
3028, 29sylib 196 . . . . . . . . . . 11 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) u. { S } ) = ( X /. R ) )
3114, 30syl5eq 2496 . . . . . . . . . 10 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( ( X /. R ) \ { S } ) u. { S } ) = ( X /. R ) )
3231unieqd 4244 . . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( ( X /. R ) \ { S } ) u. { S } ) = U. ( X /. R ) )
333, 15eqger 16125 . . . . . . . . . . 11 |- ( S e. (SubGrp ` G ) -> R Er X )
349, 33syl 16 . . . . . . . . . 10 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> R Er X )
3520a1i 11 . . . . . . . . . 10 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> R e. _V )
3634, 35uniqs2 7375 . . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( X /. R ) = X )
3732, 36eqtrd 2484 . . . . . . . 8 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( ( X /. R ) \ { S } ) u. { S } ) = X )
3813, 37syl5eqr 2498 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) u. U. { S } ) = X )
3912, 38eqtr3d 2486 . . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) u. S ) = X )
40 difss 3616 . . . . . . . . 9 |- ( ( X /. R ) \ { S } ) C_ ( X /. R )
4140unissi 4257 . . . . . . . 8 |- U. ( ( X /. R ) \ { S } ) C_ U. ( X /. R )
4241, 36syl5sseq 3537 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) C_ X )
43 df-ne 2640 . . . . . . . . . . . . 13 |- ( x =/= S <-> -. x = S )
4434adantr 465 . . . . . . . . . . . . . . . 16 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> R Er X )
45 simpr 461 . . . . . . . . . . . . . . . 16 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> x e. ( X /. R ) )
4627adantr 465 . . . . . . . . . . . . . . . 16 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> S e. ( X /. R ) )
4744, 45, 46qsdisj 7390 . . . . . . . . . . . . . . 15 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> ( x = S \/ ( x i^i S ) = (/) ) )
4847ord 377 . . . . . . . . . . . . . 14 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> ( -. x = S -> ( x i^i S ) = (/) ) )
49 disj2 3860 . . . . . . . . . . . . . 14 |- ( ( x i^i S ) = (/) <-> x C_ ( _V \ S ) )
5048, 49syl6ib 226 . . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> ( -. x = S -> x C_ ( _V \ S ) ) )
5143, 50syl5bi 217 . . . . . . . . . . . 12 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> ( x =/= S -> x C_ ( _V \ S ) ) )
5251expimpd 603 . . . . . . . . . . 11 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( x e. ( X /. R ) /\ x =/= S ) -> x C_ ( _V \ S ) ) )
53 eldifsn 4140 . . . . . . . . . . 11 |- ( x e. ( ( X /. R ) \ { S } ) <-> ( x e. ( X /. R ) /\ x =/= S ) )
54 selpw 4004 . . . . . . . . . . 11 |- ( x e. ~P ( _V \ S ) <-> x C_ ( _V \ S ) )
5552, 53, 543imtr4g 270 . . . . . . . . . 10 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( x e. ( ( X /. R ) \ { S } ) -> x e. ~P ( _V \ S ) ) )
5655ssrdv 3495 . . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) C_ ~P ( _V \ S ) )
57 sspwuni 4401 . . . . . . . . 9 |- ( ( ( X /. R ) \ { S } ) C_ ~P ( _V \ S ) <-> U. ( ( X /. R ) \ { S } ) C_ ( _V \ S ) )
5856, 57sylib 196 . . . . . . . 8 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) C_ ( _V \ S ) )
59 disj2 3860 . . . . . . . 8 |- ( ( U. ( ( X /. R ) \ { S } ) i^i S ) = (/) <-> U. ( ( X /. R ) \ { S } ) C_ ( _V \ S ) )
6058, 59sylibr 212 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) i^i S ) = (/) )
61 uneqdifeq 3902 . . . . . . 7 |- ( ( U. ( ( X /. R ) \ { S } ) C_ X /\ ( U. ( ( X /. R ) \ { S } ) i^i S ) = (/) ) -> ( ( U. ( ( X /. R ) \ { S } ) u. S ) = X <-> ( X \ U. ( ( X /. R ) \ { S } ) ) = S ) )
6242, 60, 61syl2anc 661 . . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( U. ( ( X /. R ) \ { S } ) u. S ) = X <-> ( X \ U. ( ( X /. R ) \ { S } ) ) = S ) )
6339, 62mpbid 210 . . . . 5 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X \ U. ( ( X /. R ) \ { S } ) ) = S )
648, 63eqtr3d 2486 . . . 4 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. J \ U. ( ( X /. R ) \ { S } ) ) = S )
65 topontop 19300 . . . . . . 7 |- ( J e. (TopOn ` X ) -> J e. Top )
665, 65syl 16 . . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> J e. Top )
67 simpl3 1002 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X /. R ) e. Fin )
68 diffi 7753 . . . . . . 7 |- ( ( X /. R ) e. Fin -> ( ( X /. R ) \ { S } ) e. Fin )
6967, 68syl 16 . . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) e. Fin )
70 vex 3098 . . . . . . . . . 10 |- x e. _V
7170elqs 7366 . . . . . . . . 9 |- ( x e. ( X /. R ) <-> E. y e. X x = [ y ] R )
72 simpll2 1037 . . . . . . . . . . . . . 14 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S e. (SubGrp ` G ) )
73 subgrcl 16080 . . . . . . . . . . . . . 14 |- ( S e. (SubGrp ` G ) -> G e. Grp )
7472, 73syl 16 . . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> G e. Grp )
753subgss 16076 . . . . . . . . . . . . . . 15 |- ( S e. (SubGrp ` G ) -> S C_ X )
769, 75syl 16 . . . . . . . . . . . . . 14 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S C_ X )
7776adantr 465 . . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S C_ X )
78 simpr 461 . . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> y e. X )
79 eqid 2443 . . . . . . . . . . . . . 14 |- ( +g ` G ) = ( +g ` G )
803, 15, 79eqglact 16126 . . . . . . . . . . . . 13 |- ( ( G e. Grp /\ S C_ X /\ y e. X ) -> [ y ] R = ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) )
8174, 77, 78, 80syl3anc 1229 . . . . . . . . . . . 12 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> [ y ] R = ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) )
82 simplr 755 . . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S e. ( Clsd ` J ) )
83 eqid 2443 . . . . . . . . . . . . . . . 16 |- ( z e. X |-> ( y ( +g ` G ) z ) ) = ( z e. X |-> ( y ( +g ` G ) z ) )
8483, 3, 79, 2tgplacthmeo 20475 . . . . . . . . . . . . . . 15 |- ( ( G e. TopGrp /\ y e. X ) -> ( z e. X |-> ( y ( +g ` G ) z ) ) e. ( J Homeo J ) )
851, 84sylan 471 . . . . . . . . . . . . . 14 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> ( z e. X |-> ( y ( +g ` G ) z ) ) e. ( J Homeo J ) )
8676, 7sseqtrd 3525 . . . . . . . . . . . . . . 15 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S C_ U. J )
8786adantr 465 . . . . . . . . . . . . . 14 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S C_ U. J )
88 eqid 2443 . . . . . . . . . . . . . . 15 |- U. J = U. J
8988hmeocld 20141 . . . . . . . . . . . . . 14 |- ( ( ( z e. X |-> ( y ( +g ` G ) z ) ) e. ( J Homeo J ) /\ S C_ U. J ) -> ( S e. ( Clsd ` J ) <-> ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) e. ( Clsd ` J ) ) )
9085, 87, 89syl2anc 661 . . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> ( S e. ( Clsd ` J ) <-> ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) e. ( Clsd ` J ) ) )
9182, 90mpbid 210 . . . . . . . . . . . 12 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) e. ( Clsd ` J ) )
9281, 91eqeltrd 2531 . . . . . . . . . . 11 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> [ y ] R e. ( Clsd ` J ) )
93 eleq1 2515 . . . . . . . . . . 11 |- ( x = [ y ] R -> ( x e. ( Clsd ` J ) <-> [ y ] R e. ( Clsd ` J ) ) )
9492, 93syl5ibrcom 222 . . . . . . . . . 10 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> ( x = [ y ] R -> x e. ( Clsd ` J ) ) )
9594rexlimdva 2935 . . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( E. y e. X x = [ y ] R -> x e. ( Clsd ` J ) ) )
9671, 95syl5bi 217 . . . . . . . 8 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( x e. ( X /. R ) -> x e. ( Clsd ` J ) ) )
9796ssrdv 3495 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X /. R ) C_ ( Clsd ` J ) )
9897ssdifssd 3627 . . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) C_ ( Clsd ` J ) )
9988unicld 19420 . . . . . 6 |- ( ( J e. Top /\ ( ( X /. R ) \ { S } ) e. Fin /\ ( ( X /. R ) \ { S } ) C_ ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) )
10066, 69, 98, 99syl3anc 1229 . . . . 5 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) )
10188cldopn 19405 . . . . 5 |- ( U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) -> ( U. J \ U. ( ( X /. R ) \ { S } ) ) e. J )
102100, 101syl 16 . . . 4 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. J \ U. ( ( X /. R ) \ { S } ) ) e. J )
10364, 102eqeltrrd 2532 . . 3 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. J )
104103ex 434 . 2 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. ( Clsd ` J ) -> S e. J ) )
1052opnsubg 20479 . . . 4 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ S e. J ) -> S e. ( Clsd ` J ) )
1061053expia 1199 . . 3 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) ) -> ( S e. J -> S e. ( Clsd ` J ) ) )
1071063adant3 1017 . 2 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. J -> S e. ( Clsd ` J ) ) )
108104, 107impbid 191 1 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. ( Clsd ` J ) <-> S e. J ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 974   = wceq 1383   e. wcel 1804   =/= wne 2638   E.wrex 2794   _Vcvv 3095   \ cdif 3458   u. cun 3459   i^i cin 3460   C_ wss 3461   (/)c0 3770   ~Pcpw 3997   {csn 4014   U.cuni 4234   |-> cmpt 4495   "cima 4992   ` cfv 5578  (class class class)co 6281   Er wer 7310   [cec 7311   /.cqs 7312   Fincfn 7518   Basecbs 14509   +g cplusg 14574   TopOpenctopn 14696   0gc0g 14714   Grpcgrp 15927  SubGrpcsubg 16069   ~QG cqg 16071   Topctop 19267  TopOnctopon 19268   Clsdccld 19390   Homeochmeo 20127   TopGrpctgp 20443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-ec 7315  df-qs 7319  df-map 7424  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10543  df-2 10600  df-ndx 14512  df-slot 14513  df-base 14514  df-sets 14515  df-ress 14516  df-plusg 14587  df-0g 14716  df-topgen 14718  df-plusf 15745  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-grp 15931  df-minusg 15932  df-sbg 15933  df-subg 16072  df-eqg 16074  df-top 19272  df-bases 19274  df-topon 19275  df-topsp 19276  df-cld 19393  df-cn 19601  df-cnp 19602  df-tx 19936  df-hmeo 20129  df-tmd 20444  df-tgp 20445
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator