This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 vsnex ⊢ { 𝑥 } ∈ 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 𝐴 ) ) ‘ 𝐹 ) ) )