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