Metamath Proof Explorer

Theorem cnextf

Description: Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017)

Ref Expression
Hypotheses cnextf.1 ⊢ 𝐶 = ∪ 𝐽
cnextf.2 ⊢ 𝐵 = ∪ 𝐾
cnextf.3 ⊢ ( 𝜑 → 𝐽 ∈ Top )
cnextf.4 ⊢ ( 𝜑 → 𝐾 ∈ Haus )
cnextf.5 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
cnextf.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
cnextf.6 ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝐶 )
cnextf.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
Assertion cnextf ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) : 𝐶 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 cnextf.1 ⊢ 𝐶 = ∪ 𝐽
2 cnextf.2 ⊢ 𝐵 = ∪ 𝐾
3 cnextf.3 ⊢ ( 𝜑 → 𝐽 ∈ Top )
4 cnextf.4 ⊢ ( 𝜑 → 𝐾 ∈ Haus )
5 cnextf.5 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6 cnextf.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
7 cnextf.6 ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝐶 )
8 cnextf.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
9 1 2 cnextfun ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
10 3 4 5 6 9 syl22anc ⊢ ( 𝜑 → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
11 dfdm3 ⊢ dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = { 𝑥 ∣ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) }
12 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝜑 )
13 7 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑥 ∈ 𝐶 ) )
14 13 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
15 n0 ⊢ ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
16 8 15 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
17 haustop ⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top )
18 4 17 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
19 1 2 cnextfval ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
20 3 18 5 6 19 syl22anc ⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
21 20 eleq2d ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
22 opeliunxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
23 21 22 bitrdi ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
24 23 exbidv ⊢ ( 𝜑 → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ ∃ 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
25 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∃ 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
26 24 25 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∃ 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
27 26 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∃ 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) → ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
28 12 14 16 27 syl12anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
29 26 simprbda ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
30 13 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑥 ∈ 𝐶 ) )
31 29 30 mpbid ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) → 𝑥 ∈ 𝐶 )
32 28 31 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) )
33 32 abbi2dv ⊢ ( 𝜑 → 𝐶 = { 𝑥 ∣ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) } )
34 11 33 eqtr4id ⊢ ( 𝜑 → dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = 𝐶 )
35 df-fn ⊢ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) Fn 𝐶 ↔ ( Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∧ dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = 𝐶 ) )
36 10 34 35 sylanbrc ⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) Fn 𝐶 )
37 20 rneqd ⊢ ( 𝜑 → ran ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ran ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
38 rniun ⊢ ran ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ran ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
39 vex ⊢ 𝑥 ∈ V
40 39 snnz ⊢ { 𝑥 } ≠ ∅
41 rnxp ⊢ ( { 𝑥 } ≠ ∅ → ran ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
42 40 41 ax-mp ⊢ ran ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 )
43 13 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝑥 ∈ 𝐶 )
44 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
45 18 44 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
47 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
48 3 47 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
50 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐴 ⊆ 𝐶 )
51 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
52 trnei ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
53 52 biimpa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
54 49 50 51 14 53 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
55 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
56 flfelbas ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) → 𝑦 ∈ 𝐵 )
57 56 ex ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) → 𝑦 ∈ 𝐵 ) )
58 57 ssrdv ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⊆ 𝐵 )
59 46 54 55 58 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⊆ 𝐵 )
60 43 59 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⊆ 𝐵 )
61 42 60 eqsstrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ran ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ⊆ 𝐵 )
62 61 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ran ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ⊆ 𝐵 )
63 iunss ⊢ ( ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ran ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ran ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ⊆ 𝐵 )
64 62 63 sylibr ⊢ ( 𝜑 → ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ran ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ⊆ 𝐵 )
65 38 64 eqsstrid ⊢ ( 𝜑 → ran ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ⊆ 𝐵 )
66 37 65 eqsstrd ⊢ ( 𝜑 → ran ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ⊆ 𝐵 )
67 df-f ⊢ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) : 𝐶 ⟶ 𝐵 ↔ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) Fn 𝐶 ∧ ran ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ⊆ 𝐵 ) )
68 36 66 67 sylanbrc ⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) : 𝐶 ⟶ 𝐵 )