Metamath Proof Explorer

Theorem xkoopn

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

Ref Expression
Hypotheses xkoopn.x ⊢ 𝑋 = ∪ 𝑅
xkoopn.r ⊢ ( 𝜑 → 𝑅 ∈ Top )
xkoopn.s ⊢ ( 𝜑 → 𝑆 ∈ Top )
xkoopn.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
xkoopn.c ⊢ ( 𝜑 → ( 𝑅 ↾t 𝐴 ) ∈ Comp )
xkoopn.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion xkoopn ( 𝜑 → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } ∈ ( 𝑆 ↑ko 𝑅 ) )

Proof

Step Hyp Ref Expression
1 xkoopn.x ⊢ 𝑋 = ∪ 𝑅
2 xkoopn.r ⊢ ( 𝜑 → 𝑅 ∈ Top )
3 xkoopn.s ⊢ ( 𝜑 → 𝑆 ∈ Top )
4 xkoopn.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
5 xkoopn.c ⊢ ( 𝜑 → ( 𝑅 ↾t 𝐴 ) ∈ Comp )
6 xkoopn.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 ovex ⊢ ( 𝑅 Cn 𝑆 ) ∈ V
8 7 pwex ⊢ 𝒫 ( 𝑅 Cn 𝑆 ) ∈ V
9 eqid ⊢ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp }
10 eqid ⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
11 1 9 10 xkotf ⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 )
12 frn ⊢ ( ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) : ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } × 𝑆 ) ⟶ 𝒫 ( 𝑅 Cn 𝑆 ) → ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑆 ) )
13 11 12 ax-mp ⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ 𝒫 ( 𝑅 Cn 𝑆 )
14 8 13 ssexi ⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ∈ V
15 ssfii ⊢ ( ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ∈ V → ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) )
16 14 15 ax-mp ⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
17 fvex ⊢ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ∈ V
18 bastg ⊢ ( ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ∈ V → ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ⊆ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
19 17 18 ax-mp ⊢ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ⊆ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) )
20 16 19 sstri ⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ⊆ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) )
21 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑅 ↾t 𝑥 ) = ( 𝑅 ↾t 𝐴 ) )
22 21 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑅 ↾t 𝑥 ) ∈ Comp ↔ ( 𝑅 ↾t 𝐴 ) ∈ Comp ) )
23 1 topopn ⊢ ( 𝑅 ∈ Top → 𝑋 ∈ 𝑅 )
24 elpw2g ⊢ ( 𝑋 ∈ 𝑅 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
25 2 23 24 3syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
26 4 25 mpbird ⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝑋 )
27 22 26 5 elrabd ⊢ ( 𝜑 → 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } )
28 eqidd ⊢ ( 𝜑 → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } )
29 imaeq2 ⊢ ( 𝑘 = 𝐴 → ( 𝑓 “ 𝑘 ) = ( 𝑓 “ 𝐴 ) )
30 29 sseq1d ⊢ ( 𝑘 = 𝐴 → ( ( 𝑓 “ 𝑘 ) ⊆ 𝑣 ↔ ( 𝑓 “ 𝐴 ) ⊆ 𝑣 ) )
31 30 rabbidv ⊢ ( 𝑘 = 𝐴 → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑣 } )
32 31 eqeq2d ⊢ ( 𝑘 = 𝐴 → ( { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑣 } ) )
33 sseq2 ⊢ ( 𝑣 = 𝑈 → ( ( 𝑓 “ 𝐴 ) ⊆ 𝑣 ↔ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 ) )
34 33 rabbidv ⊢ ( 𝑣 = 𝑈 → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑣 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } )
35 34 eqeq2d ⊢ ( 𝑣 = 𝑈 → ( { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑣 } ↔ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } ) )
36 32 35 rspc2ev ⊢ ( ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∧ 𝑈 ∈ 𝑆 ∧ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } ) → ∃ 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∃ 𝑣 ∈ 𝑆 { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
37 27 6 28 36 syl3anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∃ 𝑣 ∈ 𝑆 { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
38 7 rabex ⊢ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } ∈ V
39 eqeq1 ⊢ ( 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } → ( 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
40 39 2rexbidv ⊢ ( 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } → ( ∃ 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∃ 𝑣 ∈ 𝑆 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ↔ ∃ 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∃ 𝑣 ∈ 𝑆 { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
41 10 rnmpo ⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) = { 𝑦 ∣ ∃ 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∃ 𝑣 ∈ 𝑆 𝑦 = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } }
42 38 40 41 elab2 ⊢ ( { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } ∈ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ↔ ∃ 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } ∃ 𝑣 ∈ 𝑆 { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } = { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
43 37 42 sylibr ⊢ ( 𝜑 → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } ∈ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
44 20 43 sselid ⊢ ( 𝜑 → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } ∈ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
45 1 9 10 xkoval ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
46 2 3 45 syl2anc ⊢ ( 𝜑 → ( 𝑆 ↑ko 𝑅 ) = ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑅 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑆 ↦ { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
47 44 46 eleqtrrd ⊢ ( 𝜑 → { 𝑓 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑓 “ 𝐴 ) ⊆ 𝑈 } ∈ ( 𝑆 ↑ko 𝑅 ) )