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	120 23	raleqtrrdv	\|- ( ph -> A. x e. ( A [,] C ) A. y e. X if ( x <_ B , D , E ) e. U. K )
122		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 ) )
123	122	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 )
124	121 123	sylib	\|- ( ph -> ( x e. ( A [,] C ) , y e. X \|-> if ( x <_ B , D , E ) ) : ( ( A [,] C ) X. X ) --> U. K )
125	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 ) )
126	124 125	mpbid	\|- ( ph -> ( x e. ( A [,] C ) , y e. X \|-> if ( x <_ B , D , E ) ) : U. ( O tX J ) --> U. K )
127		ssid	\|- X C_ X
128		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 ) ) )
129	24 127 128	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 ) ) )
130		retop	\|- ( topGen ` ran (,) ) e. Top
131	1 130	eqeltri	\|- R e. Top
132		ovex	\|- ( A [,] C ) e. _V
133		resttop	\|- ( ( R e. Top /\ ( A [,] C ) e. _V ) -> ( R \|`t ( A [,] C ) ) e. Top )
134	131 132 133	mp2an	\|- ( R \|`t ( A [,] C ) ) e. Top
135	4 134	eqeltri	\|- O e. Top
136	135	a1i	\|- ( ph -> O e. Top )
137		ovexd	\|- ( ph -> ( A [,] B ) e. _V )
138		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 ) ) )
139	136 8 137 38 138	syl22anc	\|- ( ph -> ( ( O tX J ) \|`t ( ( A [,] B ) X. X ) ) = ( ( O \|`t ( A [,] B ) ) tX ( J \|`t X ) ) )
140	131	a1i	\|- ( ph -> R e. Top )
141		ovexd	\|- ( ph -> ( A [,] C ) e. _V )
142		restabs	\|- ( ( R e. Top /\ ( A [,] B ) C_ ( A [,] C ) /\ ( A [,] C ) e. _V ) -> ( ( R \|`t ( A [,] C ) ) \|`t ( A [,] B ) ) = ( R \|`t ( A [,] B ) ) )
143	140 24 141 142	syl3anc	\|- ( ph -> ( ( R \|`t ( A [,] C ) ) \|`t ( A [,] B ) ) = ( R \|`t ( A [,] B ) ) )
144	4	oveq1i	\|- ( O \|`t ( A [,] B ) ) = ( ( R \|`t ( A [,] C ) ) \|`t ( A [,] B ) )
145	143 144 2	3eqtr4g	\|- ( ph -> ( O \|`t ( A [,] B ) ) = M )
146	33	oveq2d	\|- ( ph -> ( J \|`t X ) = ( J \|`t U. J ) )
147	35	restid	\|- ( J e. ( TopOn ` X ) -> ( J \|`t U. J ) = J )
148	8 147	syl	\|- ( ph -> ( J \|`t U. J ) = J )
149	146 148	eqtrd	\|- ( ph -> ( J \|`t X ) = J )
150	145 149	oveq12d	\|- ( ph -> ( ( O \|`t ( A [,] B ) ) tX ( J \|`t X ) ) = ( M tX J ) )
151	139 150	eqtrd	\|- ( ph -> ( ( O tX J ) \|`t ( ( A [,] B ) X. X ) ) = ( M tX J ) )
152	151	oveq1d	\|- ( ph -> ( ( ( O tX J ) \|`t ( ( A [,] B ) X. X ) ) Cn K ) = ( ( M tX J ) Cn K ) )
153	81 129 152	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 ) )
154		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 ) ) )
155	45 127 154	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 ) ) )
156		ovexd	\|- ( ph -> ( B [,] C ) e. _V )
157		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 ) ) )
158	136 8 156 38 157	syl22anc	\|- ( ph -> ( ( O tX J ) \|`t ( ( B [,] C ) X. X ) ) = ( ( O \|`t ( B [,] C ) ) tX ( J \|`t X ) ) )
159		restabs	\|- ( ( R e. Top /\ ( B [,] C ) C_ ( A [,] C ) /\ ( A [,] C ) e. _V ) -> ( ( R \|`t ( A [,] C ) ) \|`t ( B [,] C ) ) = ( R \|`t ( B [,] C ) ) )
160	140 45 141 159	syl3anc	\|- ( ph -> ( ( R \|`t ( A [,] C ) ) \|`t ( B [,] C ) ) = ( R \|`t ( B [,] C ) ) )
161	4	oveq1i	\|- ( O \|`t ( B [,] C ) ) = ( ( R \|`t ( A [,] C ) ) \|`t ( B [,] C ) )
162	160 161 3	3eqtr4g	\|- ( ph -> ( O \|`t ( B [,] C ) ) = N )
163	162 149	oveq12d	\|- ( ph -> ( ( O \|`t ( B [,] C ) ) tX ( J \|`t X ) ) = ( N tX J ) )
164	158 163	eqtrd	\|- ( ph -> ( ( O tX J ) \|`t ( ( B [,] C ) X. X ) ) = ( N tX J ) )
165	164	oveq1d	\|- ( ph -> ( ( ( O tX J ) \|`t ( ( B [,] C ) X. X ) ) Cn K ) = ( ( N tX J ) Cn K ) )
166	113 155 165	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 ) )
167	12 13 40 50 63 126 153 166	paste	\|- ( ph -> ( x e. ( A [,] C ) , y e. X \|-> if ( x <_ B , D , E ) ) e. ( ( O tX J ) Cn K ) )

Metamath Proof Explorer

Theorem cnmpopc

Proof