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 = ( topGen ` ran (,) )
cnmpopc.m 
|- M = ( R |`t ( A [,] B ) )
cnmpopc.n 
|- N = ( R |`t ( B [,] C ) )
cnmpopc.o 
|- O = ( R |`t ( A [,] C ) )
cnmpopc.a 
|- ( ph -> A e. RR )
cnmpopc.c 
|- ( ph -> C e. RR )
cnmpopc.b 
|- ( ph -> B e. ( A [,] C ) )
cnmpopc.j 
|- ( ph -> J e. ( TopOn ` X ) )
cnmpopc.q 
|- ( ( ph /\ ( x = B /\ y e. X ) ) -> D = E )
cnmpopc.d 
|- ( ph -> ( x e. ( A [,] B ) , y e. X |-> D ) e. ( ( M tX J ) Cn K ) )
cnmpopc.e 
|- ( ph -> ( x e. ( B [,] C ) , y e. X |-> E ) e. ( ( N tX J ) Cn K ) )
Assertion cnmpopc 
|- ( ph -> ( x e. ( A [,] C ) , y e. X |-> if ( x <_ B , D , E ) ) e. ( ( O tX J ) Cn K ) )

Proof

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