Theorem cldsubg 21112

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.

Step	Hyp	Ref	Expression
1		simpl1 1008	. . . . . . . 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 )
4	2, 3	tgptopon 21084	. . . . . . . 8 |- ( G e. TopGrp -> J e. (TopOn ` X ) )
5	1, 4	syl 17	. . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> J e. (TopOn ` X ) )
6		toponuni 19929	. . . . . . 7 |- ( J e. (TopOn ` X ) -> X = U. J )
7	5, 6	syl 17	. . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> X = U. J )
8	7	difeq1d 3582	. . . . 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 1009	. . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. (SubGrp ` G ) )
10		unisng 4232	. . . . . . . . 9 |- ( S e. (SubGrp ` G ) -> U. { S } = S )
11	9, 10	syl 17	. . . . . . . 8 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. { S } = S )
12	11	uneq2d 3620	. . . . . . 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 4235	. . . . . . . 8 |- U. ( ( ( X /. R ) \ { S } ) u. { S } ) = ( U. ( ( X /. R ) \ { S } ) u. U. { S } )
14		undif1 3870	. . . . . . . . . . 11 |- ( ( ( X /. R ) \ { S } ) u. { S } ) = ( ( X /. R ) u. { S } )
15		cldsubg.1	. . . . . . . . . . . . . . . 16 |- R = ( G ~QG S )
16		eqid 2422	. . . . . . . . . . . . . . . 16 |- ( 0g ` G ) = ( 0g ` G )
17	3, 15, 16	eqgid 16857	. . . . . . . . . . . . . . 15 |- ( S e. (SubGrp ` G ) -> [ ( 0g ` G ) ] R = S )
18	9, 17	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] R = S )
19		ovex 6330	. . . . . . . . . . . . . . . 16 |- ( G ~QG S ) e. _V
20	15, 19	eqeltri 2506	. . . . . . . . . . . . . . 15 |- R e. _V
21		tgpgrp 21080	. . . . . . . . . . . . . . . . 17 |- ( G e. TopGrp -> G e. Grp )
22	1, 21	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> G e. Grp )
23	3, 16	grpidcl 16682	. . . . . . . . . . . . . . . 16 |- ( G e. Grp -> ( 0g ` G ) e. X )
24	22, 23	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( 0g ` G ) e. X )
25		ecelqsg 7423	. . . . . . . . . . . . . . 15 |- ( ( R e. _V /\ ( 0g ` G ) e. X ) -> [ ( 0g ` G ) ] R e. ( X /. R ) )
26	20, 24, 25	sylancr 667	. . . . . . . . . . . . . 14 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] R e. ( X /. R ) )
27	18, 26	eqeltrrd 2511	. . . . . . . . . . . . 13 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. ( X /. R ) )
28	27	snssd 4142	. . . . . . . . . . . 12 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> { S } C_ ( X /. R ) )
29		ssequn2 3639	. . . . . . . . . . . 12 |- ( { S } C_ ( X /. R ) <-> ( ( X /. R ) u. { S } ) = ( X /. R ) )
30	28, 29	sylib 199	. . . . . . . . . . 11 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) u. { S } ) = ( X /. R ) )
31	14, 30	syl5eq 2475	. . . . . . . . . 10 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( ( X /. R ) \ { S } ) u. { S } ) = ( X /. R ) )
32	31	unieqd 4226	. . . . . . . . 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 ) )
33	3, 15	eqger 16855	. . . . . . . . . . 11 |- ( S e. (SubGrp ` G ) -> R Er X )
34	9, 33	syl 17	. . . . . . . . . 10 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> R Er X )
35	20	a1i 11	. . . . . . . . . 10 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> R e. _V )
36	34, 35	uniqs2 7430	. . . . . . . . 9 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( X /. R ) = X )
37	32, 36	eqtrd 2463	. . . . . . . 8 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( ( X /. R ) \ { S } ) u. { S } ) = X )
38	13, 37	syl5eqr 2477	. . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) u. U. { S } ) = X )
39	12, 38	eqtr3d 2465	. . . . . 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 3592	. . . . . . . . 9 |- ( ( X /. R ) \ { S } ) C_ ( X /. R )
41	40	unissi 4239	. . . . . . . 8 |- U. ( ( X /. R ) \ { S } ) C_ U. ( X /. R )
42	41, 36	syl5sseq 3512	. . . . . . 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 2620	. . . . . . . . . . . . 13 |- ( x =/= S <-> -. x = S )
44	34	adantr 466	. . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . 16 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> x e. ( X /. R ) )
46	27	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> S e. ( X /. R ) )
47	44, 45, 46	qsdisj 7445	. . . . . . . . . . . . . . 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 ) = (/) ) )
48	47	ord 378	. . . . . . . . . . . . . 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 3840	. . . . . . . . . . . . . 14 |- ( ( x i^i S ) = (/) <-> x C_ ( _V \ S ) )
50	48, 49	syl6ib 229	. . . . . . . . . . . . 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 ) ) )
51	43, 50	syl5bi 220	. . . . . . . . . . . 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 ) ) )
52	51	expimpd 606	. . . . . . . . . . 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 4122	. . . . . . . . . . 11 |- ( x e. ( ( X /. R ) \ { S } ) <-> ( x e. ( X /. R ) /\ x =/= S ) )
54		selpw 3986	. . . . . . . . . . 11 |- ( x e. ~P ( _V \ S ) <-> x C_ ( _V \ S ) )
55	52, 53, 54	3imtr4g 273	. . . . . . . . . 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 ) ) )
56	55	ssrdv 3470	. . . . . . . . 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 4385	. . . . . . . . 9 |- ( ( ( X /. R ) \ { S } ) C_ ~P ( _V \ S ) <-> U. ( ( X /. R ) \ { S } ) C_ ( _V \ S ) )
58	56, 57	sylib 199	. . . . . . . 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 3840	. . . . . . . 8 |- ( ( U. ( ( X /. R ) \ { S } ) i^i S ) = (/) <-> U. ( ( X /. R ) \ { S } ) C_ ( _V \ S ) )
60	58, 59	sylibr 215	. . . . . . 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 3884	. . . . . . 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 ) )
62	42, 60, 61	syl2anc 665	. . . . . 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 ) )
63	39, 62	mpbid 213	. . . . 5 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X \ U. ( ( X /. R ) \ { S } ) ) = S )
64	8, 63	eqtr3d 2465	. . . 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 19928	. . . . . . 7 |- ( J e. (TopOn ` X ) -> J e. Top )
66	5, 65	syl 17	. . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> J e. Top )
67		simpl3 1010	. . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X /. R ) e. Fin )
68		diffi 7806	. . . . . . 7 |- ( ( X /. R ) e. Fin -> ( ( X /. R ) \ { S } ) e. Fin )
69	67, 68	syl 17	. . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) e. Fin )
70		vex 3084	. . . . . . . . . 10 |- x e. _V
71	70	elqs 7421	. . . . . . . . 9 |- ( x e. ( X /. R ) <-> E. y e. X x = [ y ] R )
72		simpll2 1045	. . . . . . . . . . . . . 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 16810	. . . . . . . . . . . . . 14 |- ( S e. (SubGrp ` G ) -> G e. Grp )
74	72, 73	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> G e. Grp )
75	3	subgss 16806	. . . . . . . . . . . . . . 15 |- ( S e. (SubGrp ` G ) -> S C_ X )
76	9, 75	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S C_ X )
77	76	adantr 466	. . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S C_ X )
78		simpr 462	. . . . . . . . . . . . 13 |- ( ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> y e. X )
79		eqid 2422	. . . . . . . . . . . . . 14 |- ( +g ` G ) = ( +g ` G )
80	3, 15, 79	eqglact 16856	. . . . . . . . . . . . 13 |- ( ( G e. Grp /\ S C_ X /\ y e. X ) -> [ y ] R = ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) )
81	74, 77, 78, 80	syl3anc 1264	. . . . . . . . . . . 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 760	. . . . . . . . . . . . 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 2422	. . . . . . . . . . . . . . . 16 |- ( z e. X |-> ( y ( +g ` G ) z ) ) = ( z e. X |-> ( y ( +g ` G ) z ) )
84	83, 3, 79, 2	tgplacthmeo 21105	. . . . . . . . . . . . . . 15 |- ( ( G e. TopGrp /\ y e. X ) -> ( z e. X |-> ( y ( +g ` G ) z ) ) e. ( J Homeo J ) )
85	1, 84	sylan 473	. . . . . . . . . . . . . 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 ) )
86	76, 7	sseqtrd 3500	. . . . . . . . . . . . . . 15 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S C_ U. J )
87	86	adantr 466	. . . . . . . . . . . . . 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 2422	. . . . . . . . . . . . . . 15 |- U. J = U. J
89	88	hmeocld 20769	. . . . . . . . . . . . . 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 ) ) )
90	85, 87, 89	syl2anc 665	. . . . . . . . . . . . 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 ) ) )
91	82, 90	mpbid 213	. . . . . . . . . . . 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 ) )
92	81, 91	eqeltrd 2510	. . . . . . . . . . 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 2494	. . . . . . . . . . 11 |- ( x = [ y ] R -> ( x e. ( Clsd ` J ) <-> [ y ] R e. ( Clsd ` J ) ) )
94	92, 93	syl5ibrcom 225	. . . . . . . . . 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 ) ) )
95	94	rexlimdva 2917	. . . . . . . . 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 ) ) )
96	71, 95	syl5bi 220	. . . . . . . 8 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( x e. ( X /. R ) -> x e. ( Clsd ` J ) ) )
97	96	ssrdv 3470	. . . . . . 7 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X /. R ) C_ ( Clsd ` J ) )
98	97	ssdifssd 3603	. . . . . 6 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) C_ ( Clsd ` J ) )
99	88	unicld 20048	. . . . . 6 |- ( ( J e. Top /\ ( ( X /. R ) \ { S } ) e. Fin /\ ( ( X /. R ) \ { S } ) C_ ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) )
100	66, 69, 98, 99	syl3anc 1264	. . . . 5 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) )
101	88	cldopn 20033	. . . . 5 |- ( U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) -> ( U. J \ U. ( ( X /. R ) \ { S } ) ) e. J )
102	100, 101	syl 17	. . . 4 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. J \ U. ( ( X /. R ) \ { S } ) ) e. J )
103	64, 102	eqeltrrd 2511	. . 3 |- ( ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. J )
104	103	ex 435	. 2 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. ( Clsd ` J ) -> S e. J ) )
105	2	opnsubg 21109	. . . 4 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ S e. J ) -> S e. ( Clsd ` J ) )
106	105	3expia 1207	. . 3 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) ) -> ( S e. J -> S e. ( Clsd ` J ) ) )
107	106	3adant3 1025	. 2 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. J -> S e. ( Clsd ` J ) ) )
108	104, 107	impbid 193	1 |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. ( Clsd ` J ) <-> S e. J ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1868   =/= wne 2618   E.wrex 2776   _Vcvv 3081   \ cdif 3433   u. cun 3434   i^i cin 3435   C_ wss 3436   (/)c0 3761   ~Pcpw 3979   {csn 3996   U.cuni 4216   |-> cmpt 4479   "cima 4853   ` cfv 5598  (class class class)co 6302   Er wer 7365   [cec 7366   /.cqs 7367   Fincfn 7574   Basecbs 15109   +g cplusg 15178   TopOpenctopn 15308   0gc0g 15326   Grpcgrp 16657  SubGrpcsubg 16799   ~_QG cqg 16801   Topctop 19904  TopOnctopon 19905   Clsdccld 20018   Homeochmeo 20755   TopGrpctgp 21073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-om 6704  df-1st 6804  df-2nd 6805  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-ec 7370  df-qs 7374  df-map 7479  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-nn 10611  df-2 10669  df-ndx 15112  df-slot 15113  df-base 15114  df-sets 15115  df-ress 15116  df-plusg 15191  df-0g 15328  df-topgen 15330  df-plusf 16475  df-mgm 16476  df-sgrp 16515  df-mnd 16525  df-grp 16661  df-minusg 16662  df-sbg 16663  df-subg 16802  df-eqg 16804  df-top 19908  df-bases 19909  df-topon 19910  df-topsp 19911  df-cld 20021  df-cn 20230  df-cnp 20231  df-tx 20564  df-hmeo 20757  df-tmd 21074  df-tgp 21075

This theorem is referenced by: (None)