Theorem cnnei

Description: Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018)

	Ref	Expression
Hypotheses	cnnei.x	⊢ 𝑋 = ∪ 𝐽
	cnnei.y	⊢ 𝑌 = ∪ 𝐾
Assertion	cnnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )

Proof

Step	Hyp	Ref	Expression
1		cnnei.x	⊢ 𝑋 = ∪ 𝐽
2		cnnei.y	⊢ 𝑌 = ∪ 𝐾
3	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4	2	toptopon	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
5	3 4	anbi12i	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ↔ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) )
6		cncnp	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑝 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ) ) )
7	6	baibd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ) )
8	5 7	sylanb	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ) )
9	5	anbi1i	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ↔ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) )
10		iscnp4	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) )
11	10	3expa	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) )
12	11	baibd	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
13	12	an32s	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
14	9 13	sylanb	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
15	14	ralbidva	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑝 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑝 ) ↔ ∀ 𝑝 ∈ 𝑋 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
16	8 15	bitrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
17	16	3impa	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑝 ∈ 𝑋 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑝 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )