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 ↾_{𝑡} [A, B]$
	cnmpopc.n	$⊢ N = R ↾_{𝑡} [B, C]$
	cnmpopc.o	$⊢ O = R ↾_{𝑡} [A, C]$
	cnmpopc.a	$⊢ φ \to A \in ℝ$
	cnmpopc.c	$⊢ φ \to C \in ℝ$
	cnmpopc.b	$⊢ φ \to B \in [A, C]$
	cnmpopc.j	$⊢ φ \to J \in TopOn (X)$
	cnmpopc.q	$⊢ (φ \land (x = B \land y \in X)) \to D = E$
	cnmpopc.d	$⊢ φ \to (x \in [A, B], y \in X ⟼ D) \in ((M \times_{t} J) Cn K)$
	cnmpopc.e	$⊢ φ \to (x \in [B, C], y \in X ⟼ E) \in ((N \times_{t} J) Cn K)$
Assertion	cnmpopc	$⊢ φ \to (x \in [A, C], y \in X ⟼ if (x \leq B, D, E)) \in ((O \times_{t} J) Cn K)$

Proof

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

Metamath Proof Explorer

Theorem cnmpopc

Proof