Theorem tpgprop2 14987

Description: In a topological group, the product of an open set by another set is open .

Hypotheses

Ref	Expression
trhom.1	|- X = ran G
trhom.2	|- F = (x e. X |-> (xGA))
trhom.3	|- G = (1st` K)
trhom.4	|- J = (2nd` K)
tpgprop2.1	|- .t = (cset` G)

Assertion

Ref	Expression
tpgprop2	|- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> (O.t A) e. J)

Distinct variable groups:   x,G   x,K   x,O   x,X

Proof of Theorem tpgprop2

Step	Hyp	Ref	Expression
1		trhom.3	. . . . 5 |- G = (1st` K)
2	1	topgrpgrp 14976	. . . 4 |- (K e. TopGrp -> G e. Grp)
3	2	3ad2ant1 897	. . 3 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> G e. Grp)
4		grprndm 9334	. . . . . . . 8 |- (G e. Grp -> ran G = dom dom G)
5		trhom.1	. . . . . . . 8 |- X = ran G
6	4, 5	syl5req 1941	. . . . . . 7 |- (G e. Grp -> dom dom G = X)
7	2, 6	syl 12	. . . . . 6 |- (K e. TopGrp -> dom dom G = X)
8	7	adantr 425	. . . . 5 |- ((K e. TopGrp /\ O e. J) -> dom dom G = X)
9		pweq 3036	. . . . . . 7 |- (dom dom G = X -> ~Pdom dom G = ~PX)
10	9	eleq2d 1964	. . . . . 6 |- (dom dom G = X -> (O e. ~Pdom dom G <-> O e. ~PX))
11		trhom.4	. . . . . . . . . 10 |- J = (2nd` K)
12	1, 11	topgrpbs 14974	. . . . . . . . 9 |- (K e. TopGrp -> ran G = U.J)
13		eqtr 1904	. . . . . . . . . . 11 |- ((X = ran G /\ ran G = U.J) -> X = U.J)
14		pweq 3036	. . . . . . . . . . . . 13 |- (X = U.J -> ~PX = ~PU.J)
15	14	sseq2d 2645	. . . . . . . . . . . 12 |- (X = U.J -> (J C_ ~PX <-> J C_ ~PU.J))
16	11	topgrptop 14977	. . . . . . . . . . . . 13 |- (K e. TopGrp -> J e. Top)
17		eqid 1884	. . . . . . . . . . . . . 14 |- U.J = U.J
18	17	topge 14911	. . . . . . . . . . . . 13 |- (J e. Top -> J C_ ~PU.J)
19	16, 18	syl 12	. . . . . . . . . . . 12 |- (K e. TopGrp -> J C_ ~PU.J)
20	15, 19	syl5bir 227	. . . . . . . . . . 11 |- (X = U.J -> (K e. TopGrp -> J C_ ~PX))
21	13, 20	syl 12	. . . . . . . . . 10 |- ((X = ran G /\ ran G = U.J) -> (K e. TopGrp -> J C_ ~PX))
22	5, 21	mpan 759	. . . . . . . . 9 |- (ran G = U.J -> (K e. TopGrp -> J C_ ~PX))
23	12, 22	mpcom 60	. . . . . . . 8 |- (K e. TopGrp -> J C_ ~PX)
24	23	sseld 2619	. . . . . . 7 |- (K e. TopGrp -> (O e. J -> O e. ~PX))
25	24	imp 377	. . . . . 6 |- ((K e. TopGrp /\ O e. J) -> O e. ~PX)
26	10, 25	syl5bir 227	. . . . 5 |- (dom dom G = X -> ((K e. TopGrp /\ O e. J) -> O e. ~Pdom dom G))
27	8, 26	mpcom 60	. . . 4 |- ((K e. TopGrp /\ O e. J) -> O e. ~Pdom dom G)
28	27	3adant2 895	. . 3 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> O e. ~Pdom dom G)
29	2, 4	syl 12	. . . . . . . 8 |- (K e. TopGrp -> ran G = dom dom G)
30	29, 5	syl5eq 1940	. . . . . . 7 |- (K e. TopGrp -> X = dom dom G)
31		pweq 3036	. . . . . . 7 |- (X = dom dom G -> ~PX = ~Pdom dom G)
32	30, 31	syl 12	. . . . . 6 |- (K e. TopGrp -> ~PX = ~Pdom dom G)
33	32	eleq2d 1964	. . . . 5 |- (K e. TopGrp -> (A e. ~PX <-> A e. ~Pdom dom G))
34	33	biimpa 460	. . . 4 |- ((K e. TopGrp /\ A e. ~PX) -> A e. ~Pdom dom G)
35	34	3adant3 896	. . 3 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> A e. ~Pdom dom G)
36		eqid 1884	. . . 4 |- dom dom G = dom dom G
37		tpgprop2.1	. . . 4 |- .t = (cset` G)
38	36, 37	iscst4 14522	. . 3 |- ((G e. Grp /\ O e. ~Pdom dom G /\ A e. ~Pdom dom G) -> (O.t A) = U_y e. A (O.t {y}))
39	3, 28, 35, 38	syl111anc 1100	. 2 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> (O.t A) = U_y e. A (O.t {y}))
40	16	3ad2ant1 897	. . 3 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> J e. Top)
41		simpl1 879	. . . . 5 |- (((K e. TopGrp /\ A e. ~PX /\ O e. J) /\ y e. A) -> K e. TopGrp)
42		elelpwi 3040	. . . . . . . 8 |- ((y e. A /\ A e. ~PX) -> y e. X)
43	42	expcom 403	. . . . . . 7 |- (A e. ~PX -> (y e. A -> y e. X))
44	43	3ad2ant2 898	. . . . . 6 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> (y e. A -> y e. X))
45	44	imp 377	. . . . 5 |- (((K e. TopGrp /\ A e. ~PX /\ O e. J) /\ y e. A) -> y e. X)
46		simpl3 881	. . . . 5 |- (((K e. TopGrp /\ A e. ~PX /\ O e. J) /\ y e. A) -> O e. J)
47		eqid 1884	. . . . . 6 |- (x e. X |-> (xGy)) = (x e. X |-> (xGy))
48	5, 47, 1, 11, 37	tpgprop1 14986	. . . . 5 |- ((K e. TopGrp /\ y e. X /\ O e. J) -> (O.t {y}) e. J)
49	41, 45, 46, 48	syl111anc 1100	. . . 4 |- (((K e. TopGrp /\ A e. ~PX /\ O e. J) /\ y e. A) -> (O.t {y}) e. J)
50	49	r19.21aiva 2176	. . 3 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> A.y e. A (O.t {y}) e. J)
51		iunopn 8868	. . 3 |- ((J e. Top /\ A.y e. A (O.t {y}) e. J) -> U_y e. A (O.t {y}) e. J)
52	40, 50, 51	syl11anc 524	. 2 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> U_y e. A (O.t {y}) e. J)
53	39, 52	eqeltrd 1971	1 |- ((K e. TopGrp /\ A e. ~PX /\ O e. J) -> (O.t A) e. J)

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105   C_ wss 2593  ~Pcpw 3032  {csn 3044  U.cuni 3177  U_ciun 3255  dom cdm 3986  ran crn 3987  ` cfv 3998  (class class class)co 4884   e. cmpt 5004  1stc1st 5018  2ndc2nd 5019  Topctop 8857  Grpcgr 9311  csetccst 14517  TopGrpctopgrp 14969

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-map 5383  df-top 8861  df-topsp 8862  df-bases 8863  df-topgen 8864  df-tx 8931  df-cn 9030  df-grp 9316  df-gid 9317  df-ginv 9318  df-gdiv 9319  df-homeo 10232  df-cst 14518  df-topgrp 14970

Copyright terms: Public domain