Metamath Proof Explorer


Theorem cnextfval

Description: The continuous extension of a given function F . (Contributed by Thierry Arnoux, 1-Dec-2017)

Ref Expression
Hypotheses cnextfval.1 𝑋 = 𝐽
cnextfval.2 𝐵 = 𝐾
Assertion cnextfval ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 cnextfval.1 𝑋 = 𝐽
2 cnextfval.2 𝐵 = 𝐾
3 cnextval ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 CnExt 𝐾 ) = ( 𝑓 ∈ ( 𝐾pm 𝐽 ) ↦ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) )
4 3 adantr ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → ( 𝐽 CnExt 𝐾 ) = ( 𝑓 ∈ ( 𝐾pm 𝐽 ) ↦ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) )
5 simpr ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
6 5 dmeqd ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = dom 𝐹 )
7 simplrl ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → 𝐹 : 𝐴𝐵 )
8 7 fdmd ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → dom 𝐹 = 𝐴 )
9 6 8 eqtrd ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = 𝐴 )
10 9 fveq2d ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
11 9 oveq2d ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) )
12 11 oveq2d ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) )
13 12 5 fveq12d ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
14 13 xpeq2d ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) = ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
15 10 14 iuneq12d ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) ∧ 𝑓 = 𝐹 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) = 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
16 uniexg ( 𝐾 ∈ Top → 𝐾 ∈ V )
17 16 ad2antlr ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → 𝐾 ∈ V )
18 uniexg ( 𝐽 ∈ Top → 𝐽 ∈ V )
19 18 ad2antrr ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → 𝐽 ∈ V )
20 eqid 𝐴 = 𝐴
21 20 2 feq23i ( 𝐹 : 𝐴𝐵𝐹 : 𝐴 𝐾 )
22 21 biimpi ( 𝐹 : 𝐴𝐵𝐹 : 𝐴 𝐾 )
23 22 ad2antrl ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → 𝐹 : 𝐴 𝐾 )
24 1 sseq2i ( 𝐴𝑋𝐴 𝐽 )
25 24 biimpi ( 𝐴𝑋𝐴 𝐽 )
26 25 ad2antll ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → 𝐴 𝐽 )
27 elpm2r ( ( ( 𝐾 ∈ V ∧ 𝐽 ∈ V ) ∧ ( 𝐹 : 𝐴 𝐾𝐴 𝐽 ) ) → 𝐹 ∈ ( 𝐾pm 𝐽 ) )
28 17 19 23 26 27 syl22anc ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → 𝐹 ∈ ( 𝐾pm 𝐽 ) )
29 fvex ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∈ V
30 snex { 𝑥 } ∈ V
31 fvex ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V
32 30 31 xpex ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ∈ V
33 29 32 iunex 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ∈ V
34 33 a1i ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ∈ V )
35 4 15 28 34 fvmptd ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴𝐵𝐴𝑋 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )