Metamath Proof Explorer

Definition df-pt

Description: Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Assertion df-pt ∏t = ( 𝑓 ∈ V ↦ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpt ⊢ ∏t
1 vf ⊢ 𝑓
2 cvv ⊢ V
3 ctg ⊢ topGen
4 vx ⊢ 𝑥
5 vg ⊢ 𝑔
6 5 cv ⊢ 𝑔
7 1 cv ⊢ 𝑓
8 7 cdm ⊢ dom 𝑓
9 6 8 wfn ⊢ 𝑔 Fn dom 𝑓
10 vy ⊢ 𝑦
11 10 cv ⊢ 𝑦
12 11 6 cfv ⊢ ( 𝑔 ‘ 𝑦 )
13 11 7 cfv ⊢ ( 𝑓 ‘ 𝑦 )
14 12 13 wcel ⊢ ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 )
15 14 10 8 wral ⊢ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 )
16 vz ⊢ 𝑧
17 cfn ⊢ Fin
18 16 cv ⊢ 𝑧
19 8 18 cdif ⊢ ( dom 𝑓 ∖ 𝑧 )
20 13 cuni ⊢ ∪ ( 𝑓 ‘ 𝑦 )
21 12 20 wceq ⊢ ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 )
22 21 10 19 wral ⊢ ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 )
23 22 16 17 wrex ⊢ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 )
24 9 15 23 w3a ⊢ ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) )
25 4 cv ⊢ 𝑥
26 10 8 12 cixp ⊢ X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 )
27 25 26 wceq ⊢ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 )
28 24 27 wa ⊢ ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) )
29 28 5 wex ⊢ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) )
30 29 4 cab ⊢ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) }
31 30 3 cfv ⊢ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } )
32 1 2 31 cmpt ⊢ ( 𝑓 ∈ V ↦ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } ) )
33 0 32 wceq ⊢ ∏t = ( 𝑓 ∈ V ↦ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } ) )