Step | Hyp | Ref
| Expression |
1 | | elin 3930 |
. . 3
β’ (πΊ β (Grp β© TopMnd)
β (πΊ β Grp β§
πΊ β
TopMnd)) |
2 | 1 | anbi1i 625 |
. 2
β’ ((πΊ β (Grp β© TopMnd) β§
πΌ β (π½ Cn π½)) β ((πΊ β Grp β§ πΊ β TopMnd) β§ πΌ β (π½ Cn π½))) |
3 | | fvexd 6861 |
. . . 4
β’ (π = πΊ β (TopOpenβπ) β V) |
4 | | simpl 484 |
. . . . . . 7
β’ ((π = πΊ β§ π = (TopOpenβπ)) β π = πΊ) |
5 | 4 | fveq2d 6850 |
. . . . . 6
β’ ((π = πΊ β§ π = (TopOpenβπ)) β (invgβπ) = (invgβπΊ)) |
6 | | istgp.2 |
. . . . . 6
β’ πΌ = (invgβπΊ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . 5
β’ ((π = πΊ β§ π = (TopOpenβπ)) β (invgβπ) = πΌ) |
8 | | id 22 |
. . . . . . 7
β’ (π = (TopOpenβπ) β π = (TopOpenβπ)) |
9 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΊ β (TopOpenβπ) = (TopOpenβπΊ)) |
10 | | istgp.1 |
. . . . . . . 8
β’ π½ = (TopOpenβπΊ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΊ β (TopOpenβπ) = π½) |
12 | 8, 11 | sylan9eqr 2795 |
. . . . . 6
β’ ((π = πΊ β§ π = (TopOpenβπ)) β π = π½) |
13 | 12, 12 | oveq12d 7379 |
. . . . 5
β’ ((π = πΊ β§ π = (TopOpenβπ)) β (π Cn π) = (π½ Cn π½)) |
14 | 7, 13 | eleq12d 2828 |
. . . 4
β’ ((π = πΊ β§ π = (TopOpenβπ)) β ((invgβπ) β (π Cn π) β πΌ β (π½ Cn π½))) |
15 | 3, 14 | sbcied 3788 |
. . 3
β’ (π = πΊ β ([(TopOpenβπ) / π](invgβπ) β (π Cn π) β πΌ β (π½ Cn π½))) |
16 | | df-tgp 23447 |
. . 3
β’ TopGrp =
{π β (Grp β©
TopMnd) β£ [(TopOpenβπ) / π](invgβπ) β (π Cn π)} |
17 | 15, 16 | elrab2 3652 |
. 2
β’ (πΊ β TopGrp β (πΊ β (Grp β© TopMnd) β§
πΌ β (π½ Cn π½))) |
18 | | df-3an 1090 |
. 2
β’ ((πΊ β Grp β§ πΊ β TopMnd β§ πΌ β (π½ Cn π½)) β ((πΊ β Grp β§ πΊ β TopMnd) β§ πΌ β (π½ Cn π½))) |
19 | 2, 17, 18 | 3bitr4i 303 |
1
β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopMnd β§ πΌ β (π½ Cn π½))) |