Metamath Proof Explorer

Theorem cnextfun

Description: If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 cnextfrel.1 ⊢ 𝐶 = ∪ 𝐽
2 cnextfrel.2 ⊢ 𝐵 = ∪ 𝐾
3 haustop ⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top )
4 1 2 cnextrel ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
5 3 4 sylanl2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
6 simpllr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐾 ∈ Haus )
7 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
8 7 biimpi ⊢ ( 𝐽 ∈ Top → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
9 8 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
10 simplrr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐴 ⊆ 𝐶 )
11 9 7 sylibr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐽 ∈ Top )
12 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐶 )
13 11 10 12 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐶 )
14 simpr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
15 13 14 sseldd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝑥 ∈ 𝐶 )
16 trnei ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
17 16 biimpa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
18 9 10 15 14 17 syl31anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
19 simplrl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
20 2 hausflf ⊢ ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
21 6 18 19 20 syl3anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
22 21 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
23 22 alrimiv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ∀ 𝑥 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
24 moanimv ⊢ ( ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
25 24 albii ⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
26 23 25 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
27 df-br ⊢ ( 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
28 27 a1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) )
29 1 2 cnextfval ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
30 3 29 sylanl2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
31 30 eleq2d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
32 opeliunxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
33 32 a1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
34 28 31 33 3bitrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
35 34 mobidv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ∃* 𝑦 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
36 35 albidv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ∀ 𝑥 ∃* 𝑦 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
37 26 36 mpbird ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ∀ 𝑥 ∃* 𝑦 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 )
38 dffun6 ⊢ ( Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ ( Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ) )
39 5 37 38 sylanbrc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )