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

Metamath Proof Explorer

Theorem ptbasin2

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 ptbas.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
2 1 ptbasin ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝐵 )
3 2 ralrimivva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ∩ 𝑣 ) ∈ 𝐵 )
4 1 ptuni2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐵 )
5 ixpexg ⊢ ( ∀ 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ V → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ V )
6 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
7 6 uniex ⊢ ∪ ( 𝐹 ‘ 𝑘 ) ∈ V
8 7 a1i ⊢ ( 𝑘 ∈ 𝐴 → ∪ ( 𝐹 ‘ 𝑘 ) ∈ V )
9 5 8 mprg ⊢ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ V
10 4 9 eqeltrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ∪ 𝐵 ∈ V )
11 uniexb ⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V )
12 10 11 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → 𝐵 ∈ V )
13 inficl ⊢ ( 𝐵 ∈ V → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ∩ 𝑣 ) ∈ 𝐵 ↔ ( fi ‘ 𝐵 ) = 𝐵 ) )
14 12 13 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ( 𝑢 ∩ 𝑣 ) ∈ 𝐵 ↔ ( fi ‘ 𝐵 ) = 𝐵 ) )
15 3 14 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( fi ‘ 𝐵 ) = 𝐵 )