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 bitrid ⊢ ( 𝑥 = 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 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐵 )