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 𝐾 ) ‘ 𝐹 ) )