Metamath Proof Explorer

Theorem prdstopn

Description: Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses prdstopn.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdstopn.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdstopn.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdstopn.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
prdstopn.o ⊢ 𝑂 = ( TopOpen ‘ 𝑌 )
Assertion prdstopn ( 𝜑 → 𝑂 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 prdstopn.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdstopn.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3 prdstopn.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4 prdstopn.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
5 prdstopn.o ⊢ 𝑂 = ( TopOpen ‘ 𝑌 )
6 fnex ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
7 4 3 6 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ V )
8 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
9 eqidd ⊢ ( 𝜑 → dom 𝑅 = dom 𝑅 )
10 eqid ⊢ ( TopSet ‘ 𝑌 ) = ( TopSet ‘ 𝑌 )
11 1 2 7 8 9 10 prdstset ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
12 topnfn ⊢ TopOpen Fn V
13 dffn2 ⊢ ( 𝑅 Fn 𝐼 ↔ 𝑅 : 𝐼 ⟶ V )
14 4 13 sylib ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ V )
15 fnfco ⊢ ( ( TopOpen Fn V ∧ 𝑅 : 𝐼 ⟶ V ) → ( TopOpen ∘ 𝑅 ) Fn 𝐼 )
16 12 14 15 sylancr ⊢ ( 𝜑 → ( TopOpen ∘ 𝑅 ) Fn 𝐼 )
17 eqid ⊢ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) }
18 17 ptval ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( TopOpen ∘ 𝑅 ) Fn 𝐼 ) → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ) )
19 3 16 18 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ) )
20 19 unieqd ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ∪ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ) )
21 fvco2 ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝑦 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑦 ) ) )
22 4 21 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑦 ) ) )
23 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑦 ) )
24 eqid ⊢ ( TopSet ‘ ( 𝑅 ‘ 𝑦 ) ) = ( TopSet ‘ ( 𝑅 ‘ 𝑦 ) )
25 23 24 topnval ⊢ ( ( TopSet ‘ ( 𝑅 ‘ 𝑦 ) ) ↾t ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑦 ) )
26 restsspw ⊢ ( ( TopSet ‘ ( 𝑅 ‘ 𝑦 ) ) ↾t ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ⊆ 𝒫 ( Base ‘ ( 𝑅 ‘ 𝑦 ) )
27 25 26 eqsstrri ⊢ ( TopOpen ‘ ( 𝑅 ‘ 𝑦 ) ) ⊆ 𝒫 ( Base ‘ ( 𝑅 ‘ 𝑦 ) )
28 22 27 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ⊆ 𝒫 ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
29 28 sseld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝒫 ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
30 fvex ⊢ ( 𝑔 ‘ 𝑦 ) ∈ V
31 30 elpw ⊢ ( ( 𝑔 ‘ 𝑦 ) ∈ 𝒫 ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ↔ ( 𝑔 ‘ 𝑦 ) ⊆ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
32 29 31 imbitrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) → ( 𝑔 ‘ 𝑦 ) ⊆ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
33 32 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) → ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ⊆ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
34 simpl2 ⊢ ( ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) )
35 33 34 impel ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ⊆ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
36 ss2ixp ⊢ ( ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ⊆ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) → X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ⊆ X 𝑦 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) ) → X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ⊆ X 𝑦 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
38 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) ) → 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) )
39 1 8 2 3 4 prdsbas2 ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = X 𝑦 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) ) → ( Base ‘ 𝑌 ) = X 𝑦 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
41 37 38 40 3sstr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) ) → 𝑥 ⊆ ( Base ‘ 𝑌 ) )
42 41 ex ⊢ ( 𝜑 → ( ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) → 𝑥 ⊆ ( Base ‘ 𝑌 ) ) )
43 42 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) → 𝑥 ⊆ ( Base ‘ 𝑌 ) ) )
44 velpw ⊢ ( 𝑥 ∈ 𝒫 ( Base ‘ 𝑌 ) ↔ 𝑥 ⊆ ( Base ‘ 𝑌 ) )
45 43 44 imbitrrdi ⊢ ( 𝜑 → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) → 𝑥 ∈ 𝒫 ( Base ‘ 𝑌 ) ) )
46 45 abssdv ⊢ ( 𝜑 → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ⊆ 𝒫 ( Base ‘ 𝑌 ) )
47 fvex ⊢ ( Base ‘ 𝑌 ) ∈ V
48 47 pwex ⊢ 𝒫 ( Base ‘ 𝑌 ) ∈ V
49 48 ssex ⊢ ( { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ⊆ 𝒫 ( Base ‘ 𝑌 ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ∈ V )
50 unitg ⊢ ( { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ∈ V → ∪ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ) = ∪ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } )
51 46 49 50 3syl ⊢ ( 𝜑 → ∪ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ) = ∪ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } )
52 20 51 eqtrd ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ∪ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } )
53 sspwuni ⊢ ( { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ⊆ 𝒫 ( Base ‘ 𝑌 ) ↔ ∪ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ⊆ ( Base ‘ 𝑌 ) )
54 46 53 sylib ⊢ ( 𝜑 → ∪ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐼 ( 𝑔 ‘ 𝑦 ) ) } ⊆ ( Base ‘ 𝑌 ) )
55 52 54 eqsstrd ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⊆ ( Base ‘ 𝑌 ) )
56 sspwuni ⊢ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⊆ 𝒫 ( Base ‘ 𝑌 ) ↔ ∪ ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⊆ ( Base ‘ 𝑌 ) )
57 55 56 sylibr ⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⊆ 𝒫 ( Base ‘ 𝑌 ) )
58 11 57 eqsstrd ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) ⊆ 𝒫 ( Base ‘ 𝑌 ) )
59 8 10 topnid ⊢ ( ( TopSet ‘ 𝑌 ) ⊆ 𝒫 ( Base ‘ 𝑌 ) → ( TopSet ‘ 𝑌 ) = ( TopOpen ‘ 𝑌 ) )
60 58 59 syl ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) = ( TopOpen ‘ 𝑌 ) )
61 60 5 eqtr4di ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) = 𝑂 )
62 61 11 eqtr3d ⊢ ( 𝜑 → 𝑂 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )