Theorem iscnp2

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". Based on Theorem 7.2(g) of Munkres p. 107. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	iscn.1	⊢ 𝑋 = ∪ 𝐽
	iscn.2	⊢ 𝑌 = ∪ 𝐾
Assertion	iscnp2	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscn.1	⊢ 𝑋 = ∪ 𝐽
2		iscn.2	⊢ 𝑌 = ∪ 𝐾
3		n0i	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ¬ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ∅ )
4		df-ov	⊢ ( 𝐽 CnP 𝐾 ) = ( CnP ‘ ⟨ 𝐽 , 𝐾 ⟩ )
5		ndmfv	⊢ ( ¬ ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP → ( CnP ‘ ⟨ 𝐽 , 𝐾 ⟩ ) = ∅ )
6	4 5	syl5eq	⊢ ( ¬ ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP → ( 𝐽 CnP 𝐾 ) = ∅ )
7	6	fveq1d	⊢ ( ¬ ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ( ∅ ‘ 𝑃 ) )
8		0fv	⊢ ( ∅ ‘ 𝑃 ) = ∅
9	7 8	eqtrdi	⊢ ( ¬ ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ∅ )
10	3 9	nsyl2	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP )
11		df-cnp	⊢ CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) )
12		ovex	⊢ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V
13		ssrab2	⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ⊆ ( ∪ 𝑘 ↑m ∪ 𝑗 )
14	12 13	elpwi2	⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 )
15	14	rgenw	⊢ ∀ 𝑥 ∈ ∪ 𝑗 { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 )
16		eqid	⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } )
17	16	fmpt	⊢ ( ∀ 𝑥 ∈ ∪ 𝑗 { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ↔ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) )
18	15 17	mpbi	⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 )
19		vuniex	⊢ ∪ 𝑗 ∈ V
20	12	pwex	⊢ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V
21		fex2	⊢ ( ( ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∧ ∪ 𝑗 ∈ V ∧ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V ) → ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) ∈ V )
22	18 19 20 21	mp3an	⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) ∈ V
23	11 22	dmmpo	⊢ dom CnP = ( Top × Top )
24	10 23	eleqtrdi	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ⟨ 𝐽 , 𝐾 ⟩ ∈ ( Top × Top ) )
25		opelxp	⊢ ( ⟨ 𝐽 , 𝐾 ⟩ ∈ ( Top × Top ) ↔ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )
26	24 25	sylib	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )
27	26	simpld	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐽 ∈ Top )
28	26	simprd	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top )
29		elfvdm	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ dom ( 𝐽 CnP 𝐾 ) )
30	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
31	2	toptopon	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
32		cnpfval	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
33	30 31 32	syl2anb	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
34	26 33	syl	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
35	34	dmeqd	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → dom ( 𝐽 CnP 𝐾 ) = dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
36		ovex	⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
37	36	rabex	⊢ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V
38	37	rgenw	⊢ ∀ 𝑥 ∈ 𝑋 { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V
39		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝑋 { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V → dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) = 𝑋 )
40	38 39	ax-mp	⊢ dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) = 𝑋
41	35 40	eqtrdi	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → dom ( 𝐽 CnP 𝐾 ) = 𝑋 )
42	29 41	eleqtrd	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ 𝑋 )
43	27 28 42	3jca	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) )
44		biid	⊢ ( 𝑃 ∈ 𝑋 ↔ 𝑃 ∈ 𝑋 )
45		iscnp	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
46	30 31 44 45	syl3anb	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
47	43 46	biadanii	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )