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 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )