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

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