This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐵 ) )