# Metamath Proof Explorer

## Theorem ptuni2

Description: The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptbas.1 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
Assertion ptuni2 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑘𝐴 ( 𝐹𝑘 ) = 𝐵 )

### Proof

Step Hyp Ref Expression
1 ptbas.1 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
2 1 ptbasid ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑘𝐴 ( 𝐹𝑘 ) ∈ 𝐵 )
3 elssuni ( X 𝑘𝐴 ( 𝐹𝑘 ) ∈ 𝐵X 𝑘𝐴 ( 𝐹𝑘 ) ⊆ 𝐵 )
4 2 3 syl ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑘𝐴 ( 𝐹𝑘 ) ⊆ 𝐵 )
5 simpr2 ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ) → ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) )
6 elssuni ( ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) → ( 𝑔𝑦 ) ⊆ ( 𝐹𝑦 ) )
7 6 ralimi ( ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) → ∀ 𝑦𝐴 ( 𝑔𝑦 ) ⊆ ( 𝐹𝑦 ) )
8 ss2ixp ( ∀ 𝑦𝐴 ( 𝑔𝑦 ) ⊆ ( 𝐹𝑦 ) → X 𝑦𝐴 ( 𝑔𝑦 ) ⊆ X 𝑦𝐴 ( 𝐹𝑦 ) )
9 5 7 8 3syl ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ) → X 𝑦𝐴 ( 𝑔𝑦 ) ⊆ X 𝑦𝐴 ( 𝐹𝑦 ) )
10 fveq2 ( 𝑦 = 𝑘 → ( 𝐹𝑦 ) = ( 𝐹𝑘 ) )
11 10 unieqd ( 𝑦 = 𝑘 ( 𝐹𝑦 ) = ( 𝐹𝑘 ) )
12 11 cbvixpv X 𝑦𝐴 ( 𝐹𝑦 ) = X 𝑘𝐴 ( 𝐹𝑘 )
13 9 12 sseqtrdi ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ) → X 𝑦𝐴 ( 𝑔𝑦 ) ⊆ X 𝑘𝐴 ( 𝐹𝑘 ) )
14 velpw ( 𝑥 ∈ 𝒫 X 𝑘𝐴 ( 𝐹𝑘 ) ↔ 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) )
15 sseq1 ( 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) → ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↔ X 𝑦𝐴 ( 𝑔𝑦 ) ⊆ X 𝑘𝐴 ( 𝐹𝑘 ) ) )
16 14 15 syl5bb ( 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) → ( 𝑥 ∈ 𝒫 X 𝑘𝐴 ( 𝐹𝑘 ) ↔ X 𝑦𝐴 ( 𝑔𝑦 ) ⊆ X 𝑘𝐴 ( 𝐹𝑘 ) ) )
17 13 16 syl5ibrcom ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ) → ( 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) → 𝑥 ∈ 𝒫 X 𝑘𝐴 ( 𝐹𝑘 ) ) )
18 17 expimpd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) → 𝑥 ∈ 𝒫 X 𝑘𝐴 ( 𝐹𝑘 ) ) )
19 18 exlimdv ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) → 𝑥 ∈ 𝒫 X 𝑘𝐴 ( 𝐹𝑘 ) ) )
20 19 abssdv ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ⊆ 𝒫 X 𝑘𝐴 ( 𝐹𝑘 ) )
21 1 20 eqsstrid ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → 𝐵 ⊆ 𝒫 X 𝑘𝐴 ( 𝐹𝑘 ) )
22 sspwuni ( 𝐵 ⊆ 𝒫 X 𝑘𝐴 ( 𝐹𝑘 ) ↔ 𝐵X 𝑘𝐴 ( 𝐹𝑘 ) )
23 21 22 sylib ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → 𝐵X 𝑘𝐴 ( 𝐹𝑘 ) )
24 4 23 eqssd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑘𝐴 ( 𝐹𝑘 ) = 𝐵 )