Metamath Proof Explorer


Theorem ptval2

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

Ref Expression
Hypotheses ptval2.1 𝐽 = ( ∏t𝐹 )
ptval2.2 𝑋 = 𝐽
ptval2.3 𝐺 = ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) )
Assertion ptval2 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → 𝐽 = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ran 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 ptval2.1 𝐽 = ( ∏t𝐹 )
2 ptval2.2 𝑋 = 𝐽
3 ptval2.3 𝐺 = ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) )
4 ffn ( 𝐹 : 𝐴 ⟶ Top → 𝐹 Fn 𝐴 )
5 eqid { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
6 5 ptval ( ( 𝐴𝑉𝐹 Fn 𝐴 ) → ( ∏t𝐹 ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
7 1 6 eqtrid ( ( 𝐴𝑉𝐹 Fn 𝐴 ) → 𝐽 = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
8 4 7 sylan2 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → 𝐽 = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
9 eqid X 𝑛𝐴 ( 𝐹𝑛 ) = X 𝑛𝐴 ( 𝐹𝑛 )
10 5 9 ptbasfi ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } = ( fi ‘ ( { X 𝑛𝐴 ( 𝐹𝑛 ) } ∪ ran ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ) ) ) )
11 1 ptuni ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑛𝐴 ( 𝐹𝑛 ) = 𝐽 )
12 11 2 eqtr4di ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑛𝐴 ( 𝐹𝑛 ) = 𝑋 )
13 12 sneqd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → { X 𝑛𝐴 ( 𝐹𝑛 ) } = { 𝑋 } )
14 12 3ad2ant1 ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ 𝑘𝐴𝑢 ∈ ( 𝐹𝑘 ) ) → X 𝑛𝐴 ( 𝐹𝑛 ) = 𝑋 )
15 14 mpteq1d ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ 𝑘𝐴𝑢 ∈ ( 𝐹𝑘 ) ) → ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) = ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) )
16 15 cnveqd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ 𝑘𝐴𝑢 ∈ ( 𝐹𝑘 ) ) → ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) = ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) )
17 16 imaeq1d ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ 𝑘𝐴𝑢 ∈ ( 𝐹𝑘 ) ) → ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) = ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) )
18 17 mpoeq3dva ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ) = ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ) )
19 18 3 eqtr4di ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ) = 𝐺 )
20 19 rneqd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ran ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ) = ran 𝐺 )
21 13 20 uneq12d ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( { X 𝑛𝐴 ( 𝐹𝑛 ) } ∪ ran ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ) ) = ( { 𝑋 } ∪ ran 𝐺 ) )
22 21 fveq2d ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( fi ‘ ( { X 𝑛𝐴 ( 𝐹𝑛 ) } ∪ ran ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ) ) ) = ( fi ‘ ( { 𝑋 } ∪ ran 𝐺 ) ) )
23 10 22 eqtrd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } = ( fi ‘ ( { 𝑋 } ∪ ran 𝐺 ) ) )
24 23 fveq2d ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ran 𝐺 ) ) ) )
25 8 24 eqtrd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → 𝐽 = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ran 𝐺 ) ) ) )