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 ⊢ C = ⋃ J
cnextfrel.2 ⊢ B = ⋃ K
Assertion cnextrel ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ C → Rel ⁡ J CnExt K ⁡ F

Proof

Step Hyp Ref Expression
1 cnextfrel.1 ⊢ C = ⋃ J
2 cnextfrel.2 ⊢ B = ⋃ K
3 relxp ⊢ Rel ⁡ x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
4 3 rgenw ⊢ ∀ x ∈ cls ⁡ J ⁡ A Rel ⁡ x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
5 reliun ⊢ Rel ⁡ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ ∀ x ∈ cls ⁡ J ⁡ A Rel ⁡ x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
6 4 5 mpbir ⊢ Rel ⁡ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
7 1 2 cnextfval ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ C → J CnExt K ⁡ F = ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
8 7 releqd ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ C → Rel ⁡ J CnExt K ⁡ F ↔ Rel ⁡ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
9 6 8 mpbiri ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ C → Rel ⁡ J CnExt K ⁡ F