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

Metamath Proof Explorer

Theorem cnextrel

Description: In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017)

Ref Expression
Hypotheses cnextfrel.1 ⊢ 𝐶 = ∪ 𝐽
cnextfrel.2 ⊢ 𝐵 = ∪ 𝐾
Assertion cnextrel ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 cnextfrel.1 ⊢ 𝐶 = ∪ 𝐽
2 cnextfrel.2 ⊢ 𝐵 = ∪ 𝐾
3 relxp ⊢ Rel ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
4 3 rgenw ⊢ ∀ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) Rel ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
5 reliun ⊢ ( Rel ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ∀ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) Rel ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
6 4 5 mpbir ⊢ Rel ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
7 1 2 cnextfval ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
8 7 releqd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ Rel ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
9 6 8 mpbiri ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )