MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cldsubg Structured version   Unicode version
Theorem cldsubg 19656
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 991 . . . . . . . 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 19628 . . . . . . . 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 18507 . . . . . . 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 3468 . . . . 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 992 . . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. (SubGrp ` G ) )
10 unisng 4102 . . . . . . . . 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 3505 . . . . . . 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 4105 . . . . . . . 8 |- U. ( ( ( X /. R ) \ { S } ) u. { S } ) = ( U. ( ( X /. R ) \ { S } ) u. U. { S } )
14 undif1 3749 . . . . . . . . . . 11 |- ( ( ( X /. R ) \ { S } ) u. { S } ) = ( ( X /. R ) u. { S } )
15 cldsubg.1 . . . . . . . . . . . . . . . 16 |- R = ( G ~QG S )
16 eqid 2438 . . . . . . . . . . . . . . . 16 |- ( 0g ` G ) = ( 0g ` G )
173, 15, 16eqgid 15724 . . . . . . . . . . . . . . 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 6111 . . . . . . . . . . . . . . . 16 |- ( G ~QG S ) e. _V
2015, 19eqeltri 2508 . . . . . . . . . . . . . . 15 |- R e. _V
21 tgpgrp 19624 . . . . . . . . . . . . . . . . 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 15557 . . . . . . . . . . . . . . . 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 7147 . . . . . . . . . . . . . . 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 2513 . . . . . . . . . . . . 13 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. ( X /. R ) )
2827snssd 4013 . . . . . . . . . . . 12 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> { S } C_ ( X /. R ) )
29 ssequn2 3524 . . . . . . . . . . . 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 2482 . . . . . . . . . 10 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( ( X /. R ) \ { S } ) u. { S } ) = ( X /. R ) )
3231unieqd 4096 . . . . . . . . 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 15722 . . . . . . . . . . 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 7154 . . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( X /. R ) = X )
3732, 36eqtrd 2470 . . . . . . . 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 2484 . . . . . . 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 2472 . . . . . 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 3478 . . . . . . . . 9 |- ( ( X /. R ) \ { S } ) C_ ( X /. R )
4140unissi 4109 . . . . . . . 8 |- U. ( ( X /. R ) \ { S } ) C_ U. ( X /. R )
4241, 36syl5sseq 3399 . . . . . . 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 2603 . . . . . . . . . . . . 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 7169 . . . . . . . . . . . . . . 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 3721 . . . . . . . . . . . . . 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 3995 . . . . . . . . . . 11 |- ( x e. ( ( X /. R ) \ { S } ) <-> ( x e. ( X /. R ) /\ x =/= S ) )
54 selpw 3862 . . . . . . . . . . 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 3357 . . . . . . . . 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 4251 . . . . . . . . 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 3721 . . . . . . . 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 3762 . . . . . . 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 2472 . . . 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 18506 . . . . . . 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 993 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X /. R ) e. Fin )
68 diffi 7535 . . . . . . 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 2970 . . . . . . . . . 10 |- x e. _V
7170elqs 7145 . . . . . . . . 9 |- ( x e. ( X /. R ) <-> E. y e. X x = [ y ] R )
72 simpll2 1028 . . . . . . . . . . . . . 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 15677 . . . . . . . . . . . . . 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 15673 . . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . 14 |- ( +g ` G ) = ( +g ` G )
803, 15, 79eqglact 15723 . . . . . . . . . . . . 13 |- ( ( G e. Grp /\ S C_ X /\ y e. X ) -> [ y ] R = ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) )
8174, 77, 78, 80syl3anc 1218 . . . . . . . . . . . 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 754 . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . . 16 |- ( z e. X |-> ( y ( +g ` G ) z ) ) = ( z e. X |-> ( y ( +g ` G ) z ) )
8483, 3, 79, 2tgplacthmeo 19649 . . . . . . . . . . . . . . 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 3387 . . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . . . 15 |- U. J = U. J
8988hmeocld 19315 . . . . . . . . . . . . . 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 2512 . . . . . . . . . . 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 2498 . . . . . . . . . . 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 2836 . . . . . . . . 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 3357 . . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X /. R ) C_ ( Clsd ` J ) )
9897ssdifssd 3489 . . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) C_ ( Clsd ` J ) )
9988unicld 18625 . . . . . 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 1218 . . . . 5 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) )
10188cldopn 18610 . . . . 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 2513 . . 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 19653 . . . 4 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ S e. J ) -> S e. ( Clsd ` J ) )
1061053expia 1189 . . 3 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) ) -> ( S e. J -> S e. ( Clsd ` J ) ) )
1071063adant3 1008 . 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 965   = wceq 1369   e. wcel 1756   =/= wne 2601   E.wrex 2711   _Vcvv 2967   \ cdif 3320   u. cun 3321   i^i cin 3322   C_ wss 3323   (/)c0 3632   ~Pcpw 3855   {csn 3872   U.cuni 4086   e. cmpt 4345   "cima 4838   ` cfv 5413  (class class class)co 6086   Er wer 7090   [cec 7091   /.cqs 7092   Fincfn 7302   Basecbs 14166   +g cplusg 14230   TopOpenctopn 14352   0gc0g 14370   Grpcgrp 15402  SubGrpcsubg 15666   ~QG cqg 15668   Topctop 18473  TopOnctopon 18474   Clsdccld 18595   Homeochmeo 19301   TopGrpctgp 19617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-iin 4169  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-ec 7095  df-qs 7099  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-0g 14372  df-topgen 14374  df-mnd 15407  df-plusf 15408  df-grp 15536  df-minusg 15537  df-sbg 15538  df-subg 15669  df-eqg 15671  df-top 18478  df-bases 18480  df-topon 18481  df-topsp 18482  df-cld 18598  df-cn 18806  df-cnp 18807  df-tx 19110  df-hmeo 19303  df-tmd 19618  df-tgp 19619
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator