Metamath Proof Explorer

Theorem 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 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion symgtgp ( 𝐴 ∈ 𝑉 → 𝐺 ∈ TopGrp )

Proof

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