Theorem piececn 15894

Description: Piecewise definition of a continuous function on a real interval.

Hypotheses

Ref	Expression
piececn.1	|- A e. RR
piececn.2	|- B e. RR
piececn.3	|- C e. (A[,]B)
piececn.4	|- R e. _V
piececn.5	|- S e. _V
piececn.6	|- F = {<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))}
piececn.7	|- J = (subSp` <.(A[,]B), (topGen` ran (,))>.)
piececn.8	|- K = (subSp` <.(A[,]C), (topGen` ran (,))>.)
piececn.9	|- L = (subSp` <.(C[,]B), (topGen` ran (,))>.)
piececn.10	|- (x = C -> R = S)
piececn.11	|- G = {<.x, y>. | (x e. (A[,]C) /\ y = R)}
piececn.12	|- H = {<.x, y>. | (x e. (C[,]B) /\ y = S)}
piececn.13	|- M e. Top
piececn.14	|- G e. (K Cn M)
piececn.15	|- H e. (L Cn M)

Assertion

Ref	Expression
piececn	|- F e. (J Cn M)

Distinct variable groups:   x,A,y   x,B,y   x,C,y   y,R   y,S   x,J,y   x,K,y   x,L,y   x,M,y

Proof of Theorem piececn

Step	Hyp	Ref	Expression
1		piececn.7	. . . 4 |- J = (subSp` <.(A[,]B), (topGen` ran (,))>.)
2		retop 8926	. . . . 5 |- (topGen` ran (,)) e. Top
3		piececn.1	. . . . . . 7 |- A e. RR
4		piececn.2	. . . . . . 7 |- B e. RR
5		iccssre 7565	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A[,]B) C_ RR)
6	3, 4, 5	mp2an 761	. . . . . 6 |- (A[,]B) C_ RR
7		uniretop 8927	. . . . . 6 |- U.(topGen` ran (,)) = RR
8	6, 7	sseqtr4i 2650	. . . . 5 |- (A[,]B) C_ U.(topGen` ran (,))
9		stoig3 10253	. . . . 5 |- (((topGen` ran (,)) e. Top /\ (A[,]B) C_ U.(topGen` ran (,))) -> (subSp` <.(A[,]B), (topGen` ran (,))>.) e. Top)
10	2, 8, 9	mp2an 761	. . . 4 |- (subSp` <.(A[,]B), (topGen` ran (,))>.) e. Top
11	1, 10	eqeltri 1967	. . 3 |- J e. Top
12		piececn.13	. . 3 |- M e. Top
13	11, 12	pm3.2i 307	. 2 |- (J e. Top /\ M e. Top)
14		piececn.3	. . . . . . 7 |- C e. (A[,]B)
15	6, 14	sselii 2618	. . . . . 6 |- C e. RR
16		clint3 10184	. . . . . 6 |- ((A e. RR /\ C e. RR) -> (A[,]C) e. (Clsd` (topGen` ran (,))))
17	3, 15, 16	mp2an 761	. . . . 5 |- (A[,]C) e. (Clsd` (topGen` ran (,)))
18	3, 4	pm3.2i 307	. . . . . 6 |- (A e. RR /\ B e. RR)
19	3, 15	pm3.2i 307	. . . . . 6 |- (A e. RR /\ C e. RR)
20	3	leidi 6790	. . . . . . 7 |- A <_ A
21		elicc2 7560	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B)))
22	3, 4, 21	mp2an 761	. . . . . . . . 9 |- (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B))
23	14, 22	mpbi 206	. . . . . . . 8 |- (C e. RR /\ A <_ C /\ C <_ B)
24	23	simp3i 887	. . . . . . 7 |- C <_ B
25	20, 24	pm3.2i 307	. . . . . 6 |- (A <_ A /\ C <_ B)
26		iccss 15855	. . . . . 6 |- (((A e. RR /\ B e. RR) /\ (A e. RR /\ C e. RR) /\ (A <_ A /\ C <_ B)) -> (A[,]C) C_ (A[,]B))
27	18, 19, 25, 26	mp3an 1191	. . . . 5 |- (A[,]C) C_ (A[,]B)
28	7	eqcomi 1888	. . . . . 6 |- RR = U.(topGen` ran (,))
29	28	subspcld 15838	. . . . 5 |- ((((topGen` ran (,)) e. Top /\ (A[,]B) C_ RR) /\ ((A[,]C) e. (Clsd` (topGen` ran (,))) /\ (A[,]C) C_ (A[,]B))) -> (A[,]C) e. (Clsd` (subSp` <.(A[,]B), (topGen` ran (,))>.)))
30	2, 6, 17, 27, 29	mp4an 15651	. . . 4 |- (A[,]C) e. (Clsd` (subSp` <.(A[,]B), (topGen` ran (,))>.))
31	1	fveq2i 4684	. . . 4 |- (Clsd` J) = (Clsd` (subSp` <.(A[,]B), (topGen` ran (,))>.))
32	30, 31	eleqtrri 1970	. . 3 |- (A[,]C) e. (Clsd` J)
33		clint3 10184	. . . . . 6 |- ((C e. RR /\ B e. RR) -> (C[,]B) e. (Clsd` (topGen` ran (,))))
34	15, 4, 33	mp2an 761	. . . . 5 |- (C[,]B) e. (Clsd` (topGen` ran (,)))
35	15, 4	pm3.2i 307	. . . . . 6 |- (C e. RR /\ B e. RR)
36	23	simp2i 886	. . . . . . 7 |- A <_ C
37	4	leidi 6790	. . . . . . 7 |- B <_ B
38	36, 37	pm3.2i 307	. . . . . 6 |- (A <_ C /\ B <_ B)
39		iccss 15855	. . . . . 6 |- (((A e. RR /\ B e. RR) /\ (C e. RR /\ B e. RR) /\ (A <_ C /\ B <_ B)) -> (C[,]B) C_ (A[,]B))
40	18, 35, 38, 39	mp3an 1191	. . . . 5 |- (C[,]B) C_ (A[,]B)
41	28	subspcld 15838	. . . . 5 |- ((((topGen` ran (,)) e. Top /\ (A[,]B) C_ RR) /\ ((C[,]B) e. (Clsd` (topGen` ran (,))) /\ (C[,]B) C_ (A[,]B))) -> (C[,]B) e. (Clsd` (subSp` <.(A[,]B), (topGen` ran (,))>.)))
42	2, 6, 34, 40, 41	mp4an 15651	. . . 4 |- (C[,]B) e. (Clsd` (subSp` <.(A[,]B), (topGen` ran (,))>.))
43	42, 31	eleqtrri 1970	. . 3 |- (C[,]B) e. (Clsd` J)
44		iccsplit 15854	. . . . 5 |- ((A e. RR /\ B e. RR /\ C e. (A[,]B)) -> (A[,]B) = ((A[,]C) u. (C[,]B)))
45	3, 4, 14, 44	mp3an 1191	. . . 4 |- (A[,]B) = ((A[,]C) u. (C[,]B))
46	45	eqcomi 1888	. . 3 |- ((A[,]C) u. (C[,]B)) = (A[,]B)
47	32, 43, 46	3pm3.2i 1048	. 2 |- ((A[,]C) e. (Clsd` J) /\ (C[,]B) e. (Clsd` J) /\ ((A[,]C) u. (C[,]B)) = (A[,]B))
48		piececn.6	. . . 4 |- F = {<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))}
49	45	eleq2i 1961	. . . . . 6 |- (x e. (A[,]B) <-> x e. ((A[,]C) u. (C[,]B)))
50		elun 2741	. . . . . 6 |- (x e. ((A[,]C) u. (C[,]B)) <-> (x e. (A[,]C) \/ x e. (C[,]B)))
51	49, 50	bitri 190	. . . . 5 |- (x e. (A[,]B) <-> (x e. (A[,]C) \/ x e. (C[,]B)))
52		elicc2 7560	. . . . . . . . . . 11 |- ((A e. RR /\ C e. RR) -> (x e. (A[,]C) <-> (x e. RR /\ A <_ x /\ x <_ C)))
53	3, 15, 52	mp2an 761	. . . . . . . . . 10 |- (x e. (A[,]C) <-> (x e. RR /\ A <_ x /\ x <_ C))
54	53	simp3bi 893	. . . . . . . . 9 |- (x e. (A[,]C) -> x <_ C)
55		iftrue 2989	. . . . . . . . 9 |- (x <_ C -> if(x <_ C, R, S) = R)
56	54, 55	syl 12	. . . . . . . 8 |- (x e. (A[,]C) -> if(x <_ C, R, S) = R)
57		piececn.4	. . . . . . . . . 10 |- R e. _V
58		fvopab2 4754	. . . . . . . . . 10 |- ((x e. (A[,]C) /\ R e. _V) -> ({<.x, y>. | (x e. (A[,]C) /\ y = R)}` x) = R)
59	57, 58	mpan2 760	. . . . . . . . 9 |- (x e. (A[,]C) -> ({<.x, y>. | (x e. (A[,]C) /\ y = R)}` x) = R)
60		piececn.11	. . . . . . . . . 10 |- G = {<.x, y>. | (x e. (A[,]C) /\ y = R)}
61	60	fveq1i 4682	. . . . . . . . 9 |- (G` x) = ({<.x, y>. | (x e. (A[,]C) /\ y = R)}` x)
62	59, 61	syl5eq 1940	. . . . . . . 8 |- (x e. (A[,]C) -> (G` x) = R)
63	56, 62	eqtr4d 1928	. . . . . . 7 |- (x e. (A[,]C) -> if(x <_ C, R, S) = (G` x))
64		piececn.8	. . . . . . . . . 10 |- K = (subSp` <.(A[,]C), (topGen` ran (,))>.)
65		iccssre 7565	. . . . . . . . . . . . 13 |- ((A e. RR /\ C e. RR) -> (A[,]C) C_ RR)
66	3, 15, 65	mp2an 761	. . . . . . . . . . . 12 |- (A[,]C) C_ RR
67	66, 7	sseqtr4i 2650	. . . . . . . . . . 11 |- (A[,]C) C_ U.(topGen` ran (,))
68		stoig3 10253	. . . . . . . . . . 11 |- (((topGen` ran (,)) e. Top /\ (A[,]C) C_ U.(topGen` ran (,))) -> (subSp` <.(A[,]C), (topGen` ran (,))>.) e. Top)
69	2, 67, 68	mp2an 761	. . . . . . . . . 10 |- (subSp` <.(A[,]C), (topGen` ran (,))>.) e. Top
70	64, 69	eqeltri 1967	. . . . . . . . 9 |- K e. Top
71		piececn.14	. . . . . . . . 9 |- G e. (K Cn M)
72	64	unieqi 3187	. . . . . . . . . . 11 |- U.K = U.(subSp` <.(A[,]C), (topGen` ran (,))>.)
73		stoig2 10252	. . . . . . . . . . . 12 |- (((topGen` ran (,)) e. Top /\ (A[,]C) C_ U.(topGen` ran (,))) -> U.(subSp` <.(A[,]C), (topGen` ran (,))>.) = (A[,]C))
74	2, 67, 73	mp2an 761	. . . . . . . . . . 11 |- U.(subSp` <.(A[,]C), (topGen` ran (,))>.) = (A[,]C)
75	72, 74	eqtr2i 1909	. . . . . . . . . 10 |- (A[,]C) = U.K
76		eqid 1884	. . . . . . . . . 10 |- U.M = U.M
77	75, 76	cnf 9038	. . . . . . . . 9 |- ((K e. Top /\ M e. Top /\ G e. (K Cn M)) -> G:(A[,]C)-->U.M)
78	70, 12, 71, 77	mp3an 1191	. . . . . . . 8 |- G:(A[,]C)-->U.M
79	78	ffvelrni 4788	. . . . . . 7 |- (x e. (A[,]C) -> (G` x) e. U.M)
80	63, 79	eqeltrd 1971	. . . . . 6 |- (x e. (A[,]C) -> if(x <_ C, R, S) e. U.M)
81		elicc2 7560	. . . . . . . . . 10 |- ((C e. RR /\ B e. RR) -> (x e. (C[,]B) <-> (x e. RR /\ C <_ x /\ x <_ B)))
82	15, 4, 81	mp2an 761	. . . . . . . . 9 |- (x e. (C[,]B) <-> (x e. RR /\ C <_ x /\ x <_ B))
83		leloe 6688	. . . . . . . . . . . . 13 |- ((C e. RR /\ x e. RR) -> (C <_ x <-> (C < x \/ C = x)))
84	15, 83	mpan 759	. . . . . . . . . . . 12 |- (x e. RR -> (C <_ x <-> (C < x \/ C = x)))
85	84	biimpa 460	. . . . . . . . . . 11 |- ((x e. RR /\ C <_ x) -> (C < x \/ C = x))
86		ltnle 6680	. . . . . . . . . . . . . . 15 |- ((C e. RR /\ x e. RR) -> (C < x <-> -. x <_ C))
87	15, 86	mpan 759	. . . . . . . . . . . . . 14 |- (x e. RR -> (C < x <-> -. x <_ C))
88	87	biimpa 460	. . . . . . . . . . . . 13 |- ((x e. RR /\ C < x) -> -. x <_ C)
89		iffalse 2991	. . . . . . . . . . . . 13 |- (-. x <_ C -> if(x <_ C, R, S) = S)
90	88, 89	syl 12	. . . . . . . . . . . 12 |- ((x e. RR /\ C < x) -> if(x <_ C, R, S) = S)
91	15	leidi 6790	. . . . . . . . . . . . . . . . 17 |- C <_ C
92		breq1 3341	. . . . . . . . . . . . . . . . 17 |- (x = C -> (x <_ C <-> C <_ C))
93	91, 92	mpbiri 211	. . . . . . . . . . . . . . . 16 |- (x = C -> x <_ C)
94	93, 55	syl 12	. . . . . . . . . . . . . . 15 |- (x = C -> if(x <_ C, R, S) = R)
95		piececn.10	. . . . . . . . . . . . . . 15 |- (x = C -> R = S)
96	94, 95	eqtrd 1925	. . . . . . . . . . . . . 14 |- (x = C -> if(x <_ C, R, S) = S)
97	96	eqcoms 1887	. . . . . . . . . . . . 13 |- (C = x -> if(x <_ C, R, S) = S)
98	97	adantl 424	. . . . . . . . . . . 12 |- ((x e. RR /\ C = x) -> if(x <_ C, R, S) = S)
99	90, 98	jaodan 471	. . . . . . . . . . 11 |- ((x e. RR /\ (C < x \/ C = x)) -> if(x <_ C, R, S) = S)
100	85, 99	syldan 516	. . . . . . . . . 10 |- ((x e. RR /\ C <_ x) -> if(x <_ C, R, S) = S)
101	100	3adant3 896	. . . . . . . . 9 |- ((x e. RR /\ C <_ x /\ x <_ B) -> if(x <_ C, R, S) = S)
102	82, 101	sylbi 216	. . . . . . . 8 |- (x e. (C[,]B) -> if(x <_ C, R, S) = S)
103		piececn.5	. . . . . . . . . 10 |- S e. _V
104		fvopab2 4754	. . . . . . . . . 10 |- ((x e. (C[,]B) /\ S e. _V) -> ({<.x, y>. | (x e. (C[,]B) /\ y = S)}` x) = S)
105	103, 104	mpan2 760	. . . . . . . . 9 |- (x e. (C[,]B) -> ({<.x, y>. | (x e. (C[,]B) /\ y = S)}` x) = S)
106		piececn.12	. . . . . . . . . 10 |- H = {<.x, y>. | (x e. (C[,]B) /\ y = S)}
107	106	fveq1i 4682	. . . . . . . . 9 |- (H` x) = ({<.x, y>. | (x e. (C[,]B) /\ y = S)}` x)
108	105, 107	syl5eq 1940	. . . . . . . 8 |- (x e. (C[,]B) -> (H` x) = S)
109	102, 108	eqtr4d 1928	. . . . . . 7 |- (x e. (C[,]B) -> if(x <_ C, R, S) = (H` x))
110		piececn.9	. . . . . . . . . 10 |- L = (subSp` <.(C[,]B), (topGen` ran (,))>.)
111		iccssre 7565	. . . . . . . . . . . . 13 |- ((C e. RR /\ B e. RR) -> (C[,]B) C_ RR)
112	15, 4, 111	mp2an 761	. . . . . . . . . . . 12 |- (C[,]B) C_ RR
113	112, 7	sseqtr4i 2650	. . . . . . . . . . 11 |- (C[,]B) C_ U.(topGen` ran (,))
114		stoig3 10253	. . . . . . . . . . 11 |- (((topGen` ran (,)) e. Top /\ (C[,]B) C_ U.(topGen` ran (,))) -> (subSp` <.(C[,]B), (topGen` ran (,))>.) e. Top)
115	2, 113, 114	mp2an 761	. . . . . . . . . 10 |- (subSp` <.(C[,]B), (topGen` ran (,))>.) e. Top
116	110, 115	eqeltri 1967	. . . . . . . . 9 |- L e. Top
117		piececn.15	. . . . . . . . 9 |- H e. (L Cn M)
118	110	unieqi 3187	. . . . . . . . . . 11 |- U.L = U.(subSp` <.(C[,]B), (topGen` ran (,))>.)
119		stoig2 10252	. . . . . . . . . . . 12 |- (((topGen` ran (,)) e. Top /\ (C[,]B) C_ U.(topGen` ran (,))) -> U.(subSp` <.(C[,]B), (topGen` ran (,))>.) = (C[,]B))
120	2, 113, 119	mp2an 761	. . . . . . . . . . 11 |- U.(subSp` <.(C[,]B), (topGen` ran (,))>.) = (C[,]B)
121	118, 120	eqtr2i 1909	. . . . . . . . . 10 |- (C[,]B) = U.L
122	121, 76	cnf 9038	. . . . . . . . 9 |- ((L e. Top /\ M e. Top /\ H e. (L Cn M)) -> H:(C[,]B)-->U.M)
123	116, 12, 117, 122	mp3an 1191	. . . . . . . 8 |- H:(C[,]B)-->U.M
124	123	ffvelrni 4788	. . . . . . 7 |- (x e. (C[,]B) -> (H` x) e. U.M)
125	109, 124	eqeltrd 1971	. . . . . 6 |- (x e. (C[,]B) -> if(x <_ C, R, S) e. U.M)
126	80, 125	jaoi 368	. . . . 5 |- ((x e. (A[,]C) \/ x e. (C[,]B)) -> if(x <_ C, R, S) e. U.M)
127	51, 126	sylbi 216	. . . 4 |- (x e. (A[,]B) -> if(x <_ C, R, S) e. U.M)
128	48, 127	fopab 4800	. . 3 |- F:(A[,]B)-->U.M
129		reseq1 4218	. . . . . . 7 |- (F = {<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} -> (F |` (A[,]C)) = ({<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} |` (A[,]C)))
130	48, 129	ax-mp 7	. . . . . 6 |- (F |` (A[,]C)) = ({<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} |` (A[,]C))
131		resopab2 4256	. . . . . . 7 |- ((A[,]C) C_ (A[,]B) -> ({<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} |` (A[,]C)) = {<.x, y>. | (x e. (A[,]C) /\ y = if(x <_ C, R, S))})
132	27, 131	ax-mp 7	. . . . . 6 |- ({<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} |` (A[,]C)) = {<.x, y>. | (x e. (A[,]C) /\ y = if(x <_ C, R, S))}
133	56	eqeq2d 1895	. . . . . . . 8 |- (x e. (A[,]C) -> (y = if(x <_ C, R, S) <-> y = R))
134	133	pm5.32i 707	. . . . . . 7 |- ((x e. (A[,]C) /\ y = if(x <_ C, R, S)) <-> (x e. (A[,]C) /\ y = R))
135	134	opabbii 3402	. . . . . 6 |- {<.x, y>. | (x e. (A[,]C) /\ y = if(x <_ C, R, S))} = {<.x, y>. | (x e. (A[,]C) /\ y = R)}
136	130, 132, 135	3eqtri 1912	. . . . 5 |- (F |` (A[,]C)) = {<.x, y>. | (x e. (A[,]C) /\ y = R)}
137	136, 60	eqtr4i 1911	. . . 4 |- (F |` (A[,]C)) = G
138	28	subspabs 15840	. . . . . . . 8 |- (((topGen` ran (,)) e. Top /\ (A[,]B) C_ RR /\ (A[,]C) C_ (A[,]B)) -> (subSp` <.(A[,]C), (subSp` <.(A[,]B), (topGen` ran (,))>.)>.) = (subSp` <.(A[,]C), (topGen` ran (,))>.))
139	2, 6, 27, 138	mp3an 1191	. . . . . . 7 |- (subSp` <.(A[,]C), (subSp` <.(A[,]B), (topGen` ran (,))>.)>.) = (subSp` <.(A[,]C), (topGen` ran (,))>.)
140	1	opeq2i 3162	. . . . . . . 8 |- <.(A[,]C), J>. = <.(A[,]C), (subSp` <.(A[,]B), (topGen` ran (,))>.)>.
141	140	fveq2i 4684	. . . . . . 7 |- (subSp` <.(A[,]C), J>.) = (subSp` <.(A[,]C), (subSp` <.(A[,]B), (topGen` ran (,))>.)>.)
142	139, 141, 64	3eqtr4i 1921	. . . . . 6 |- (subSp` <.(A[,]C), J>.) = K
143	142	opreq1i 4892	. . . . 5 |- ((subSp` <.(A[,]C), J>.) Cn M) = (K Cn M)
144	71, 143	eleqtrri 1970	. . . 4 |- G e. ((subSp` <.(A[,]C), J>.) Cn M)
145	137, 144	eqeltri 1967	. . 3 |- (F |` (A[,]C)) e. ((subSp` <.(A[,]C), J>.) Cn M)
146		reseq1 4218	. . . . . . 7 |- (F = {<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} -> (F |` (C[,]B)) = ({<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} |` (C[,]B)))
147	48, 146	ax-mp 7	. . . . . 6 |- (F |` (C[,]B)) = ({<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} |` (C[,]B))
148		resopab2 4256	. . . . . . 7 |- ((C[,]B) C_ (A[,]B) -> ({<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} |` (C[,]B)) = {<.x, y>. | (x e. (C[,]B) /\ y = if(x <_ C, R, S))})
149	40, 148	ax-mp 7	. . . . . 6 |- ({<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))} |` (C[,]B)) = {<.x, y>. | (x e. (C[,]B) /\ y = if(x <_ C, R, S))}
150	102	eqeq2d 1895	. . . . . . . 8 |- (x e. (C[,]B) -> (y = if(x <_ C, R, S) <-> y = S))
151	150	pm5.32i 707	. . . . . . 7 |- ((x e. (C[,]B) /\ y = if(x <_ C, R, S)) <-> (x e. (C[,]B) /\ y = S))
152	151	opabbii 3402	. . . . . 6 |- {<.x, y>. | (x e. (C[,]B) /\ y = if(x <_ C, R, S))} = {<.x, y>. | (x e. (C[,]B) /\ y = S)}
153	147, 149, 152	3eqtri 1912	. . . . 5 |- (F |` (C[,]B)) = {<.x, y>. | (x e. (C[,]B) /\ y = S)}
154	153, 106	eqtr4i 1911	. . . 4 |- (F |` (C[,]B)) = H
155	28	subspabs 15840	. . . . . . . 8 |- (((topGen` ran (,)) e. Top /\ (A[,]B) C_ RR /\ (C[,]B) C_ (A[,]B)) -> (subSp` <.(C[,]B), (subSp` <.(A[,]B), (topGen` ran (,))>.)>.) = (subSp` <.(C[,]B), (topGen` ran (,))>.))
156	2, 6, 40, 155	mp3an 1191	. . . . . . 7 |- (subSp` <.(C[,]B), (subSp` <.(A[,]B), (topGen` ran (,))>.)>.) = (subSp` <.(C[,]B), (topGen` ran (,))>.)
157	1	opeq2i 3162	. . . . . . . 8 |- <.(C[,]B), J>. = <.(C[,]B), (subSp` <.(A[,]B), (topGen` ran (,))>.)>.
158	157	fveq2i 4684	. . . . . . 7 |- (subSp` <.(C[,]B), J>.) = (subSp` <.(C[,]B), (subSp` <.(A[,]B), (topGen` ran (,))>.)>.)
159	156, 158, 110	3eqtr4i 1921	. . . . . 6 |- (subSp` <.(C[,]B), J>.) = L
160	159	opreq1i 4892	. . . . 5 |- ((subSp` <.(C[,]B), J>.) Cn M) = (L Cn M)
161	117, 160	eleqtrri 1970	. . . 4 |- H e. ((subSp` <.(C[,]B), J>.) Cn M)
162	154, 161	eqeltri 1967	. . 3 |- (F |` (C[,]B)) e. ((subSp` <.(C[,]B), J>.) Cn M)
163	128, 145, 162	3pm3.2i 1048	. 2 |- (F:(A[,]B)-->U.M /\ (F |` (A[,]C)) e. ((subSp` <.(A[,]C), J>.) Cn M) /\ (F |` (C[,]B)) e. ((subSp` <.(C[,]B), J>.) Cn M))
164	1	unieqi 3187	. . . 4 |- U.J = U.(subSp` <.(A[,]B), (topGen` ran (,))>.)
165		stoig2 10252	. . . . 5 |- (((topGen` ran (,)) e. Top /\ (A[,]B) C_ U.(topGen` ran (,))) -> U.(subSp` <.(A[,]B), (topGen` ran (,))>.) = (A[,]B))
166	2, 8, 165	mp2an 761	. . . 4 |- U.(subSp` <.(A[,]B), (topGen` ran (,))>.) = (A[,]B)
167	164, 166	eqtr2i 1909	. . 3 |- (A[,]B) = U.J
168	167, 76	paste 15893	. 2 |- (((J e. Top /\ M e. Top) /\ ((A[,]C) e. (Clsd` J) /\ (C[,]B) e. (Clsd` J) /\ ((A[,]C) u. (C[,]B)) = (A[,]B)) /\ (F:(A[,]B)-->U.M /\ (F |` (A[,]C)) e. ((subSp` <.(A[,]C), J>.) Cn M) /\ (F |` (C[,]B)) e. ((subSp` <.(C[,]B), J>.) Cn M))) -> F e. (J Cn M))
169	13, 47, 163, 168	mp3an 1191	1 |- F e. (J Cn M)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  _Vcvv 2292   u. cun 2591   C_ wss 2593  ifcif 2982  <.cop 3046  U.cuni 3177   class class class wbr 3338  {copab 3395  ran crn 3987   |` cres 3988  -->wf 3994  ` cfv 3998  (class class class)co 4884  RRcr 6385   <_ cle 6448   < clt 6653  (,)cioo 7524  [,]cicc 7527  Topctop 8857  topGenctg 8860  Clsdccld 8936   Cn ccn 9028  subSpcsubsp 10242

This theorem is referenced by:  pcopt 16084  pcoass 16085

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-n0 7309  df-z 7345  df-q 7436  df-ioo 7528  df-icc 7531  df-top 8861  df-topsp 8862  df-bases 8863  df-topgen 8864  df-cld 8939  df-cn 9030  df-subsp 10243

Copyright terms: Public domain