# Metamath Proof Explorer

## Theorem cnmpopc

Description: Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses cnmpopc.r ${⊢}{R}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
cnmpopc.m ${⊢}{M}={R}{↾}_{𝑡}\left[{A},{B}\right]$
cnmpopc.n ${⊢}{N}={R}{↾}_{𝑡}\left[{B},{C}\right]$
cnmpopc.o ${⊢}{O}={R}{↾}_{𝑡}\left[{A},{C}\right]$
cnmpopc.a ${⊢}{\phi }\to {A}\in ℝ$
cnmpopc.c ${⊢}{\phi }\to {C}\in ℝ$
cnmpopc.b ${⊢}{\phi }\to {B}\in \left[{A},{C}\right]$
cnmpopc.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
cnmpopc.q ${⊢}\left({\phi }\wedge \left({x}={B}\wedge {y}\in {X}\right)\right)\to {D}={E}$
cnmpopc.d ${⊢}{\phi }\to \left({x}\in \left[{A},{B}\right],{y}\in {X}⟼{D}\right)\in \left(\left({M}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
cnmpopc.e ${⊢}{\phi }\to \left({x}\in \left[{B},{C}\right],{y}\in {X}⟼{E}\right)\in \left(\left({N}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
Assertion cnmpopc ${⊢}{\phi }\to \left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)\in \left(\left({O}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$

### Proof

Step Hyp Ref Expression
1 cnmpopc.r ${⊢}{R}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
2 cnmpopc.m ${⊢}{M}={R}{↾}_{𝑡}\left[{A},{B}\right]$
3 cnmpopc.n ${⊢}{N}={R}{↾}_{𝑡}\left[{B},{C}\right]$
4 cnmpopc.o ${⊢}{O}={R}{↾}_{𝑡}\left[{A},{C}\right]$
5 cnmpopc.a ${⊢}{\phi }\to {A}\in ℝ$
6 cnmpopc.c ${⊢}{\phi }\to {C}\in ℝ$
7 cnmpopc.b ${⊢}{\phi }\to {B}\in \left[{A},{C}\right]$
8 cnmpopc.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
9 cnmpopc.q ${⊢}\left({\phi }\wedge \left({x}={B}\wedge {y}\in {X}\right)\right)\to {D}={E}$
10 cnmpopc.d ${⊢}{\phi }\to \left({x}\in \left[{A},{B}\right],{y}\in {X}⟼{D}\right)\in \left(\left({M}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
11 cnmpopc.e ${⊢}{\phi }\to \left({x}\in \left[{B},{C}\right],{y}\in {X}⟼{E}\right)\in \left(\left({N}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
12 eqid ${⊢}\bigcup \left({O}{×}_{t}{J}\right)=\bigcup \left({O}{×}_{t}{J}\right)$
13 eqid ${⊢}\bigcup {K}=\bigcup {K}$
14 iccssre ${⊢}\left({A}\in ℝ\wedge {C}\in ℝ\right)\to \left[{A},{C}\right]\subseteq ℝ$
15 5 6 14 syl2anc ${⊢}{\phi }\to \left[{A},{C}\right]\subseteq ℝ$
16 15 7 sseldd ${⊢}{\phi }\to {B}\in ℝ$
17 icccld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
18 5 16 17 syl2anc ${⊢}{\phi }\to \left[{A},{B}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
19 1 fveq2i ${⊢}\mathrm{Clsd}\left({R}\right)=\mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
20 18 19 eleqtrrdi ${⊢}{\phi }\to \left[{A},{B}\right]\in \mathrm{Clsd}\left({R}\right)$
21 ssun1 ${⊢}\left[{A},{B}\right]\subseteq \left[{A},{B}\right]\cup \left[{B},{C}\right]$
22 iccsplit ${⊢}\left({A}\in ℝ\wedge {C}\in ℝ\wedge {B}\in \left[{A},{C}\right]\right)\to \left[{A},{C}\right]=\left[{A},{B}\right]\cup \left[{B},{C}\right]$
23 5 6 7 22 syl3anc ${⊢}{\phi }\to \left[{A},{C}\right]=\left[{A},{B}\right]\cup \left[{B},{C}\right]$
24 21 23 sseqtrrid ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq \left[{A},{C}\right]$
25 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
26 1 unieqi ${⊢}\bigcup {R}=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
27 25 26 eqtr4i ${⊢}ℝ=\bigcup {R}$
28 27 restcldi ${⊢}\left(\left[{A},{C}\right]\subseteq ℝ\wedge \left[{A},{B}\right]\in \mathrm{Clsd}\left({R}\right)\wedge \left[{A},{B}\right]\subseteq \left[{A},{C}\right]\right)\to \left[{A},{B}\right]\in \mathrm{Clsd}\left({R}{↾}_{𝑡}\left[{A},{C}\right]\right)$
29 15 20 24 28 syl3anc ${⊢}{\phi }\to \left[{A},{B}\right]\in \mathrm{Clsd}\left({R}{↾}_{𝑡}\left[{A},{C}\right]\right)$
30 4 fveq2i ${⊢}\mathrm{Clsd}\left({O}\right)=\mathrm{Clsd}\left({R}{↾}_{𝑡}\left[{A},{C}\right]\right)$
31 29 30 eleqtrrdi ${⊢}{\phi }\to \left[{A},{B}\right]\in \mathrm{Clsd}\left({O}\right)$
32 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
33 8 32 syl ${⊢}{\phi }\to {X}=\bigcup {J}$
34 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
35 eqid ${⊢}\bigcup {J}=\bigcup {J}$
36 35 topcld ${⊢}{J}\in \mathrm{Top}\to \bigcup {J}\in \mathrm{Clsd}\left({J}\right)$
37 8 34 36 3syl ${⊢}{\phi }\to \bigcup {J}\in \mathrm{Clsd}\left({J}\right)$
38 33 37 eqeltrd ${⊢}{\phi }\to {X}\in \mathrm{Clsd}\left({J}\right)$
39 txcld ${⊢}\left(\left[{A},{B}\right]\in \mathrm{Clsd}\left({O}\right)\wedge {X}\in \mathrm{Clsd}\left({J}\right)\right)\to \left[{A},{B}\right]×{X}\in \mathrm{Clsd}\left({O}{×}_{t}{J}\right)$
40 31 38 39 syl2anc ${⊢}{\phi }\to \left[{A},{B}\right]×{X}\in \mathrm{Clsd}\left({O}{×}_{t}{J}\right)$
41 icccld ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to \left[{B},{C}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
42 16 6 41 syl2anc ${⊢}{\phi }\to \left[{B},{C}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
43 42 19 eleqtrrdi ${⊢}{\phi }\to \left[{B},{C}\right]\in \mathrm{Clsd}\left({R}\right)$
44 ssun2 ${⊢}\left[{B},{C}\right]\subseteq \left[{A},{B}\right]\cup \left[{B},{C}\right]$
45 44 23 sseqtrrid ${⊢}{\phi }\to \left[{B},{C}\right]\subseteq \left[{A},{C}\right]$
46 27 restcldi ${⊢}\left(\left[{A},{C}\right]\subseteq ℝ\wedge \left[{B},{C}\right]\in \mathrm{Clsd}\left({R}\right)\wedge \left[{B},{C}\right]\subseteq \left[{A},{C}\right]\right)\to \left[{B},{C}\right]\in \mathrm{Clsd}\left({R}{↾}_{𝑡}\left[{A},{C}\right]\right)$
47 15 43 45 46 syl3anc ${⊢}{\phi }\to \left[{B},{C}\right]\in \mathrm{Clsd}\left({R}{↾}_{𝑡}\left[{A},{C}\right]\right)$
48 47 30 eleqtrrdi ${⊢}{\phi }\to \left[{B},{C}\right]\in \mathrm{Clsd}\left({O}\right)$
49 txcld ${⊢}\left(\left[{B},{C}\right]\in \mathrm{Clsd}\left({O}\right)\wedge {X}\in \mathrm{Clsd}\left({J}\right)\right)\to \left[{B},{C}\right]×{X}\in \mathrm{Clsd}\left({O}{×}_{t}{J}\right)$
50 48 38 49 syl2anc ${⊢}{\phi }\to \left[{B},{C}\right]×{X}\in \mathrm{Clsd}\left({O}{×}_{t}{J}\right)$
51 23 xpeq1d ${⊢}{\phi }\to \left[{A},{C}\right]×{X}=\left(\left[{A},{B}\right]\cup \left[{B},{C}\right]\right)×{X}$
52 xpundir ${⊢}\left(\left[{A},{B}\right]\cup \left[{B},{C}\right]\right)×{X}=\left(\left[{A},{B}\right]×{X}\right)\cup \left(\left[{B},{C}\right]×{X}\right)$
53 51 52 eqtrdi ${⊢}{\phi }\to \left[{A},{C}\right]×{X}=\left(\left[{A},{B}\right]×{X}\right)\cup \left(\left[{B},{C}\right]×{X}\right)$
54 retopon ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
55 1 54 eqeltri ${⊢}{R}\in \mathrm{TopOn}\left(ℝ\right)$
56 resttopon ${⊢}\left({R}\in \mathrm{TopOn}\left(ℝ\right)\wedge \left[{A},{C}\right]\subseteq ℝ\right)\to {R}{↾}_{𝑡}\left[{A},{C}\right]\in \mathrm{TopOn}\left(\left[{A},{C}\right]\right)$
57 55 15 56 sylancr ${⊢}{\phi }\to {R}{↾}_{𝑡}\left[{A},{C}\right]\in \mathrm{TopOn}\left(\left[{A},{C}\right]\right)$
58 4 57 eqeltrid ${⊢}{\phi }\to {O}\in \mathrm{TopOn}\left(\left[{A},{C}\right]\right)$
59 txtopon ${⊢}\left({O}\in \mathrm{TopOn}\left(\left[{A},{C}\right]\right)\wedge {J}\in \mathrm{TopOn}\left({X}\right)\right)\to {O}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{A},{C}\right]×{X}\right)$
60 58 8 59 syl2anc ${⊢}{\phi }\to {O}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{A},{C}\right]×{X}\right)$
61 toponuni ${⊢}{O}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{A},{C}\right]×{X}\right)\to \left[{A},{C}\right]×{X}=\bigcup \left({O}{×}_{t}{J}\right)$
62 60 61 syl ${⊢}{\phi }\to \left[{A},{C}\right]×{X}=\bigcup \left({O}{×}_{t}{J}\right)$
63 53 62 eqtr3d ${⊢}{\phi }\to \left(\left[{A},{B}\right]×{X}\right)\cup \left(\left[{B},{C}\right]×{X}\right)=\bigcup \left({O}{×}_{t}{J}\right)$
64 24 15 sstrd ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq ℝ$
65 resttopon ${⊢}\left({R}\in \mathrm{TopOn}\left(ℝ\right)\wedge \left[{A},{B}\right]\subseteq ℝ\right)\to {R}{↾}_{𝑡}\left[{A},{B}\right]\in \mathrm{TopOn}\left(\left[{A},{B}\right]\right)$
66 55 64 65 sylancr ${⊢}{\phi }\to {R}{↾}_{𝑡}\left[{A},{B}\right]\in \mathrm{TopOn}\left(\left[{A},{B}\right]\right)$
67 2 66 eqeltrid ${⊢}{\phi }\to {M}\in \mathrm{TopOn}\left(\left[{A},{B}\right]\right)$
68 txtopon ${⊢}\left({M}\in \mathrm{TopOn}\left(\left[{A},{B}\right]\right)\wedge {J}\in \mathrm{TopOn}\left({X}\right)\right)\to {M}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{A},{B}\right]×{X}\right)$
69 67 8 68 syl2anc ${⊢}{\phi }\to {M}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{A},{B}\right]×{X}\right)$
70 cntop2 ${⊢}\left({x}\in \left[{A},{B}\right],{y}\in {X}⟼{D}\right)\in \left(\left({M}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)\to {K}\in \mathrm{Top}$
71 10 70 syl ${⊢}{\phi }\to {K}\in \mathrm{Top}$
72 toptopon2 ${⊢}{K}\in \mathrm{Top}↔{K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
73 71 72 sylib ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
74 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left[{A},{B}\right]↔\left({x}\in ℝ\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
75 5 16 74 syl2anc ${⊢}{\phi }\to \left({x}\in \left[{A},{B}\right]↔\left({x}\in ℝ\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
76 75 biimpa ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to \left({x}\in ℝ\wedge {A}\le {x}\wedge {x}\le {B}\right)$
77 76 simp3d ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\le {B}$
78 77 3adant3 ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\wedge {y}\in {X}\right)\to {x}\le {B}$
79 78 iftrued ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\wedge {y}\in {X}\right)\to if\left({x}\le {B},{D},{E}\right)={D}$
80 79 mpoeq3dva ${⊢}{\phi }\to \left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)=\left({x}\in \left[{A},{B}\right],{y}\in {X}⟼{D}\right)$
81 80 10 eqeltrd ${⊢}{\phi }\to \left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)\in \left(\left({M}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
82 cnf2 ${⊢}\left({M}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{A},{B}\right]×{X}\right)\wedge {K}\in \mathrm{TopOn}\left(\bigcup {K}\right)\wedge \left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)\in \left(\left({M}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)\right)\to \left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{A},{B}\right]×{X}⟶\bigcup {K}$
83 69 73 81 82 syl3anc ${⊢}{\phi }\to \left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{A},{B}\right]×{X}⟶\bigcup {K}$
84 eqid ${⊢}\left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)=\left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)$
85 84 fmpo ${⊢}\forall {x}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}↔\left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{A},{B}\right]×{X}⟶\bigcup {K}$
86 83 85 sylibr ${⊢}{\phi }\to \forall {x}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}$
87 45 15 sstrd ${⊢}{\phi }\to \left[{B},{C}\right]\subseteq ℝ$
88 resttopon ${⊢}\left({R}\in \mathrm{TopOn}\left(ℝ\right)\wedge \left[{B},{C}\right]\subseteq ℝ\right)\to {R}{↾}_{𝑡}\left[{B},{C}\right]\in \mathrm{TopOn}\left(\left[{B},{C}\right]\right)$
89 55 87 88 sylancr ${⊢}{\phi }\to {R}{↾}_{𝑡}\left[{B},{C}\right]\in \mathrm{TopOn}\left(\left[{B},{C}\right]\right)$
90 3 89 eqeltrid ${⊢}{\phi }\to {N}\in \mathrm{TopOn}\left(\left[{B},{C}\right]\right)$
91 txtopon ${⊢}\left({N}\in \mathrm{TopOn}\left(\left[{B},{C}\right]\right)\wedge {J}\in \mathrm{TopOn}\left({X}\right)\right)\to {N}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{B},{C}\right]×{X}\right)$
92 90 8 91 syl2anc ${⊢}{\phi }\to {N}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{B},{C}\right]×{X}\right)$
93 elicc2 ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to \left({x}\in \left[{B},{C}\right]↔\left({x}\in ℝ\wedge {B}\le {x}\wedge {x}\le {C}\right)\right)$
94 16 6 93 syl2anc ${⊢}{\phi }\to \left({x}\in \left[{B},{C}\right]↔\left({x}\in ℝ\wedge {B}\le {x}\wedge {x}\le {C}\right)\right)$
95 94 biimpa ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\right)\to \left({x}\in ℝ\wedge {B}\le {x}\wedge {x}\le {C}\right)$
96 95 simp2d ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\right)\to {B}\le {x}$
97 96 biantrud ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\right)\to \left({x}\le {B}↔\left({x}\le {B}\wedge {B}\le {x}\right)\right)$
98 95 simp1d ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\right)\to {x}\in ℝ$
99 16 adantr ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\right)\to {B}\in ℝ$
100 98 99 letri3d ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\right)\to \left({x}={B}↔\left({x}\le {B}\wedge {B}\le {x}\right)\right)$
101 97 100 bitr4d ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\right)\to \left({x}\le {B}↔{x}={B}\right)$
102 101 3adant3 ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\wedge {y}\in {X}\right)\to \left({x}\le {B}↔{x}={B}\right)$
103 9 ancom2s ${⊢}\left({\phi }\wedge \left({y}\in {X}\wedge {x}={B}\right)\right)\to {D}={E}$
104 103 ifeq1d ${⊢}\left({\phi }\wedge \left({y}\in {X}\wedge {x}={B}\right)\right)\to if\left({x}\le {B},{D},{E}\right)=if\left({x}\le {B},{E},{E}\right)$
105 ifid ${⊢}if\left({x}\le {B},{E},{E}\right)={E}$
106 104 105 eqtrdi ${⊢}\left({\phi }\wedge \left({y}\in {X}\wedge {x}={B}\right)\right)\to if\left({x}\le {B},{D},{E}\right)={E}$
107 106 expr ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to \left({x}={B}\to if\left({x}\le {B},{D},{E}\right)={E}\right)$
108 107 3adant2 ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\wedge {y}\in {X}\right)\to \left({x}={B}\to if\left({x}\le {B},{D},{E}\right)={E}\right)$
109 102 108 sylbid ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\wedge {y}\in {X}\right)\to \left({x}\le {B}\to if\left({x}\le {B},{D},{E}\right)={E}\right)$
110 iffalse ${⊢}¬{x}\le {B}\to if\left({x}\le {B},{D},{E}\right)={E}$
111 109 110 pm2.61d1 ${⊢}\left({\phi }\wedge {x}\in \left[{B},{C}\right]\wedge {y}\in {X}\right)\to if\left({x}\le {B},{D},{E}\right)={E}$
112 111 mpoeq3dva ${⊢}{\phi }\to \left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)=\left({x}\in \left[{B},{C}\right],{y}\in {X}⟼{E}\right)$
113 112 11 eqeltrd ${⊢}{\phi }\to \left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)\in \left(\left({N}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$
114 cnf2 ${⊢}\left({N}{×}_{t}{J}\in \mathrm{TopOn}\left(\left[{B},{C}\right]×{X}\right)\wedge {K}\in \mathrm{TopOn}\left(\bigcup {K}\right)\wedge \left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)\in \left(\left({N}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)\right)\to \left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{B},{C}\right]×{X}⟶\bigcup {K}$
115 92 73 113 114 syl3anc ${⊢}{\phi }\to \left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{B},{C}\right]×{X}⟶\bigcup {K}$
116 eqid ${⊢}\left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)=\left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)$
117 116 fmpo ${⊢}\forall {x}\in \left[{B},{C}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}↔\left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{B},{C}\right]×{X}⟶\bigcup {K}$
118 115 117 sylibr ${⊢}{\phi }\to \forall {x}\in \left[{B},{C}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}$
119 ralun ${⊢}\left(\forall {x}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}\wedge \forall {x}\in \left[{B},{C}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}\right)\to \forall {x}\in \left(\left[{A},{B}\right]\cup \left[{B},{C}\right]\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}$
120 86 118 119 syl2anc ${⊢}{\phi }\to \forall {x}\in \left(\left[{A},{B}\right]\cup \left[{B},{C}\right]\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}$
121 23 raleqdv ${⊢}{\phi }\to \left(\forall {x}\in \left[{A},{C}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}↔\forall {x}\in \left(\left[{A},{B}\right]\cup \left[{B},{C}\right]\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}\right)$
122 120 121 mpbird ${⊢}{\phi }\to \forall {x}\in \left[{A},{C}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}$
123 eqid ${⊢}\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)=\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)$
124 123 fmpo ${⊢}\forall {x}\in \left[{A},{C}\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}if\left({x}\le {B},{D},{E}\right)\in \bigcup {K}↔\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{A},{C}\right]×{X}⟶\bigcup {K}$
125 122 124 sylib ${⊢}{\phi }\to \left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{A},{C}\right]×{X}⟶\bigcup {K}$
126 62 feq2d ${⊢}{\phi }\to \left(\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\left[{A},{C}\right]×{X}⟶\bigcup {K}↔\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\bigcup \left({O}{×}_{t}{J}\right)⟶\bigcup {K}\right)$
127 125 126 mpbid ${⊢}{\phi }\to \left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right):\bigcup \left({O}{×}_{t}{J}\right)⟶\bigcup {K}$
128 ssid ${⊢}{X}\subseteq {X}$
129 resmpo ${⊢}\left(\left[{A},{B}\right]\subseteq \left[{A},{C}\right]\wedge {X}\subseteq {X}\right)\to {\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)↾}_{\left(\left[{A},{B}\right]×{X}\right)}=\left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)$
130 24 128 129 sylancl ${⊢}{\phi }\to {\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)↾}_{\left(\left[{A},{B}\right]×{X}\right)}=\left({x}\in \left[{A},{B}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)$
131 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
132 1 131 eqeltri ${⊢}{R}\in \mathrm{Top}$
133 ovex ${⊢}\left[{A},{C}\right]\in \mathrm{V}$
134 resttop ${⊢}\left({R}\in \mathrm{Top}\wedge \left[{A},{C}\right]\in \mathrm{V}\right)\to {R}{↾}_{𝑡}\left[{A},{C}\right]\in \mathrm{Top}$
135 132 133 134 mp2an ${⊢}{R}{↾}_{𝑡}\left[{A},{C}\right]\in \mathrm{Top}$
136 4 135 eqeltri ${⊢}{O}\in \mathrm{Top}$
137 136 a1i ${⊢}{\phi }\to {O}\in \mathrm{Top}$
138 ovexd ${⊢}{\phi }\to \left[{A},{B}\right]\in \mathrm{V}$
139 txrest ${⊢}\left(\left({O}\in \mathrm{Top}\wedge {J}\in \mathrm{TopOn}\left({X}\right)\right)\wedge \left(\left[{A},{B}\right]\in \mathrm{V}\wedge {X}\in \mathrm{Clsd}\left({J}\right)\right)\right)\to \left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{A},{B}\right]×{X}\right)=\left({O}{↾}_{𝑡}\left[{A},{B}\right]\right){×}_{t}\left({J}{↾}_{𝑡}{X}\right)$
140 137 8 138 38 139 syl22anc ${⊢}{\phi }\to \left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{A},{B}\right]×{X}\right)=\left({O}{↾}_{𝑡}\left[{A},{B}\right]\right){×}_{t}\left({J}{↾}_{𝑡}{X}\right)$
141 132 a1i ${⊢}{\phi }\to {R}\in \mathrm{Top}$
142 ovexd ${⊢}{\phi }\to \left[{A},{C}\right]\in \mathrm{V}$
143 restabs ${⊢}\left({R}\in \mathrm{Top}\wedge \left[{A},{B}\right]\subseteq \left[{A},{C}\right]\wedge \left[{A},{C}\right]\in \mathrm{V}\right)\to \left({R}{↾}_{𝑡}\left[{A},{C}\right]\right){↾}_{𝑡}\left[{A},{B}\right]={R}{↾}_{𝑡}\left[{A},{B}\right]$
144 141 24 142 143 syl3anc ${⊢}{\phi }\to \left({R}{↾}_{𝑡}\left[{A},{C}\right]\right){↾}_{𝑡}\left[{A},{B}\right]={R}{↾}_{𝑡}\left[{A},{B}\right]$
145 4 oveq1i ${⊢}{O}{↾}_{𝑡}\left[{A},{B}\right]=\left({R}{↾}_{𝑡}\left[{A},{C}\right]\right){↾}_{𝑡}\left[{A},{B}\right]$
146 144 145 2 3eqtr4g ${⊢}{\phi }\to {O}{↾}_{𝑡}\left[{A},{B}\right]={M}$
147 33 oveq2d ${⊢}{\phi }\to {J}{↾}_{𝑡}{X}={J}{↾}_{𝑡}\bigcup {J}$
148 35 restid ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}{↾}_{𝑡}\bigcup {J}={J}$
149 8 148 syl ${⊢}{\phi }\to {J}{↾}_{𝑡}\bigcup {J}={J}$
150 147 149 eqtrd ${⊢}{\phi }\to {J}{↾}_{𝑡}{X}={J}$
151 146 150 oveq12d ${⊢}{\phi }\to \left({O}{↾}_{𝑡}\left[{A},{B}\right]\right){×}_{t}\left({J}{↾}_{𝑡}{X}\right)={M}{×}_{t}{J}$
152 140 151 eqtrd ${⊢}{\phi }\to \left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{A},{B}\right]×{X}\right)={M}{×}_{t}{J}$
153 152 oveq1d ${⊢}{\phi }\to \left(\left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{A},{B}\right]×{X}\right)\right)\mathrm{Cn}{K}=\left({M}{×}_{t}{J}\right)\mathrm{Cn}{K}$
154 81 130 153 3eltr4d ${⊢}{\phi }\to {\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)↾}_{\left(\left[{A},{B}\right]×{X}\right)}\in \left(\left(\left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{A},{B}\right]×{X}\right)\right)\mathrm{Cn}{K}\right)$
155 resmpo ${⊢}\left(\left[{B},{C}\right]\subseteq \left[{A},{C}\right]\wedge {X}\subseteq {X}\right)\to {\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)↾}_{\left(\left[{B},{C}\right]×{X}\right)}=\left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)$
156 45 128 155 sylancl ${⊢}{\phi }\to {\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)↾}_{\left(\left[{B},{C}\right]×{X}\right)}=\left({x}\in \left[{B},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)$
157 ovexd ${⊢}{\phi }\to \left[{B},{C}\right]\in \mathrm{V}$
158 txrest ${⊢}\left(\left({O}\in \mathrm{Top}\wedge {J}\in \mathrm{TopOn}\left({X}\right)\right)\wedge \left(\left[{B},{C}\right]\in \mathrm{V}\wedge {X}\in \mathrm{Clsd}\left({J}\right)\right)\right)\to \left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{B},{C}\right]×{X}\right)=\left({O}{↾}_{𝑡}\left[{B},{C}\right]\right){×}_{t}\left({J}{↾}_{𝑡}{X}\right)$
159 137 8 157 38 158 syl22anc ${⊢}{\phi }\to \left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{B},{C}\right]×{X}\right)=\left({O}{↾}_{𝑡}\left[{B},{C}\right]\right){×}_{t}\left({J}{↾}_{𝑡}{X}\right)$
160 restabs ${⊢}\left({R}\in \mathrm{Top}\wedge \left[{B},{C}\right]\subseteq \left[{A},{C}\right]\wedge \left[{A},{C}\right]\in \mathrm{V}\right)\to \left({R}{↾}_{𝑡}\left[{A},{C}\right]\right){↾}_{𝑡}\left[{B},{C}\right]={R}{↾}_{𝑡}\left[{B},{C}\right]$
161 141 45 142 160 syl3anc ${⊢}{\phi }\to \left({R}{↾}_{𝑡}\left[{A},{C}\right]\right){↾}_{𝑡}\left[{B},{C}\right]={R}{↾}_{𝑡}\left[{B},{C}\right]$
162 4 oveq1i ${⊢}{O}{↾}_{𝑡}\left[{B},{C}\right]=\left({R}{↾}_{𝑡}\left[{A},{C}\right]\right){↾}_{𝑡}\left[{B},{C}\right]$
163 161 162 3 3eqtr4g ${⊢}{\phi }\to {O}{↾}_{𝑡}\left[{B},{C}\right]={N}$
164 163 150 oveq12d ${⊢}{\phi }\to \left({O}{↾}_{𝑡}\left[{B},{C}\right]\right){×}_{t}\left({J}{↾}_{𝑡}{X}\right)={N}{×}_{t}{J}$
165 159 164 eqtrd ${⊢}{\phi }\to \left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{B},{C}\right]×{X}\right)={N}{×}_{t}{J}$
166 165 oveq1d ${⊢}{\phi }\to \left(\left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{B},{C}\right]×{X}\right)\right)\mathrm{Cn}{K}=\left({N}{×}_{t}{J}\right)\mathrm{Cn}{K}$
167 113 156 166 3eltr4d ${⊢}{\phi }\to {\left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)↾}_{\left(\left[{B},{C}\right]×{X}\right)}\in \left(\left(\left({O}{×}_{t}{J}\right){↾}_{𝑡}\left(\left[{B},{C}\right]×{X}\right)\right)\mathrm{Cn}{K}\right)$
168 12 13 40 50 63 127 154 167 paste ${⊢}{\phi }\to \left({x}\in \left[{A},{C}\right],{y}\in {X}⟼if\left({x}\le {B},{D},{E}\right)\right)\in \left(\left({O}{×}_{t}{J}\right)\mathrm{Cn}{K}\right)$