Metamath Proof Explorer

Theorem cnextfvval

Description: The value of the continuous extension of a given function F at a point X . (Contributed by Thierry Arnoux, 21-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 cnextfvval ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑋 ) = ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )

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 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝐽 ∈ Top )
10 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝐾 ∈ Haus )
11 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
12 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝐴 ⊆ 𝐶 )
13 1 2 cnextfun ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
14 9 10 11 12 13 syl22anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
15 7 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑋 ∈ 𝐶 ) )
16 15 biimpar ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
17 fvex ⊢ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V
18 17 uniex ⊢ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V
19 18 snid ⊢ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) }
20 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
21 20 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) )
22 21 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) )
23 22 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) )
24 23 fveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
25 24 breq1d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) )
26 25 imbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝜑 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) ↔ ( 𝜑 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) ) )
27 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐾 ∈ Haus )
28 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐽 ∈ Top )
29 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
30 28 29 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
31 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐴 ⊆ 𝐶 )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
33 7 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑥 ∈ 𝐶 ) )
34 33 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
35 trnei ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
36 35 biimpa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
37 30 31 32 34 36 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
38 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
39 2 hausflf2 ⊢ ( ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
40 27 37 38 8 39 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
41 40 expcom ⊢ ( 𝑥 ∈ 𝐶 → ( 𝜑 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) )
42 26 41 vtoclga ⊢ ( 𝑋 ∈ 𝐶 → ( 𝜑 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) )
43 42 impcom ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
44 en1b ⊢ ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } )
45 43 44 sylib ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } )
46 19 45 eleqtrrid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
47 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
48 47 nfel2 ⊢ Ⅎ 𝑥 ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
49 nfv ⊢ Ⅎ 𝑥 ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
50 48 49 nfbi ⊢ Ⅎ 𝑥 ( ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
51 opeq1 ⊢ ( 𝑥 = 𝑋 → ⟨ 𝑥 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ = ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ )
52 51 eleq1d ⊢ ( 𝑥 = 𝑋 → ( ⟨ 𝑥 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
53 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
54 24 eleq2d ⊢ ( 𝑥 = 𝑋 → ( ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
55 53 54 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
56 52 55 bibi12d ⊢ ( 𝑥 = 𝑋 → ( ( ⟨ 𝑥 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) ↔ ( ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) ) )
57 opeliunxp ⊢ ( ⟨ 𝑥 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
58 50 56 57 vtoclg1f ⊢ ( 𝑋 ∈ 𝐶 → ( ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
60 16 46 59 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
61 df-br ⊢ ( 𝑋 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
62 haustop ⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top )
63 4 62 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝐾 ∈ Top )
65 1 2 cnextfval ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
66 9 64 11 12 65 syl22anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
67 66 eleq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
68 61 67 bitrid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝑋 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ⟨ 𝑋 , ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) )
69 60 68 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
70 funbrfv ⊢ ( Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) → ( 𝑋 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑋 ) = ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
71 14 69 70 sylc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑋 ) = ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )