Metamath Proof Explorer

Theorem xkouni

Description: The base set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypothesis xkouni.1 ⊢ 𝐽 = ( 𝑆 ↑ko 𝑅 )
Assertion xkouni ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) = ∪ 𝐽 )

Proof

Step Hyp Ref Expression
1 xkouni.1 ⊢ 𝐽 = ( 𝑆 ↑ko 𝑅 )
2 ima0 ⊢ ( 𝑓 “ ∅ ) = ∅
3 0ss ⊢ ∅ ⊆ ∪ 𝑆
4 2 3 eqsstri ⊢ ( 𝑓 “ ∅ ) ⊆ ∪ 𝑆
5 4 a1i ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑓 “ ∅ ) ⊆ ∪ 𝑆 )
6 5 ralrimiva ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∀ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ( 𝑓 “ ∅ ) ⊆ ∪ 𝑆 )
7 rabid2 ⊢ ( ( 𝑅 Cn 𝑆 ) = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ ∅ ) ⊆ ∪ 𝑆 } ↔ ∀ 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ( 𝑓 “ ∅ ) ⊆ ∪ 𝑆 )
8 6 7 sylibr ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ ∅ ) ⊆ ∪ 𝑆 } )
9 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
10 simpl ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝑅 ∈ Top )
11 simpr ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝑆 ∈ Top )
12 0ss ⊢ ∅ ⊆ ∪ 𝑅
13 12 a1i ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∅ ⊆ ∪ 𝑅 )
14 rest0 ⊢ ( 𝑅 ∈ Top → ( 𝑅 ↾t ∅ ) = { ∅ } )
15 14 adantr ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ↾t ∅ ) = { ∅ } )
16 0cmp ⊢ { ∅ } ∈ Comp
17 15 16 eqeltrdi ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ↾t ∅ ) ∈ Comp )
18 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
19 18 topopn ⊢ ( 𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆 )
20 19 adantl ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∪ 𝑆 ∈ 𝑆 )
21 9 10 11 13 17 20 xkoopn ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ ∅ ) ⊆ ∪ 𝑆 } ∈ ( 𝑆 ↑ko 𝑅 ) )
22 8 21 eqeltrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) ∈ ( 𝑆 ↑ko 𝑅 ) )
23 22 1 eleqtrrdi ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) ∈ 𝐽 )
24 elssuni ⊢ ( ( 𝑅 Cn 𝑆 ) ∈ 𝐽 → ( 𝑅 Cn 𝑆 ) ⊆ ∪ 𝐽 )
25 23 24 syl ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) ⊆ ∪ 𝐽 )
26 eqid ⊢ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } = { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp }
27 eqid ⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
28 9 26 27 xkoval ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
29 28 unieqd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∪ ( 𝑆 ↑ko 𝑅 ) = ∪ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
30 1 unieqi ⊢ ∪ 𝐽 = ∪ ( 𝑆 ↑ko 𝑅 )
31 ovex ⊢ ( 𝑅 Cn 𝑆 ) ∈ V
32 31 pwex ⊢ 𝒫 ( 𝑅 Cn 𝑆 ) ∈ V
33 9 26 27 xkotf ⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 )
34 frn ⊢ ( ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 ) → ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑆 ) )
35 33 34 ax-mp ⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑆 )
36 32 35 ssexi ⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ∈ V
37 fiuni ⊢ ( ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ∈ V → ∪ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ∪ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) )
38 36 37 ax-mp ⊢ ∪ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ∪ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
39 fvex ⊢ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ∈ V
40 unitg ⊢ ( ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ∈ V → ∪ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) = ∪ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) )
41 39 40 ax-mp ⊢ ∪ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) = ∪ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
42 38 41 eqtr4i ⊢ ∪ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ∪ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) )
43 29 30 42 3eqtr4g ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∪ 𝐽 = ∪ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
44 35 a1i ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑆 ) )
45 sspwuni ⊢ ( ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑆 ) ↔ ∪ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ ( 𝑅 Cn 𝑆 ) )
46 44 45 sylib ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∪ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑅 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ ( 𝑅 Cn 𝑆 ) )
47 43 46 eqsstrd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∪ 𝐽 ⊆ ( 𝑅 Cn 𝑆 ) )
48 25 47 eqssd ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) = ∪ 𝐽 )