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

Metamath Proof Explorer

Theorem cnpfval

Description: The function mapping the points in a topology J to the set of all functions from J to topology K continuous at that point. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnpfval ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )

Proof

Step Hyp Ref Expression
1 df-cnp ⊢ CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑤 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝑗 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
2 1 a1i ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑤 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝑗 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) ) )
3 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑗 = 𝐽 )
4 3 unieqd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑗 = ∪ 𝐽 )
5 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
6 5 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑋 = ∪ 𝐽 )
7 4 6 eqtr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑗 = 𝑋 )
8 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑘 = 𝐾 )
9 8 unieqd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑘 = ∪ 𝐾 )
10 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
11 10 ad2antlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑌 = ∪ 𝐾 )
12 9 11 eqtr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑘 = 𝑌 )
13 12 7 oveq12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ∪ 𝑘 ↑m ∪ 𝑗 ) = ( 𝑌 ↑m 𝑋 ) )
14 3 rexeqdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ∃ 𝑣 ∈ 𝑗 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ↔ ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) )
15 14 imbi2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝑗 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) ) )
16 8 15 raleqbidv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ∀ 𝑤 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝑗 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) ) )
17 13 16 rabeqbidv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑤 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝑗 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } )
18 7 17 mpteq12dv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑤 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝑗 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
19 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
20 19 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐽 ∈ Top )
21 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
22 21 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐾 ∈ Top )
23 ovex ⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
24 ssrab2 ⊢ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ⊆ ( 𝑌 ↑m 𝑋 )
25 23 24 elpwi2 ⊢ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ 𝒫 ( 𝑌 ↑m 𝑋 )
26 25 a1i ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ 𝒫 ( 𝑌 ↑m 𝑋 ) )
27 26 fmpttd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) : 𝑋 ⟶ 𝒫 ( 𝑌 ↑m 𝑋 ) )
28 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
29 28 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → 𝑋 ∈ 𝐽 )
30 23 pwex ⊢ 𝒫 ( 𝑌 ↑m 𝑋 ) ∈ V
31 30 a1i ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → 𝒫 ( 𝑌 ↑m 𝑋 ) ∈ V )
32 fex2 ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) : 𝑋 ⟶ 𝒫 ( 𝑌 ↑m 𝑋 ) ∧ 𝑋 ∈ 𝐽 ∧ 𝒫 ( 𝑌 ↑m 𝑋 ) ∈ V ) → ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) ∈ V )
33 27 29 31 32 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) ∈ V )
34 2 18 20 22 33 ovmpod ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )