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 ⊢X=⋃J
cnextfval.2 ⊢B=⋃K
Assertion cnextfval ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→JCnExtK⁡F=⋃x∈cls⁡J⁡Ax×KfLimfnei⁡J⁡x↾𝑡A⁡F

Proof

Step Hyp Ref Expression
1 cnextfval.1 ⊢X=⋃J
2 cnextfval.2 ⊢B=⋃K
3 cnextval ⊢J∈Top∧K∈Top→JCnExtK=f∈⋃K↑𝑝𝑚⋃J⟼⋃x∈cls⁡J⁡dom⁡fx×KfLimfnei⁡J⁡x↾𝑡dom⁡f⁡f
4 3 adantr ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→JCnExtK=f∈⋃K↑𝑝𝑚⋃J⟼⋃x∈cls⁡J⁡dom⁡fx×KfLimfnei⁡J⁡x↾𝑡dom⁡f⁡f
5 simpr ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→f=F
6 5 dmeqd ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→dom⁡f=dom⁡F
7 simplrl ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→F:A⟶B
8 7 fdmd ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→dom⁡F=A
9 6 8 eqtrd ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→dom⁡f=A
10 9 fveq2d ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→cls⁡J⁡dom⁡f=cls⁡J⁡A
11 9 oveq2d ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→nei⁡J⁡x↾𝑡dom⁡f=nei⁡J⁡x↾𝑡A
12 11 oveq2d ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→KfLimfnei⁡J⁡x↾𝑡dom⁡f=KfLimfnei⁡J⁡x↾𝑡A
13 12 5 fveq12d ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→KfLimfnei⁡J⁡x↾𝑡dom⁡f⁡f=KfLimfnei⁡J⁡x↾𝑡A⁡F
14 13 xpeq2d ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→x×KfLimfnei⁡J⁡x↾𝑡dom⁡f⁡f=x×KfLimfnei⁡J⁡x↾𝑡A⁡F
15 10 14 iuneq12d ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X∧f=F→⋃x∈cls⁡J⁡dom⁡fx×KfLimfnei⁡J⁡x↾𝑡dom⁡f⁡f=⋃x∈cls⁡J⁡Ax×KfLimfnei⁡J⁡x↾𝑡A⁡F
16 uniexg ⊢K∈Top→⋃K∈V
17 16 ad2antlr ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→⋃K∈V
18 uniexg ⊢J∈Top→⋃J∈V
19 18 ad2antrr ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→⋃J∈V
20 eqid ⊢A=A
21 20 2 feq23i ⊢F:A⟶B↔F:A⟶⋃K
22 21 biimpi ⊢F:A⟶B→F:A⟶⋃K
23 22 ad2antrl ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→F:A⟶⋃K
24 1 sseq2i ⊢A⊆X↔A⊆⋃J
25 24 biimpi ⊢A⊆X→A⊆⋃J
26 25 ad2antll ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→A⊆⋃J
27 elpm2r ⊢⋃K∈V∧⋃J∈V∧F:A⟶⋃K∧A⊆⋃J→F∈⋃K↑𝑝𝑚⋃J
28 17 19 23 26 27 syl22anc ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→F∈⋃K↑𝑝𝑚⋃J
29 fvex ⊢cls⁡J⁡A∈V
30 vsnex ⊢x∈V
31 fvex ⊢KfLimfnei⁡J⁡x↾𝑡A⁡F∈V
32 30 31 xpex ⊢x×KfLimfnei⁡J⁡x↾𝑡A⁡F∈V
33 29 32 iunex ⊢⋃x∈cls⁡J⁡Ax×KfLimfnei⁡J⁡x↾𝑡A⁡F∈V
34 33 a1i ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→⋃x∈cls⁡J⁡Ax×KfLimfnei⁡J⁡x↾𝑡A⁡F∈V
35 4 15 28 34 fvmptd ⊢J∈Top∧K∈Top∧F:A⟶B∧A⊆X→JCnExtK⁡F=⋃x∈cls⁡J⁡Ax×KfLimfnei⁡J⁡x↾𝑡A⁡F