Metamath Proof Explorer


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 ‘ 𝐽 ) ‘ { 𝑝 } ) ( 𝐹𝑣 ) ⊆ 𝑤 ) )