Theorem symgtgp 21905

Description: The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015.)

Hypothesis

Ref	Expression
symgtgp.g	⊢ 𝐺 = (SymGrp‘𝐴)

Assertion

Ref	Expression
symgtgp	⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopGrp)

Proof of Theorem symgtgp

Dummy variables 𝑡 𝑓 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		symgtgp.g	. . 3 ⊢ 𝐺 = (SymGrp‘𝐴)
2	1	symggrp 17820	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Grp)
3		grpmnd 17429	. . . 4 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
4	2, 3	syl 17	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd)
5		eqid 2622	. . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺)
6	1, 5	symgtopn 17825	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) = (TopOpen‘𝐺))
7		distopon 20801	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
8		eqid 2622	. . . . . . . 8 ⊢ (∏t‘(𝐴 × {𝒫 𝐴})) = (∏t‘(𝐴 × {𝒫 𝐴}))
9	8	pttoponconst 21400	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚 𝐴)))
10	7, 9	mpdan 702	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚 𝐴)))
11	1, 5	elsymgbas 17802	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴))
12		f1of 6137	. . . . . . . . 9 ⊢ (𝑥:𝐴–1-1-onto→𝐴 → 𝑥:𝐴⟶𝐴)
13		elmapg 7870	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (𝐴 ↑𝑚 𝐴) ↔ 𝑥:𝐴⟶𝐴))
14	13	anidms 677	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝐴 ↑𝑚 𝐴) ↔ 𝑥:𝐴⟶𝐴))
15	12, 14	syl5ibr 236	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (𝑥:𝐴–1-1-onto→𝐴 → 𝑥 ∈ (𝐴 ↑𝑚 𝐴)))
16	11, 15	sylbid 230	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (𝐴 ↑𝑚 𝐴)))
17	16	ssrdv 3609	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ⊆ (𝐴 ↑𝑚 𝐴))
18		resttopon 20965	. . . . . 6 ⊢ (((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚 𝐴)) ∧ (Base‘𝐺) ⊆ (𝐴 ↑𝑚 𝐴)) → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) ∈ (TopOn‘(Base‘𝐺)))
19	10, 17, 18	syl2anc 693	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) ∈ (TopOn‘(Base‘𝐺)))
20	6, 19	eqeltrrd 2702	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)))
21		eqid 2622	. . . . 5 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺)
22	5, 21	istps 20738	. . . 4 ⊢ (𝐺 ∈ TopSp ↔ (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)))
23	20, 22	sylibr 224	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopSp)
24		eqid 2622	. . . . . . . 8 ⊢ (+g‘𝐺) = (+g‘𝐺)
25	1, 5, 24	symgplusg 17809	. . . . . . 7 ⊢ (+g‘𝐺) = (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 ∘ 𝑦))
26		eqid 2622	. . . . . . . 8 ⊢ ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)) = ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))
27		distop 20799	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)
28		eqid 2622	. . . . . . . . . 10 ⊢ (𝒫 𝐴 ^ko 𝒫 𝐴) = (𝒫 𝐴 ^ko 𝒫 𝐴)
29	28	xkotopon 21403	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝒫 𝐴 ∈ Top) → (𝒫 𝐴 ^ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)))
30	27, 27, 29	syl2anc 693	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ^ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)))
31		cndis 21095	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑𝑚 𝐴))
32	7, 31	mpdan 702	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑𝑚 𝐴))
33	17, 32	sseqtr4d 3642	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴))
34		disllycmp 21301	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Locally Comp)
35		llynlly 21280	. . . . . . . . . 10 ⊢ (𝒫 𝐴 ∈ Locally Comp → 𝒫 𝐴 ∈ 𝑛-Locally Comp)
36	34, 35	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ 𝑛-Locally Comp)
37		eqid 2622	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦))
38	37	xkococn 21463	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝒫 𝐴 ∈ 𝑛-Locally Comp ∧ 𝒫 𝐴 ∈ Top) → (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) ∈ (((𝒫 𝐴 ^ko 𝒫 𝐴) ×t (𝒫 𝐴 ^ko 𝒫 𝐴)) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)))
39	27, 36, 27, 38	syl3anc 1326	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) ∈ (((𝒫 𝐴 ^ko 𝒫 𝐴) ×t (𝒫 𝐴 ^ko 𝒫 𝐴)) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)))
40	26, 30, 33, 26, 30, 33, 39	cnmpt2res 21480	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 ∘ 𝑦)) ∈ ((((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)) ×t ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)))
41	25, 40	syl5eqel 2705	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ ((((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)) ×t ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)))
42		xkopt 21458	. . . . . . . . . . 11 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 ^ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝒫 𝐴})))
43	27, 42	mpancom 703	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ^ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝒫 𝐴})))
44	43	oveq1d 6665	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)) = ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)))
45	44, 6	eqtrd 2656	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)) = (TopOpen‘𝐺))
46	45, 45	oveq12d 6668	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)) ×t ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))) = ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)))
47	46	oveq1d 6665	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ((((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)) ×t ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)) = (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)))
48	41, 47	eleqtrd 2703	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)))
49		vex 3203	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
50		vex 3203	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
51	49, 50	coex 7118	. . . . . . . . . . 11 ⊢ (𝑥 ∘ 𝑦) ∈ V
52	25, 51	fnmpt2i 7239	. . . . . . . . . 10 ⊢ (+g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺))
53		eqid 2622	. . . . . . . . . . 11 ⊢ (+𝑓‘𝐺) = (+𝑓‘𝐺)
54	5, 24, 53	plusfeq 17249	. . . . . . . . . 10 ⊢ ((+g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (+𝑓‘𝐺) = (+g‘𝐺))
55	52, 54	ax-mp 5	. . . . . . . . 9 ⊢ (+𝑓‘𝐺) = (+g‘𝐺)
56	55	eqcomi 2631	. . . . . . . 8 ⊢ (+g‘𝐺) = (+𝑓‘𝐺)
57	5, 56	grpplusf 17434	. . . . . . 7 ⊢ (𝐺 ∈ Grp → (+g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
58		frn 6053	. . . . . . 7 ⊢ ((+g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → ran (+g‘𝐺) ⊆ (Base‘𝐺))
59	2, 57, 58	3syl 18	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ran (+g‘𝐺) ⊆ (Base‘𝐺))
60		cnrest2 21090	. . . . . 6 ⊢ (((𝒫 𝐴 ^ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)) ∧ ran (+g‘𝐺) ⊆ (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) → ((+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)) ↔ (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)))))
61	30, 59, 33, 60	syl3anc 1326	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → ((+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)) ↔ (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)))))
62	48, 61	mpbid 222	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))))
63	45	oveq2d 6666	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))) = (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)))
64	62, 63	eleqtrd 2703	. . 3 ⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)))
65	56, 21	istmd 21878	. . 3 ⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))))
66	4, 23, 64, 65	syl3anbrc 1246	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopMnd)
67		id 22	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉)
68		fconst6g 6094	. . . . . . 7 ⊢ (𝒫 𝐴 ∈ Top → (𝐴 × {𝒫 𝐴}):𝐴⟶Top)
69	27, 68	syl 17	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × {𝒫 𝐴}):𝐴⟶Top)
70	11	biimpa 501	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴)
71		f1ocnv 6149	. . . . . . . . . . . 12 ⊢ (𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴–1-1-onto→𝐴)
72		f1of 6137	. . . . . . . . . . . 12 ⊢ (◡𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴⟶𝐴)
73	70, 71, 72	3syl 18	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥:𝐴⟶𝐴)
74	73	ffvelrnda 6359	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑦 ∈ 𝐴) → (◡𝑥‘𝑦) ∈ 𝐴)
75	74	an32s 846	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥‘𝑦) ∈ 𝐴)
76		eqid 2622	. . . . . . . . 9 ⊢ (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) = (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))
77	75, 76	fmptd 6385	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴)
78	77	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴)
79		cnveq 5296	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑓 → ◡𝑥 = ◡𝑓)
80	79	fveq1d 6193	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑓 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦))
81		fvex 6201	. . . . . . . . . . . . . . 15 ⊢ (◡𝑓‘𝑦) ∈ V
82	80, 76, 81	fvmpt 6282	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) = (◡𝑓‘𝑦))
83	82	ad2antlr 763	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) = (◡𝑓‘𝑦))
84	83	eleq1d 2686	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 ↔ (◡𝑓‘𝑦) ∈ 𝑡))
85		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦)))
86	85	mptiniseg 5629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ V → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦})
87	50, 86	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}
88		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) = ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺))
89	10	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚 𝐴)))
90	17	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (Base‘𝐺) ⊆ (𝐴 ↑𝑚 𝐴))
91		toponuni 20719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚 𝐴)) → (𝐴 ↑𝑚 𝐴) = ∪ (∏t‘(𝐴 × {𝒫 𝐴})))
92		mpteq1 4737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ↑𝑚 𝐴) = ∪ (∏t‘(𝐴 × {𝒫 𝐴})) → (𝑢 ∈ (𝐴 ↑𝑚 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))))
93	89, 91, 92	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴 ↑𝑚 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))))
94		simpll 790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝐴 ∈ 𝑉)
95	69	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝐴 × {𝒫 𝐴}):𝐴⟶Top)
96	1, 5	elsymgbas 17802	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∈ 𝑉 → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴–1-1-onto→𝐴))
97	96	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴–1-1-onto→𝐴))
98	97	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓:𝐴–1-1-onto→𝐴)
99		f1ocnv 6149	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:𝐴–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→𝐴)
100		f1of 6137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (◡𝑓:𝐴–1-1-onto→𝐴 → ◡𝑓:𝐴⟶𝐴)
101	98, 99, 100	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ◡𝑓:𝐴⟶𝐴)
102		simplr 792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑦 ∈ 𝐴)
103	101, 102	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝐴)
104		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) = ∪ (∏t‘(𝐴 × {𝒫 𝐴}))
105	104, 8	ptpjcn 21414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝒫 𝐴}):𝐴⟶Top ∧ (◡𝑓‘𝑦) ∈ 𝐴) → (𝑢 ∈ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦))))
106	94, 95, 103, 105	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦))))
107	27	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ Top)
108		fvconst2g 6467	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝒫 𝐴 ∈ Top ∧ (◡𝑓‘𝑦) ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)) = 𝒫 𝐴)
109	107, 103, 108	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)) = 𝒫 𝐴)
110	109	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦))) = ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴))
111	106, 110	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴))
112	93, 111	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴 ↑𝑚 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴))
113	88, 89, 90, 112	cnmpt1res 21479	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) Cn 𝒫 𝐴))
114	6	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ 𝑉 → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) Cn 𝒫 𝐴) = ((TopOpen‘𝐺) Cn 𝒫 𝐴))
115	114	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) Cn 𝒫 𝐴) = ((TopOpen‘𝐺) Cn 𝒫 𝐴))
116	113, 115	eleqtrd 2703	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴))
117		snelpwi 4912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴)
118	117	ad2antlr 763	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑦} ∈ 𝒫 𝐴)
119		cnima 21069	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ∧ {𝑦} ∈ 𝒫 𝐴) → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺))
120	116, 118, 119	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺))
121	87, 120	syl5eqelr 2706	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺))
122	121	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺))
123		simplr 792	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓 ∈ (Base‘𝐺))
124	98	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓:𝐴–1-1-onto→𝐴)
125		simpllr 799	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑦 ∈ 𝐴)
126		f1ocnvfv2 6533	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:𝐴–1-1-onto→𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑓‘(◡𝑓‘𝑦)) = 𝑦)
127	124, 125, 126	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (𝑓‘(◡𝑓‘𝑦)) = 𝑦)
128		fveq1 6190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑓 → (𝑢‘(◡𝑓‘𝑦)) = (𝑓‘(◡𝑓‘𝑦)))
129	128	eqeq1d 2624	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑓 → ((𝑢‘(◡𝑓‘𝑦)) = 𝑦 ↔ (𝑓‘(◡𝑓‘𝑦)) = 𝑦))
130	129	elrab 3363	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ↔ (𝑓 ∈ (Base‘𝐺) ∧ (𝑓‘(◡𝑓‘𝑦)) = 𝑦))
131	123, 127, 130	sylanbrc 698	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦})
132		ssrab2 3687	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺)
133	132	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺))
134	11	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴))
135	134	biimpa 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴)
136	103	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝐴)
137		f1ocnvfv 6534	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥:𝐴–1-1-onto→𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝐴) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦)))
138	135, 136, 137	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦)))
139		simplrr 801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝑡)
140		eleq1 2689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡𝑥‘𝑦) = (◡𝑓‘𝑦) → ((◡𝑥‘𝑦) ∈ 𝑡 ↔ (◡𝑓‘𝑦) ∈ 𝑡))
141	139, 140	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((◡𝑥‘𝑦) = (◡𝑓‘𝑦) → (◡𝑥‘𝑦) ∈ 𝑡))
142	138, 141	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡))
143	142	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡))
144		fveq1 6190	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑢‘(◡𝑓‘𝑦)) = (𝑥‘(◡𝑓‘𝑦)))
145	144	eqeq1d 2624	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → ((𝑢‘(◡𝑓‘𝑦)) = 𝑦 ↔ (𝑥‘(◡𝑓‘𝑦)) = 𝑦))
146	145	ralrab 3368	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡))
147	143, 146	sylibr 224	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡)
148		ssrab 3680	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡} ↔ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺) ∧ ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡))
149	133, 147, 148	sylanbrc 698	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡})
150	76	mptpreima 5628	. . . . . . . . . . . . . . . 16 ⊢ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡) = {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡}
151	149, 150	syl6sseqr 3652	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡))
152		funmpt 5926	. . . . . . . . . . . . . . . 16 ⊢ Fun (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))
153		fvex 6201	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑥‘𝑦) ∈ V
154	153, 76	dmmpti 6023	. . . . . . . . . . . . . . . . 17 ⊢ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) = (Base‘𝐺)
155	133, 154	syl6sseqr 3652	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)))
156		funimass3 6333	. . . . . . . . . . . . . . . 16 ⊢ ((Fun (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∧ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡)))
157	152, 155, 156	sylancr 695	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡)))
158	151, 157	mpbird 247	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)
159		eleq2 2690	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → (𝑓 ∈ 𝑣 ↔ 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}))
160		imaeq2 5462	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) = ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}))
161	160	sseq1d 3632	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡 ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡))
162	159, 161	anbi12d 747	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → ((𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡) ↔ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)))
163	162	rspcev 3309	. . . . . . . . . . . . . 14 ⊢ (({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺) ∧ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))
164	122, 131, 158, 163	syl12anc 1324	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))
165	164	expr 643	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((◡𝑓‘𝑦) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)))
166	84, 165	sylbid 230	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)))
167	166	ralrimiva 2966	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)))
168	20	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)))
169	7	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ (TopOn‘𝐴))
170		simpr 477	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓 ∈ (Base‘𝐺))
171		iscnp 21041	. . . . . . . . . . 11 ⊢ (((TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)))))
172	168, 169, 170, 171	syl3anc 1326	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)))))
173	78, 167, 172	mpbir2and 957	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))
174	173	ralrimiva 2966	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))
175		cncnp 21084	. . . . . . . . . 10 ⊢ (((TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))))
176	20, 7, 175	syl2anc 693	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))))
177	176	adantr 481	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))))
178	77, 174, 177	mpbir2and 957	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴))
179		fvconst2g 6467	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴)
180	27, 179	sylan 488	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴)
181	180	oveq2d 6666	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦)) = ((TopOpen‘𝐺) Cn 𝒫 𝐴))
182	178, 181	eleqtrrd 2704	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦)))
183	8, 20, 67, 69, 182	ptcn 21430	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) ∈ ((TopOpen‘𝐺) Cn (∏t‘(𝐴 × {𝒫 𝐴}))))
184		eqid 2622	. . . . . . . . 9 ⊢ (invg‘𝐺) = (invg‘𝐺)
185	5, 184	grpinvf 17466	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → (invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺))
186	2, 185	syl 17	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺))
187	186	feqmptd 6249	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)))
188	1, 5, 184	symginv 17822	. . . . . . . . 9 ⊢ (𝑥 ∈ (Base‘𝐺) → ((invg‘𝐺)‘𝑥) = ◡𝑥)
189	188	adantl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = ◡𝑥)
190	73	feqmptd 6249	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥 = (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦)))
191	189, 190	eqtrd 2656	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦)))
192	191	mpteq2dva 4744	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))))
193	187, 192	eqtrd 2656	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))))
194	43	oveq2d 6666	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → ((TopOpen‘𝐺) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)) = ((TopOpen‘𝐺) Cn (∏t‘(𝐴 × {𝒫 𝐴}))))
195	183, 193, 194	3eltr4d 2716	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)))
196		frn 6053	. . . . . 6 ⊢ ((invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺) → ran (invg‘𝐺) ⊆ (Base‘𝐺))
197	2, 185, 196	3syl 18	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → ran (invg‘𝐺) ⊆ (Base‘𝐺))
198		cnrest2 21090	. . . . 5 ⊢ (((𝒫 𝐴 ^ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)) ∧ ran (invg‘𝐺) ⊆ (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) → ((invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)) ↔ (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)))))
199	30, 197, 33, 198	syl3anc 1326	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ((invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)) ↔ (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺)))))
200	195, 199	mpbid 222	. . 3 ⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))))
201	45	oveq2d 6666	. . 3 ⊢ (𝐴 ∈ 𝑉 → ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t (Base‘𝐺))) = ((TopOpen‘𝐺) Cn (TopOpen‘𝐺)))
202	200, 201	eleqtrd 2703	. 2 ⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺)))
203	21, 184	istgp 21881	. 2 ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))))
204	2, 66, 202, 203	syl3anbrc 1246	1 ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopGrp)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ⊆ wss 3574  𝒫 cpw 4158  {csn 4177  ∪ cuni 4436   ↦ cmpt 4729   × cxp 5112  ^◡ccnv 5113  dom cdm 5114  ran crn 5115   “ cima 5117   ∘ ccom 5118  Fun wfun 5882   Fn wfn 5883  ⟶wf 5884  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ↦ cmpt2 6652   ↑_𝑚 cmap 7857  Basecbs 15857  +_gcplusg 15941   ↾_t crest 16081  TopOpenctopn 16082  ∏_tcpt 16099  +_𝑓cplusf 17239  Mndcmnd 17294  Grpcgrp 17422  inv_gcminusg 17423  SymGrpcsymg 17797  Topctop 20698  TopOnctopon 20715  TopSpctps 20736   Cn ccn 21028   CnP ccnp 21029  Compccmp 21189  Locally clly 21267  𝑛-Locally cnlly 21268   ×_t ctx 21363   ^_ko cxko 21364  TopMndctmd 21874  TopGrpctgp 21875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-plusg 15954  df-tset 15960  df-rest 16083  df-topn 16084  df-0g 16102  df-topgen 16104  df-pt 16105  df-plusf 17241  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-minusg 17426  df-symg 17798  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-ntr 20824  df-nei 20902  df-cn 21031  df-cnp 21032  df-cmp 21190  df-lly 21269  df-nlly 21270  df-tx 21365  df-xko 21366  df-tmd 21876  df-tgp 21877

This theorem is referenced by: (None)