Metamath Proof Explorer


Theorem qtopval

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis qtopval.1 X = J
Assertion qtopval J V F W J qTop F = s 𝒫 F X | F -1 s X J

Proof

Step Hyp Ref Expression
1 qtopval.1 X = J
2 elex J V J V
3 elex F W F V
4 imaexg F V F X V
5 pwexg F X V 𝒫 F X V
6 rabexg 𝒫 F X V s 𝒫 F X | F -1 s X J V
7 4 5 6 3syl F V s 𝒫 F X | F -1 s X J V
8 7 adantl J V F V s 𝒫 F X | F -1 s X J V
9 simpr j = J f = F f = F
10 simpl j = J f = F j = J
11 10 unieqd j = J f = F j = J
12 11 1 syl6eqr j = J f = F j = X
13 9 12 imaeq12d j = J f = F f j = F X
14 13 pweqd j = J f = F 𝒫 f j = 𝒫 F X
15 9 cnveqd j = J f = F f -1 = F -1
16 15 imaeq1d j = J f = F f -1 s = F -1 s
17 16 12 ineq12d j = J f = F f -1 s j = F -1 s X
18 17 10 eleq12d j = J f = F f -1 s j j F -1 s X J
19 14 18 rabeqbidv j = J f = F s 𝒫 f j | f -1 s j j = s 𝒫 F X | F -1 s X J
20 df-qtop qTop = j V , f V s 𝒫 f j | f -1 s j j
21 19 20 ovmpoga J V F V s 𝒫 F X | F -1 s X J V J qTop F = s 𝒫 F X | F -1 s X J
22 8 21 mpd3an3 J V F V J qTop F = s 𝒫 F X | F -1 s X J
23 2 3 22 syl2an J V F W J qTop F = s 𝒫 F X | F -1 s X J