Metamath Proof Explorer


Theorem ptval

Description: The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptval.1 B = x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
Assertion ptval A V F Fn A 𝑡 F = topGen B

Proof

Step Hyp Ref Expression
1 ptval.1 B = x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
2 df-pt 𝑡 = f V topGen x | g g Fn dom f y dom f g y f y z Fin y dom f z g y = f y x = y dom f g y
3 simpr A V F Fn A f = F f = F
4 3 dmeqd A V F Fn A f = F dom f = dom F
5 fndm F Fn A dom F = A
6 5 ad2antlr A V F Fn A f = F dom F = A
7 4 6 eqtrd A V F Fn A f = F dom f = A
8 7 fneq2d A V F Fn A f = F g Fn dom f g Fn A
9 3 fveq1d A V F Fn A f = F f y = F y
10 9 eleq2d A V F Fn A f = F g y f y g y F y
11 7 10 raleqbidv A V F Fn A f = F y dom f g y f y y A g y F y
12 7 difeq1d A V F Fn A f = F dom f z = A z
13 9 unieqd A V F Fn A f = F f y = F y
14 13 eqeq2d A V F Fn A f = F g y = f y g y = F y
15 12 14 raleqbidv A V F Fn A f = F y dom f z g y = f y y A z g y = F y
16 15 rexbidv A V F Fn A f = F z Fin y dom f z g y = f y z Fin y A z g y = F y
17 8 11 16 3anbi123d A V F Fn A f = F g Fn dom f y dom f g y f y z Fin y dom f z g y = f y g Fn A y A g y F y z Fin y A z g y = F y
18 7 ixpeq1d A V F Fn A f = F y dom f g y = y A g y
19 18 eqeq2d A V F Fn A f = F x = y dom f g y x = y A g y
20 17 19 anbi12d A V F Fn A f = F g Fn dom f y dom f g y f y z Fin y dom f z g y = f y x = y dom f g y g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
21 20 exbidv A V F Fn A f = F g g Fn dom f y dom f g y f y z Fin y dom f z g y = f y x = y dom f g y g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
22 21 abbidv A V F Fn A f = F x | g g Fn dom f y dom f g y f y z Fin y dom f z g y = f y x = y dom f g y = x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
23 22 1 eqtr4di A V F Fn A f = F x | g g Fn dom f y dom f g y f y z Fin y dom f z g y = f y x = y dom f g y = B
24 23 fveq2d A V F Fn A f = F topGen x | g g Fn dom f y dom f g y f y z Fin y dom f z g y = f y x = y dom f g y = topGen B
25 fnex F Fn A A V F V
26 25 ancoms A V F Fn A F V
27 fvexd A V F Fn A topGen B V
28 2 24 26 27 fvmptd2 A V F Fn A 𝑡 F = topGen B