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 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
Assertion ptval ( ( 𝐴𝑉𝐹 Fn 𝐴 ) → ( ∏t𝐹 ) = ( topGen ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ptval.1 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
2 df-pt t = ( 𝑓 ∈ V ↦ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ) } ) )
3 simpr ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
4 3 dmeqd ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = dom 𝐹 )
5 fndm ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6 5 ad2antlr ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝐹 = 𝐴 )
7 4 6 eqtrd ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = 𝐴 )
8 7 fneq2d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑔 Fn dom 𝑓𝑔 Fn 𝐴 ) )
9 3 fveq1d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑓𝑦 ) = ( 𝐹𝑦 ) )
10 9 eleq2d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ↔ ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ) )
11 7 10 raleqbidv ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ↔ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ) )
12 7 difeq1d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( dom 𝑓𝑧 ) = ( 𝐴𝑧 ) )
13 9 unieqd ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑓𝑦 ) = ( 𝐹𝑦 ) )
14 13 eqeq2d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ↔ ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) )
15 12 14 raleqbidv ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) )
16 15 rexbidv ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ↔ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) )
17 8 11 16 3anbi123d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ) ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ) )
18 7 ixpeq1d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → X 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) = X 𝑦𝐴 ( 𝑔𝑦 ) )
19 18 eqeq2d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ↔ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) )
20 17 19 anbi12d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ) ↔ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) ) )
21 20 exbidv ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) ) )
22 21 abbidv ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } )
23 22 1 eqtr4di ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ) } = 𝐵 )
24 23 fveq2d ( ( ( 𝐴𝑉𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓𝑧 ) ( 𝑔𝑦 ) = ( 𝑓𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔𝑦 ) ) } ) = ( topGen ‘ 𝐵 ) )
25 fnex ( ( 𝐹 Fn 𝐴𝐴𝑉 ) → 𝐹 ∈ V )
26 25 ancoms ( ( 𝐴𝑉𝐹 Fn 𝐴 ) → 𝐹 ∈ V )
27 fvexd ( ( 𝐴𝑉𝐹 Fn 𝐴 ) → ( topGen ‘ 𝐵 ) ∈ V )
28 2 24 26 27 fvmptd2 ( ( 𝐴𝑉𝐹 Fn 𝐴 ) → ( ∏t𝐹 ) = ( topGen ‘ 𝐵 ) )