symgtgp

Description: The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015) (Proof shortened by AV, 30-Mar-2024)

		Ref	Expression
	Hypothesis	symgtgp.g	$⊢ G = SymGrp (A)$
	Assertion	symgtgp	$⊢ A \in V \to G \in TopGrp$

Proof

Step	Hyp	Ref	Expression
1		symgtgp.g	$⊢ G = SymGrp (A)$
2	1	symggrp	$⊢ A \in V \to G \in Grp$
3		eqid	$⊢ EndoFMnd (A) = EndoFMnd (A)$
4	3	efmndtmd	$⊢ A \in V \to EndoFMnd (A) \in TopMnd$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6	3 1 5	symgsubmefmnd	$⊢ A \in V \to {Base}_{G} \in SubMnd (EndoFMnd (A))$
7	1 5 3	symgressbas	$⊢ G = EndoFMnd (A) ↾_{𝑠} {Base}_{G}$
8	7	submtmd	$⊢ (EndoFMnd (A) \in TopMnd \land {Base}_{G} \in SubMnd (EndoFMnd (A))) \to G \in TopMnd$
9	4 6 8	syl2anc	$⊢ A \in V \to G \in TopMnd$
10		eqid	$⊢ \prod_{𝑡} (A \times \{𝒫 A\}) = \prod_{𝑡} (A \times \{𝒫 A\})$
11	1 5	symgtopn	$⊢ A \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G} = TopOpen (G)$
12		distopon	$⊢ A \in V \to 𝒫 A \in TopOn (A)$
13	10	pttoponconst	$⊢ (A \in V \land 𝒫 A \in TopOn (A)) \to \prod_{𝑡} (A \times \{𝒫 A\}) \in TopOn (A^{A})$
14	12 13	mpdan	$⊢ A \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) \in TopOn (A^{A})$
15	1 5	elsymgbas	$⊢ A \in V \to (x \in {Base}_{G} \leftrightarrow x : A \underset{1-1 onto}{⟶} A)$
16		f1of	$⊢ x : A \underset{1-1 onto}{⟶} A \to x : A ⟶ A$
17		elmapg	$⊢ (A \in V \land A \in V) \to (x \in (A^{A}) \leftrightarrow x : A ⟶ A)$
18	17	anidms	$⊢ A \in V \to (x \in (A^{A}) \leftrightarrow x : A ⟶ A)$
19	16 18	imbitrrid	$⊢ A \in V \to (x : A \underset{1-1 onto}{⟶} A \to x \in (A^{A}))$
20	15 19	sylbid	$⊢ A \in V \to (x \in {Base}_{G} \to x \in (A^{A}))$
21	20	ssrdv	$⊢ A \in V \to {Base}_{G} \subseteq A^{A}$
22		resttopon	$⊢ (\prod_{𝑡} (A \times \{𝒫 A\}) \in TopOn (A^{A}) \land {Base}_{G} \subseteq A^{A}) \to \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G} \in TopOn ({Base}_{G})$
23	14 21 22	syl2anc	$⊢ A \in V \to \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G} \in TopOn ({Base}_{G})$
24	11 23	eqeltrrd	$⊢ A \in V \to TopOpen (G) \in TopOn ({Base}_{G})$
25		id	$⊢ A \in V \to A \in V$
26		distop	$⊢ A \in V \to 𝒫 A \in Top$
27		fconst6g	$⊢ 𝒫 A \in Top \to (A \times \{𝒫 A\}) : A ⟶ Top$
28	26 27	syl	$⊢ A \in V \to (A \times \{𝒫 A\}) : A ⟶ Top$
29	15	biimpa	$⊢ (A \in V \land x \in {Base}_{G}) \to x : A \underset{1-1 onto}{⟶} A$
30		f1ocnv	$⊢ x : A \underset{1-1 onto}{⟶} A \to x^{-1} : A \underset{1-1 onto}{⟶} A$
31		f1of	$⊢ x^{-1} : A \underset{1-1 onto}{⟶} A \to x^{-1} : A ⟶ A$
32	29 30 31	3syl	$⊢ (A \in V \land x \in {Base}_{G}) \to x^{-1} : A ⟶ A$
33	32	ffvelcdmda	$⊢ ((A \in V \land x \in {Base}_{G}) \land y \in A) \to x^{-1} (y) \in A$
34	33	an32s	$⊢ ((A \in V \land y \in A) \land x \in {Base}_{G}) \to x^{-1} (y) \in A$
35	34	fmpttd	$⊢ (A \in V \land y \in A) \to (x \in {Base}_{G} ⟼ x^{-1} (y)) : {Base}_{G} ⟶ A$
36	35	adantr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (x \in {Base}_{G} ⟼ x^{-1} (y)) : {Base}_{G} ⟶ A$
37		cnveq	$⊢ x = f \to x^{-1} = f^{-1}$
38	37	fveq1d	$⊢ x = f \to x^{-1} (y) = f^{-1} (y)$
39		eqid	$⊢ (x \in {Base}_{G} ⟼ x^{-1} (y)) = (x \in {Base}_{G} ⟼ x^{-1} (y))$
40		fvex	$⊢ f^{-1} (y) \in V$
41	38 39 40	fvmpt	$⊢ f \in {Base}_{G} \to (x \in {Base}_{G} ⟼ x^{-1} (y)) (f) = f^{-1} (y)$
42	41	ad2antlr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land t \in 𝒫 A) \to (x \in {Base}_{G} ⟼ x^{-1} (y)) (f) = f^{-1} (y)$
43	42	eleq1d	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land t \in 𝒫 A) \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) (f) \in t \leftrightarrow f^{-1} (y) \in t)$
44		eqid	$⊢ (u \in {Base}_{G} ⟼ u (f^{-1} (y))) = (u \in {Base}_{G} ⟼ u (f^{-1} (y)))$
45	44	mptiniseg	$⊢ y \in V \to {(u \in {Base}_{G} ⟼ u (f^{-1} (y)))}^{-1} [\{y\}] = \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}$
46	45	elv	$⊢ {(u \in {Base}_{G} ⟼ u (f^{-1} (y)))}^{-1} [\{y\}] = \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}$
47		eqid	$⊢ \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G} = \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G}$
48	14	ad2antrr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to \prod_{𝑡} (A \times \{𝒫 A\}) \in TopOn (A^{A})$
49	21	ad2antrr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to {Base}_{G} \subseteq A^{A}$
50		toponuni	$⊢ \prod_{𝑡} (A \times \{𝒫 A\}) \in TopOn (A^{A}) \to A^{A} = ⋃ \prod_{𝑡} (A \times \{𝒫 A\})$
51		mpteq1	$⊢ A^{A} = ⋃ \prod_{𝑡} (A \times \{𝒫 A\}) \to (u \in (A^{A}) ⟼ u (f^{-1} (y))) = (u \in ⋃ \prod_{𝑡} (A \times \{𝒫 A\}) ⟼ u (f^{-1} (y)))$
52	48 50 51	3syl	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (u \in (A^{A}) ⟼ u (f^{-1} (y))) = (u \in ⋃ \prod_{𝑡} (A \times \{𝒫 A\}) ⟼ u (f^{-1} (y)))$
53		simpll	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to A \in V$
54	28	ad2antrr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (A \times \{𝒫 A\}) : A ⟶ Top$
55	1 5	elsymgbas	$⊢ A \in V \to (f \in {Base}_{G} \leftrightarrow f : A \underset{1-1 onto}{⟶} A)$
56	55	adantr	$⊢ (A \in V \land y \in A) \to (f \in {Base}_{G} \leftrightarrow f : A \underset{1-1 onto}{⟶} A)$
57	56	biimpa	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to f : A \underset{1-1 onto}{⟶} A$
58		f1ocnv	$⊢ f : A \underset{1-1 onto}{⟶} A \to f^{-1} : A \underset{1-1 onto}{⟶} A$
59		f1of	$⊢ f^{-1} : A \underset{1-1 onto}{⟶} A \to f^{-1} : A ⟶ A$
60	57 58 59	3syl	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to f^{-1} : A ⟶ A$
61		simplr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to y \in A$
62	60 61	ffvelcdmd	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to f^{-1} (y) \in A$
63		eqid	$⊢ ⋃ \prod_{𝑡} (A \times \{𝒫 A\}) = ⋃ \prod_{𝑡} (A \times \{𝒫 A\})$
64	63 10	ptpjcn	$⊢ (A \in V \land (A \times \{𝒫 A\}) : A ⟶ Top \land f^{-1} (y) \in A) \to (u \in ⋃ \prod_{𝑡} (A \times \{𝒫 A\}) ⟼ u (f^{-1} (y))) \in (\prod_{𝑡} (A \times \{𝒫 A\}) Cn (A \times \{𝒫 A\}) (f^{-1} (y)))$
65	53 54 62 64	syl3anc	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (u \in ⋃ \prod_{𝑡} (A \times \{𝒫 A\}) ⟼ u (f^{-1} (y))) \in (\prod_{𝑡} (A \times \{𝒫 A\}) Cn (A \times \{𝒫 A\}) (f^{-1} (y)))$
66	26	ad2antrr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to 𝒫 A \in Top$
67		fvconst2g	$⊢ (𝒫 A \in Top \land f^{-1} (y) \in A) \to (A \times \{𝒫 A\}) (f^{-1} (y)) = 𝒫 A$
68	66 62 67	syl2anc	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (A \times \{𝒫 A\}) (f^{-1} (y)) = 𝒫 A$
69	68	oveq2d	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to \prod_{𝑡} (A \times \{𝒫 A\}) Cn (A \times \{𝒫 A\}) (f^{-1} (y)) = \prod_{𝑡} (A \times \{𝒫 A\}) Cn 𝒫 A$
70	65 69	eleqtrd	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (u \in ⋃ \prod_{𝑡} (A \times \{𝒫 A\}) ⟼ u (f^{-1} (y))) \in (\prod_{𝑡} (A \times \{𝒫 A\}) Cn 𝒫 A)$
71	52 70	eqeltrd	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (u \in (A^{A}) ⟼ u (f^{-1} (y))) \in (\prod_{𝑡} (A \times \{𝒫 A\}) Cn 𝒫 A)$
72	47 48 49 71	cnmpt1res	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (u \in {Base}_{G} ⟼ u (f^{-1} (y))) \in ((\prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G}) Cn 𝒫 A)$
73	11	oveq1d	$⊢ A \in V \to (\prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G}) Cn 𝒫 A = TopOpen (G) Cn 𝒫 A$
74	73	ad2antrr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (\prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G}) Cn 𝒫 A = TopOpen (G) Cn 𝒫 A$
75	72 74	eleqtrd	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (u \in {Base}_{G} ⟼ u (f^{-1} (y))) \in (TopOpen (G) Cn 𝒫 A)$
76		snelpwi	$⊢ y \in A \to \{y\} \in 𝒫 A$
77	76	ad2antlr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to \{y\} \in 𝒫 A$
78		cnima	$⊢ ((u \in {Base}_{G} ⟼ u (f^{-1} (y))) \in (TopOpen (G) Cn 𝒫 A) \land \{y\} \in 𝒫 A) \to {(u \in {Base}_{G} ⟼ u (f^{-1} (y)))}^{-1} [\{y\}] \in TopOpen (G)$
79	75 77 78	syl2anc	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to {(u \in {Base}_{G} ⟼ u (f^{-1} (y)))}^{-1} [\{y\}] \in TopOpen (G)$
80	46 79	eqeltrrid	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \in TopOpen (G)$
81	80	adantr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \in TopOpen (G)$
82		fveq1	$⊢ u = f \to u (f^{-1} (y)) = f (f^{-1} (y))$
83	82	eqeq1d	$⊢ u = f \to (u (f^{-1} (y)) = y \leftrightarrow f (f^{-1} (y)) = y)$
84		simplr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to f \in {Base}_{G}$
85	57	adantr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to f : A \underset{1-1 onto}{⟶} A$
86		simpllr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to y \in A$
87		f1ocnvfv2	$⊢ (f : A \underset{1-1 onto}{⟶} A \land y \in A) \to f (f^{-1} (y)) = y$
88	85 86 87	syl2anc	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to f (f^{-1} (y)) = y$
89	83 84 88	elrabd	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to f \in \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}$
90		ssrab2	$⊢ \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq {Base}_{G}$
91	90	a1i	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq {Base}_{G}$
92	15	ad3antrrr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to (x \in {Base}_{G} \leftrightarrow x : A \underset{1-1 onto}{⟶} A)$
93	92	biimpa	$⊢ ((((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \land x \in {Base}_{G}) \to x : A \underset{1-1 onto}{⟶} A$
94	62	ad2antrr	$⊢ ((((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \land x \in {Base}_{G}) \to f^{-1} (y) \in A$
95		f1ocnvfv	$⊢ (x : A \underset{1-1 onto}{⟶} A \land f^{-1} (y) \in A) \to (x (f^{-1} (y)) = y \to x^{-1} (y) = f^{-1} (y))$
96	93 94 95	syl2anc	$⊢ ((((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \land x \in {Base}_{G}) \to (x (f^{-1} (y)) = y \to x^{-1} (y) = f^{-1} (y))$
97		simplrr	$⊢ ((((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \land x \in {Base}_{G}) \to f^{-1} (y) \in t$
98		eleq1	$⊢ x^{-1} (y) = f^{-1} (y) \to (x^{-1} (y) \in t \leftrightarrow f^{-1} (y) \in t)$
99	97 98	syl5ibrcom	$⊢ ((((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \land x \in {Base}_{G}) \to (x^{-1} (y) = f^{-1} (y) \to x^{-1} (y) \in t)$
100	96 99	syld	$⊢ ((((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \land x \in {Base}_{G}) \to (x (f^{-1} (y)) = y \to x^{-1} (y) \in t)$
101	100	ralrimiva	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to \forall x \in {Base}_{G} (x (f^{-1} (y)) = y \to x^{-1} (y) \in t)$
102		fveq1	$⊢ u = x \to u (f^{-1} (y)) = x (f^{-1} (y))$
103	102	eqeq1d	$⊢ u = x \to (u (f^{-1} (y)) = y \leftrightarrow x (f^{-1} (y)) = y)$
104	103	ralrab	$⊢ \forall x \in \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} x^{-1} (y) \in t \leftrightarrow \forall x \in {Base}_{G} (x (f^{-1} (y)) = y \to x^{-1} (y) \in t)$
105	101 104	sylibr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to \forall x \in \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} x^{-1} (y) \in t$
106		ssrab	$⊢ \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq \{x \in {Base}_{G} \| x^{-1} (y) \in t\} \leftrightarrow (\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq {Base}_{G} \land \forall x \in \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} x^{-1} (y) \in t)$
107	91 105 106	sylanbrc	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq \{x \in {Base}_{G} \| x^{-1} (y) \in t\}$
108	39	mptpreima	$⊢ {(x \in {Base}_{G} ⟼ x^{-1} (y))}^{-1} [t] = \{x \in {Base}_{G} \| x^{-1} (y) \in t\}$
109	107 108	sseqtrrdi	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq {(x \in {Base}_{G} ⟼ x^{-1} (y))}^{-1} [t]$
110		funmpt	$⊢ Fun (x \in {Base}_{G} ⟼ x^{-1} (y))$
111		fvex	$⊢ x^{-1} (y) \in V$
112	111 39	dmmpti	$⊢ dom (x \in {Base}_{G} ⟼ x^{-1} (y)) = {Base}_{G}$
113	91 112	sseqtrrdi	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq dom (x \in {Base}_{G} ⟼ x^{-1} (y))$
114		funimass3	$⊢ (Fun (x \in {Base}_{G} ⟼ x^{-1} (y)) \land \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq dom (x \in {Base}_{G} ⟼ x^{-1} (y))) \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) [\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}] \subseteq t \leftrightarrow \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq {(x \in {Base}_{G} ⟼ x^{-1} (y))}^{-1} [t])$
115	110 113 114	sylancr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) [\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}] \subseteq t \leftrightarrow \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \subseteq {(x \in {Base}_{G} ⟼ x^{-1} (y))}^{-1} [t])$
116	109 115	mpbird	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to (x \in {Base}_{G} ⟼ x^{-1} (y)) [\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}] \subseteq t$
117		eleq2	$⊢ v = \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \to (f \in v \leftrightarrow f \in \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\})$
118		imaeq2	$⊢ v = \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \to (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] = (x \in {Base}_{G} ⟼ x^{-1} (y)) [\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}]$
119	118	sseq1d	$⊢ v = \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t \leftrightarrow (x \in {Base}_{G} ⟼ x^{-1} (y)) [\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}] \subseteq t)$
120	117 119	anbi12d	$⊢ v = \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \to ((f \in v \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t) \leftrightarrow (f \in \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}] \subseteq t))$
121	120	rspcev	$⊢ (\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \in TopOpen (G) \land (f \in \{u \in {Base}_{G} \| u (f^{-1} (y)) = y\} \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [\{u \in {Base}_{G} \| u (f^{-1} (y)) = y\}] \subseteq t)) \to \exists v \in TopOpen (G) (f \in v \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t)$
122	81 89 116 121	syl12anc	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land (t \in 𝒫 A \land f^{-1} (y) \in t)) \to \exists v \in TopOpen (G) (f \in v \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t)$
123	122	expr	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land t \in 𝒫 A) \to (f^{-1} (y) \in t \to \exists v \in TopOpen (G) (f \in v \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t))$
124	43 123	sylbid	$⊢ (((A \in V \land y \in A) \land f \in {Base}_{G}) \land t \in 𝒫 A) \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) (f) \in t \to \exists v \in TopOpen (G) (f \in v \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t))$
125	124	ralrimiva	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to \forall t \in 𝒫 A ((x \in {Base}_{G} ⟼ x^{-1} (y)) (f) \in t \to \exists v \in TopOpen (G) (f \in v \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t))$
126	24	ad2antrr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to TopOpen (G) \in TopOn ({Base}_{G})$
127	12	ad2antrr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to 𝒫 A \in TopOn (A)$
128		simpr	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to f \in {Base}_{G}$
129		iscnp	$⊢ (TopOpen (G) \in TopOn ({Base}_{G}) \land 𝒫 A \in TopOn (A) \land f \in {Base}_{G}) \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) CnP 𝒫 A) (f) \leftrightarrow ((x \in {Base}_{G} ⟼ x^{-1} (y)) : {Base}_{G} ⟶ A \land \forall t \in 𝒫 A ((x \in {Base}_{G} ⟼ x^{-1} (y)) (f) \in t \to \exists v \in TopOpen (G) (f \in v \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t))))$
130	126 127 128 129	syl3anc	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) CnP 𝒫 A) (f) \leftrightarrow ((x \in {Base}_{G} ⟼ x^{-1} (y)) : {Base}_{G} ⟶ A \land \forall t \in 𝒫 A ((x \in {Base}_{G} ⟼ x^{-1} (y)) (f) \in t \to \exists v \in TopOpen (G) (f \in v \land (x \in {Base}_{G} ⟼ x^{-1} (y)) [v] \subseteq t))))$
131	36 125 130	mpbir2and	$⊢ ((A \in V \land y \in A) \land f \in {Base}_{G}) \to (x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) CnP 𝒫 A) (f)$
132	131	ralrimiva	$⊢ (A \in V \land y \in A) \to \forall f \in {Base}_{G} (x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) CnP 𝒫 A) (f)$
133		cncnp	$⊢ (TopOpen (G) \in TopOn ({Base}_{G}) \land 𝒫 A \in TopOn (A)) \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) Cn 𝒫 A) \leftrightarrow ((x \in {Base}_{G} ⟼ x^{-1} (y)) : {Base}_{G} ⟶ A \land \forall f \in {Base}_{G} (x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) CnP 𝒫 A) (f)))$
134	24 12 133	syl2anc	$⊢ A \in V \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) Cn 𝒫 A) \leftrightarrow ((x \in {Base}_{G} ⟼ x^{-1} (y)) : {Base}_{G} ⟶ A \land \forall f \in {Base}_{G} (x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) CnP 𝒫 A) (f)))$
135	134	adantr	$⊢ (A \in V \land y \in A) \to ((x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) Cn 𝒫 A) \leftrightarrow ((x \in {Base}_{G} ⟼ x^{-1} (y)) : {Base}_{G} ⟶ A \land \forall f \in {Base}_{G} (x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) CnP 𝒫 A) (f)))$
136	35 132 135	mpbir2and	$⊢ (A \in V \land y \in A) \to (x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) Cn 𝒫 A)$
137		fvconst2g	$⊢ (𝒫 A \in Top \land y \in A) \to (A \times \{𝒫 A\}) (y) = 𝒫 A$
138	26 137	sylan	$⊢ (A \in V \land y \in A) \to (A \times \{𝒫 A\}) (y) = 𝒫 A$
139	138	oveq2d	$⊢ (A \in V \land y \in A) \to TopOpen (G) Cn (A \times \{𝒫 A\}) (y) = TopOpen (G) Cn 𝒫 A$
140	136 139	eleqtrrd	$⊢ (A \in V \land y \in A) \to (x \in {Base}_{G} ⟼ x^{-1} (y)) \in (TopOpen (G) Cn (A \times \{𝒫 A\}) (y))$
141	10 24 25 28 140	ptcn	$⊢ A \in V \to (x \in {Base}_{G} ⟼ (y \in A ⟼ x^{-1} (y))) \in (TopOpen (G) Cn \prod_{𝑡} (A \times \{𝒫 A\}))$
142		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
143	5 142	grpinvf	$⊢ G \in Grp \to {inv}_{g} (G) : {Base}_{G} ⟶ {Base}_{G}$
144	2 143	syl	$⊢ A \in V \to {inv}_{g} (G) : {Base}_{G} ⟶ {Base}_{G}$
145	144	feqmptd	$⊢ A \in V \to {inv}_{g} (G) = (x \in {Base}_{G} ⟼ {inv}_{g} (G) (x))$
146	1 5 142	symginv	$⊢ x \in {Base}_{G} \to {inv}_{g} (G) (x) = x^{-1}$
147	146	adantl	$⊢ (A \in V \land x \in {Base}_{G}) \to {inv}_{g} (G) (x) = x^{-1}$
148	32	feqmptd	$⊢ (A \in V \land x \in {Base}_{G}) \to x^{-1} = (y \in A ⟼ x^{-1} (y))$
149	147 148	eqtrd	$⊢ (A \in V \land x \in {Base}_{G}) \to {inv}_{g} (G) (x) = (y \in A ⟼ x^{-1} (y))$
150	149	mpteq2dva	$⊢ A \in V \to (x \in {Base}_{G} ⟼ {inv}_{g} (G) (x)) = (x \in {Base}_{G} ⟼ (y \in A ⟼ x^{-1} (y)))$
151	145 150	eqtrd	$⊢ A \in V \to {inv}_{g} (G) = (x \in {Base}_{G} ⟼ (y \in A ⟼ x^{-1} (y)))$
152		xkopt	$⊢ (𝒫 A \in Top \land A \in V) \to 𝒫 A^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{𝒫 A\})$
153	26 152	mpancom	$⊢ A \in V \to 𝒫 A^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{𝒫 A\})$
154	153	oveq2d	$⊢ A \in V \to TopOpen (G) Cn (𝒫 A^_{ko} 𝒫 A) = TopOpen (G) Cn \prod_{𝑡} (A \times \{𝒫 A\})$
155	141 151 154	3eltr4d	$⊢ A \in V \to {inv}_{g} (G) \in (TopOpen (G) Cn (𝒫 A^_{ko} 𝒫 A))$
156		eqid	$⊢ 𝒫 A^_{ko} 𝒫 A = 𝒫 A^_{ko} 𝒫 A$
157	156	xkotopon	$⊢ (𝒫 A \in Top \land 𝒫 A \in Top) \to 𝒫 A^_{ko} 𝒫 A \in TopOn (𝒫 A Cn 𝒫 A)$
158	26 26 157	syl2anc	$⊢ A \in V \to 𝒫 A^_{ko} 𝒫 A \in TopOn (𝒫 A Cn 𝒫 A)$
159		frn	$⊢ {inv}_{g} (G) : {Base}_{G} ⟶ {Base}_{G} \to ran {inv}_{g} (G) \subseteq {Base}_{G}$
160	2 143 159	3syl	$⊢ A \in V \to ran {inv}_{g} (G) \subseteq {Base}_{G}$
161		cndis	$⊢ (A \in V \land 𝒫 A \in TopOn (A)) \to 𝒫 A Cn 𝒫 A = A^{A}$
162	12 161	mpdan	$⊢ A \in V \to 𝒫 A Cn 𝒫 A = A^{A}$
163	21 162	sseqtrrd	$⊢ A \in V \to {Base}_{G} \subseteq 𝒫 A Cn 𝒫 A$
164		cnrest2	$⊢ (𝒫 A^_{ko} 𝒫 A \in TopOn (𝒫 A Cn 𝒫 A) \land ran {inv}_{g} (G) \subseteq {Base}_{G} \land {Base}_{G} \subseteq 𝒫 A Cn 𝒫 A) \to ({inv}_{g} (G) \in (TopOpen (G) Cn (𝒫 A^_{ko} 𝒫 A)) \leftrightarrow {inv}_{g} (G) \in (TopOpen (G) Cn ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{G})))$
165	158 160 163 164	syl3anc	$⊢ A \in V \to ({inv}_{g} (G) \in (TopOpen (G) Cn (𝒫 A^_{ko} 𝒫 A)) \leftrightarrow {inv}_{g} (G) \in (TopOpen (G) Cn ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{G})))$
166	155 165	mpbid	$⊢ A \in V \to {inv}_{g} (G) \in (TopOpen (G) Cn ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{G}))$
167	153	oveq1d	$⊢ A \in V \to (𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{G} = \prod_{𝑡} (A \times \{𝒫 A\}) ↾_{𝑡} {Base}_{G}$
168	167 11	eqtrd	$⊢ A \in V \to (𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{G} = TopOpen (G)$
169	168	oveq2d	$⊢ A \in V \to TopOpen (G) Cn ((𝒫 A^_{ko} 𝒫 A) ↾_{𝑡} {Base}_{G}) = TopOpen (G) Cn TopOpen (G)$
170	166 169	eleqtrd	$⊢ A \in V \to {inv}_{g} (G) \in (TopOpen (G) Cn TopOpen (G))$
171		eqid	$⊢ TopOpen (G) = TopOpen (G)$
172	171 142	istgp	$⊢ G \in TopGrp \leftrightarrow (G \in Grp \land G \in TopMnd \land {inv}_{g} (G) \in (TopOpen (G) Cn TopOpen (G)))$
173	2 9 170 172	syl3anbrc	$⊢ A \in V \to G \in TopGrp$

Metamath Proof Explorer

Theorem symgtgp

Proof