Theorem pcocn 16076

Description: The concatenation of two paths is a path.

Assertion

Ref	Expression
pcocn	|- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F(*p` J)G) e. (II Cn J))

Proof of Theorem pcocn

Step	Hyp	Ref	Expression
1		iitop 15867	. . 3 |- II e. Top
2	1	a1i 8	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> II e. Top)
3		simpl 346	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> J e. Top)
4		eqid 1884	. . . . . . 7 |- ((abs o. - ) |` (RR X. RR)) = ((abs o. - ) |` (RR X. RR))
5	4	remet 9188	. . . . . 6 |- ((abs o. - ) |` (RR X. RR)) e. Met
6		eqid 1884	. . . . . . 7 |- (Open` ((abs o. - ) |` (RR X. RR))) = (Open` ((abs o. - ) |` (RR X. RR)))
7	6	opntop 9147	. . . . . 6 |- (((abs o. - ) |` (RR X. RR)) e. Met -> (Open` ((abs o. - ) |` (RR X. RR))) e. Top)
8	5, 7	ax-mp 7	. . . . 5 |- (Open` ((abs o. - ) |` (RR X. RR))) e. Top
9		0re 6603	. . . . . 6 |- 0 e. RR
10		1re 6598	. . . . . 6 |- 1 e. RR
11		iccssre 7565	. . . . . 6 |- ((0 e. RR /\ 1 e. RR) -> (0[,]1) C_ RR)
12	9, 10, 11	mp2an 761	. . . . 5 |- (0[,]1) C_ RR
13		2re 7163	. . . . . . . 8 |- 2 e. RR
14		2ne0 7174	. . . . . . . 8 |- 2 =/= 0
15	13, 14	rereccli 6979	. . . . . . 7 |- (1 / 2) e. RR
16		clint3 10184	. . . . . . 7 |- ((0 e. RR /\ (1 / 2) e. RR) -> (0[,](1 / 2)) e. (Clsd` (topGen` ran (,))))
17	9, 15, 16	mp2an 761	. . . . . 6 |- (0[,](1 / 2)) e. (Clsd` (topGen` ran (,)))
18	4, 6	tgioo 9193	. . . . . . 7 |- (topGen` ran (,)) = (Open` ((abs o. - ) |` (RR X. RR)))
19	18	fveq2i 4684	. . . . . 6 |- (Clsd` (topGen` ran (,))) = (Clsd` (Open` ((abs o. - ) |` (RR X. RR))))
20	17, 19	eleqtri 1969	. . . . 5 |- (0[,](1 / 2)) e. (Clsd` (Open` ((abs o. - ) |` (RR X. RR))))
21	9, 10	pm3.2i 307	. . . . . 6 |- (0 e. RR /\ 1 e. RR)
22	9, 15	pm3.2i 307	. . . . . 6 |- (0 e. RR /\ (1 / 2) e. RR)
23	9	leidi 6790	. . . . . . 7 |- 0 <_ 0
24		halflt1 7216	. . . . . . . 8 |- (1 / 2) < 1
25	15, 10, 24	ltleii 6756	. . . . . . 7 |- (1 / 2) <_ 1
26	23, 25	pm3.2i 307	. . . . . 6 |- (0 <_ 0 /\ (1 / 2) <_ 1)
27		iccss 15855	. . . . . 6 |- (((0 e. RR /\ 1 e. RR) /\ (0 e. RR /\ (1 / 2) e. RR) /\ (0 <_ 0 /\ (1 / 2) <_ 1)) -> (0[,](1 / 2)) C_ (0[,]1))
28	21, 22, 26, 27	mp3an 1191	. . . . 5 |- (0[,](1 / 2)) C_ (0[,]1)
29	4	remetba 9187	. . . . . . . . 9 |- RR = dom dom ((abs o. - ) |` (RR X. RR))
30	29, 6	uniopn2 9138	. . . . . . . 8 |- (((abs o. - ) |` (RR X. RR)) e. Met -> U.(Open` ((abs o. - ) |` (RR X. RR))) = RR)
31	5, 30	ax-mp 7	. . . . . . 7 |- U.(Open` ((abs o. - ) |` (RR X. RR))) = RR
32	31	eqcomi 1888	. . . . . 6 |- RR = U.(Open` ((abs o. - ) |` (RR X. RR)))
33	32	subspcld 15838	. . . . 5 |- ((((Open` ((abs o. - ) |` (RR X. RR))) e. Top /\ (0[,]1) C_ RR) /\ ((0[,](1 / 2)) e. (Clsd` (Open` ((abs o. - ) |` (RR X. RR)))) /\ (0[,](1 / 2)) C_ (0[,]1))) -> (0[,](1 / 2)) e. (Clsd` (subSp` <.(0[,]1), (Open` ((abs o. - ) |` (RR X. RR)))>.)))
34	8, 12, 20, 28, 33	mp4an 15651	. . . 4 |- (0[,](1 / 2)) e. (Clsd` (subSp` <.(0[,]1), (Open` ((abs o. - ) |` (RR X. RR)))>.))
35		xpss12 4089	. . . . . . . . 9 |- (((0[,]1) C_ RR /\ (0[,]1) C_ RR) -> ((0[,]1) X. (0[,]1)) C_ (RR X. RR))
36	12, 12, 35	mp2an 761	. . . . . . . 8 |- ((0[,]1) X. (0[,]1)) C_ (RR X. RR)
37		resabs1 4244	. . . . . . . . 9 |- (((0[,]1) X. (0[,]1)) C_ (RR X. RR) -> (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1))) = ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
38	37	eqcomd 1889	. . . . . . . 8 |- (((0[,]1) X. (0[,]1)) C_ (RR X. RR) -> ((abs o. - ) |` ((0[,]1) X. (0[,]1))) = (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1))))
39	36, 38	ax-mp 7	. . . . . . 7 |- ((abs o. - ) |` ((0[,]1) X. (0[,]1))) = (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1)))
40	39	fveq2i 4684	. . . . . 6 |- (Open` ((abs o. - ) |` ((0[,]1) X. (0[,]1)))) = (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1))))
41		df-ii 15866	. . . . . 6 |- II = (Open` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
42		eqid 1884	. . . . . . . 8 |- (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1))) = (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1)))
43		eqid 1884	. . . . . . . 8 |- (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1)))) = (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1))))
44	42, 29, 6, 43	subtopmet 10256	. . . . . . 7 |- ((((abs o. - ) |` (RR X. RR)) e. Met /\ (0[,]1) C_ RR) -> (subSp` <.(0[,]1), (Open` ((abs o. - ) |` (RR X. RR)))>.) = (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1)))))
45	5, 12, 44	mp2an 761	. . . . . 6 |- (subSp` <.(0[,]1), (Open` ((abs o. - ) |` (RR X. RR)))>.) = (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,]1) X. (0[,]1))))
46	40, 41, 45	3eqtr4i 1921	. . . . 5 |- II = (subSp` <.(0[,]1), (Open` ((abs o. - ) |` (RR X. RR)))>.)
47	46	fveq2i 4684	. . . 4 |- (Clsd` II) = (Clsd` (subSp` <.(0[,]1), (Open` ((abs o. - ) |` (RR X. RR)))>.))
48	34, 47	eleqtrri 1970	. . 3 |- (0[,](1 / 2)) e. (Clsd` II)
49	48	a1i 8	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (0[,](1 / 2)) e. (Clsd` II))
50		clint3 10184	. . . . . . 7 |- (((1 / 2) e. RR /\ 1 e. RR) -> ((1 / 2)[,]1) e. (Clsd` (topGen` ran (,))))
51	15, 10, 50	mp2an 761	. . . . . 6 |- ((1 / 2)[,]1) e. (Clsd` (topGen` ran (,)))
52	51, 19	eleqtri 1969	. . . . 5 |- ((1 / 2)[,]1) e. (Clsd` (Open` ((abs o. - ) |` (RR X. RR))))
53	15, 10	pm3.2i 307	. . . . . 6 |- ((1 / 2) e. RR /\ 1 e. RR)
54		halfgt0 7215	. . . . . . . 8 |- 0 < (1 / 2)
55	9, 15, 54	ltleii 6756	. . . . . . 7 |- 0 <_ (1 / 2)
56	10	leidi 6790	. . . . . . 7 |- 1 <_ 1
57	55, 56	pm3.2i 307	. . . . . 6 |- (0 <_ (1 / 2) /\ 1 <_ 1)
58		iccss 15855	. . . . . 6 |- (((0 e. RR /\ 1 e. RR) /\ ((1 / 2) e. RR /\ 1 e. RR) /\ (0 <_ (1 / 2) /\ 1 <_ 1)) -> ((1 / 2)[,]1) C_ (0[,]1))
59	21, 53, 57, 58	mp3an 1191	. . . . 5 |- ((1 / 2)[,]1) C_ (0[,]1)
60	32	subspcld 15838	. . . . 5 |- ((((Open` ((abs o. - ) |` (RR X. RR))) e. Top /\ (0[,]1) C_ RR) /\ (((1 / 2)[,]1) e. (Clsd` (Open` ((abs o. - ) |` (RR X. RR)))) /\ ((1 / 2)[,]1) C_ (0[,]1))) -> ((1 / 2)[,]1) e. (Clsd` (subSp` <.(0[,]1), (Open` ((abs o. - ) |` (RR X. RR)))>.)))
61	8, 12, 52, 59, 60	mp4an 15651	. . . 4 |- ((1 / 2)[,]1) e. (Clsd` (subSp` <.(0[,]1), (Open` ((abs o. - ) |` (RR X. RR)))>.))
62	61, 47	eleqtrri 1970	. . 3 |- ((1 / 2)[,]1) e. (Clsd` II)
63	62	a1i 8	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((1 / 2)[,]1) e. (Clsd` II))
64		elicc2 7560	. . . . . . 7 |- ((0 e. RR /\ 1 e. RR) -> ((1 / 2) e. (0[,]1) <-> ((1 / 2) e. RR /\ 0 <_ (1 / 2) /\ (1 / 2) <_ 1)))
65	9, 10, 64	mp2an 761	. . . . . 6 |- ((1 / 2) e. (0[,]1) <-> ((1 / 2) e. RR /\ 0 <_ (1 / 2) /\ (1 / 2) <_ 1))
66	65, 15, 55, 25	mpbir3an 1052	. . . . 5 |- (1 / 2) e. (0[,]1)
67		iccsplit 15854	. . . . 5 |- ((0 e. RR /\ 1 e. RR /\ (1 / 2) e. (0[,]1)) -> (0[,]1) = ((0[,](1 / 2)) u. ((1 / 2)[,]1)))
68	9, 10, 66, 67	mp3an 1191	. . . 4 |- (0[,]1) = ((0[,](1 / 2)) u. ((1 / 2)[,]1))
69	68	eqcomi 1888	. . 3 |- ((0[,](1 / 2)) u. ((1 / 2)[,]1)) = (0[,]1)
70	69	a1i 8	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((0[,](1 / 2)) u. ((1 / 2)[,]1)) = (0[,]1))
71		df-f 4010	. . 3 |- ((F(*p` J)G):(0[,]1)-->U.J <-> ((F(*p` J)G) Fn (0[,]1) /\ ran ( F(*p` J)G) C_ U.J))
72		fvex 4689	. . . . . 6 |- (F` (2 x. x)) e. _V
73		fvex 4689	. . . . . 6 |- (G` ((2 x. x) - 1)) e. _V
74	72, 73	ifex 3031	. . . . 5 |- if(x <_ (1 / 2), (F` (2 x. x)), (G` ((2 x. x) - 1))) e. _V
75		eqid 1884	. . . . 5 |- {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (F` (2 x. x)), (G` ((2 x. x) - 1))))} = {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (F` (2 x. x)), (G` ((2 x. x) - 1))))}
76	74, 75	fnopab2 4549	. . . 4 |- {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (F` (2 x. x)), (G` ((2 x. x) - 1))))} Fn (0[,]1)
77		pcoval 16073	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F(*p` J)G) = {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (F` (2 x. x)), (G` ((2 x. x) - 1))))})
78	77	fneq1d 4505	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G) Fn (0[,]1) <-> {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (F` (2 x. x)), (G` ((2 x. x) - 1))))} Fn (0[,]1)))
79	76, 78	mpbiri 211	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F(*p` J)G) Fn (0[,]1))
80		pcoval1 16074	. . . . . . . 8 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ x e. (0[,](1 / 2))) -> ((F(*p` J)G)` x) = (F` (2 x. x)))
81		ffvelrn 4787	. . . . . . . . 9 |- ((F:(0[,]1)-->U.J /\ (2 x. x) e. (0[,]1)) -> (F` (2 x. x)) e. U.J)
82		iiuni 15868	. . . . . . . . . . . 12 |- (0[,]1) = U.II
83		eqid 1884	. . . . . . . . . . . 12 |- U.J = U.J
84	82, 83	cnf 9038	. . . . . . . . . . 11 |- ((II e. Top /\ J e. Top /\ F e. (II Cn J)) -> F:(0[,]1)-->U.J)
85	1, 84	mp3an1 1178	. . . . . . . . . 10 |- ((J e. Top /\ F e. (II Cn J)) -> F:(0[,]1)-->U.J)
86	85	3ad2antr1 1041	. . . . . . . . 9 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> F:(0[,]1)-->U.J)
87		iihalf1 15872	. . . . . . . . 9 |- (x e. (0[,](1 / 2)) -> (2 x. x) e. (0[,]1))
88	81, 86, 87	syl2an 503	. . . . . . . 8 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ x e. (0[,](1 / 2))) -> (F` (2 x. x)) e. U.J)
89	80, 88	eqeltrd 1971	. . . . . . 7 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ x e. (0[,](1 / 2))) -> ((F(*p` J)G)` x) e. U.J)
90		pcoval2 16075	. . . . . . . 8 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ x e. ((1 / 2)[,]1)) -> ((F(*p` J)G)` x) = (G` ((2 x. x) - 1)))
91		ffvelrn 4787	. . . . . . . . 9 |- ((G:(0[,]1)-->U.J /\ ((2 x. x) - 1) e. (0[,]1)) -> (G` ((2 x. x) - 1)) e. U.J)
92	82, 83	cnf 9038	. . . . . . . . . . 11 |- ((II e. Top /\ J e. Top /\ G e. (II Cn J)) -> G:(0[,]1)-->U.J)
93	1, 92	mp3an1 1178	. . . . . . . . . 10 |- ((J e. Top /\ G e. (II Cn J)) -> G:(0[,]1)-->U.J)
94	93	3ad2antr2 1042	. . . . . . . . 9 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> G:(0[,]1)-->U.J)
95		iihalf2 15873	. . . . . . . . 9 |- (x e. ((1 / 2)[,]1) -> ((2 x. x) - 1) e. (0[,]1))
96	91, 94, 95	syl2an 503	. . . . . . . 8 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ x e. ((1 / 2)[,]1)) -> (G` ((2 x. x) - 1)) e. U.J)
97	90, 96	eqeltrd 1971	. . . . . . 7 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ x e. ((1 / 2)[,]1)) -> ((F(*p` J)G)` x) e. U.J)
98	89, 97	jaodan 471	. . . . . 6 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ (x e. (0[,](1 / 2)) \/ x e. ((1 / 2)[,]1))) -> ((F(*p` J)G)` x) e. U.J)
99	68	eleq2i 1961	. . . . . . 7 |- (x e. (0[,]1) <-> x e. ((0[,](1 / 2)) u. ((1 / 2)[,]1)))
100		elun 2741	. . . . . . 7 |- (x e. ((0[,](1 / 2)) u. ((1 / 2)[,]1)) <-> (x e. (0[,](1 / 2)) \/ x e. ((1 / 2)[,]1)))
101	99, 100	bitri 190	. . . . . 6 |- (x e. (0[,]1) <-> (x e. (0[,](1 / 2)) \/ x e. ((1 / 2)[,]1)))
102	98, 101	sylan2b 501	. . . . 5 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ x e. (0[,]1)) -> ((F(*p` J)G)` x) e. U.J)
103	102	r19.21aiva 2176	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> A.x e. (0[,]1)((F(*p` J)G)` x) e. U.J)
104		fnfvrnss 4803	. . . 4 |- (((F(*p` J)G) Fn (0[,]1) /\ A.x e. (0[,]1)((F(*p` J)G)` x) e. U.J) -> ran ( F(*p` J)G) C_ U.J)
105	79, 103, 104	syl11anc 524	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ran ( F(*p` J)G) C_ U.J)
106	71, 79, 105	sylanbrc 527	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F(*p` J)G):(0[,]1)-->U.J)
107		pcoval1 16074	. . . . . . 7 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> ((F(*p` J)G)` z) = (F` (2 x. z)))
108		fvres 4691	. . . . . . . 8 |- (z e. (0[,](1 / 2)) -> (((F(*p` J)G) |` (0[,](1 / 2)))` z) = ((F(*p` J)G)` z))
109	108	adantl 424	. . . . . . 7 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> (((F(*p` J)G) |` (0[,](1 / 2)))` z) = ((F(*p` J)G)` z))
110		ffun 4565	. . . . . . . . . . . 12 |- (F:(0[,]1)-->U.J -> Fun F)
111	85, 110	syl 12	. . . . . . . . . . 11 |- ((J e. Top /\ F e. (II Cn J)) -> Fun F)
112	111	3ad2antr1 1041	. . . . . . . . . 10 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> Fun F)
113	112	adantr 425	. . . . . . . . 9 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> Fun F)
114		oprex 4907	. . . . . . . . . . . 12 |- (2 x. x) e. _V
115		eqid 1884	. . . . . . . . . . . 12 |- {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} = {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}
116	114, 115	fnopab2 4549	. . . . . . . . . . 11 |- {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} Fn (0[,](1 / 2))
117		fnfun 4510	. . . . . . . . . . 11 |- ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} Fn (0[,](1 / 2)) -> Fun {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})
118	116, 117	ax-mp 7	. . . . . . . . . 10 |- Fun {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}
119	118	a1i 8	. . . . . . . . 9 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> Fun {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})
120	114, 115	dmopab2 4550	. . . . . . . . . . . 12 |- dom {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} = (0[,](1 / 2))
121	120	eleq2i 1961	. . . . . . . . . . 11 |- (z e. dom {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} <-> z e. (0[,](1 / 2)))
122	121	biimpri 169	. . . . . . . . . 10 |- (z e. (0[,](1 / 2)) -> z e. dom {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})
123	122	adantl 424	. . . . . . . . 9 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> z e. dom {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})
124		fvco 4736	. . . . . . . . 9 |- ((Fun F /\ Fun {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} /\ z e. dom {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}) -> ((F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})` z) = (F` ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}` z)))
125	113, 119, 123, 124	syl111anc 1100	. . . . . . . 8 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> ((F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})` z) = (F` ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}` z)))
126		opreq2 4890	. . . . . . . . . . 11 |- (x = z -> (2 x. x) = (2 x. z))
127		oprex 4907	. . . . . . . . . . 11 |- (2 x. z) e. _V
128	126, 115, 127	fvopab4 4743	. . . . . . . . . 10 |- (z e. (0[,](1 / 2)) -> ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}` z) = (2 x. z))
129	128	adantl 424	. . . . . . . . 9 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}` z) = (2 x. z))
130	129	fveq2d 4685	. . . . . . . 8 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> (F` ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}` z)) = (F` (2 x. z)))
131	125, 130	eqtrd 1925	. . . . . . 7 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> ((F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})` z) = (F` (2 x. z)))
132	107, 109, 131	3eqtr4d 1937	. . . . . 6 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. (0[,](1 / 2))) -> (((F(*p` J)G) |` (0[,](1 / 2)))` z) = ((F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})` z))
133	132	r19.21aiva 2176	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> A.z e. (0[,](1 / 2))(((F(*p` J)G) |` (0[,](1 / 2)))` z) = ((F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})` z))
134		eqid 1884	. . . . 5 |- (0[,](1 / 2)) = (0[,](1 / 2))
135	133, 134	jctil 316	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((0[,](1 / 2)) = (0[,](1 / 2)) /\ A.z e. (0[,](1 / 2))(((F(*p` J)G) |` (0[,](1 / 2)))` z) = ((F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})` z)))
136		fnssres 4526	. . . . . 6 |- (((F(*p` J)G) Fn (0[,]1) /\ (0[,](1 / 2)) C_ (0[,]1)) -> ((F(*p` J)G) |` (0[,](1 / 2))) Fn (0[,](1 / 2)))
137	136, 79, 28	sylancl 525	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G) |` (0[,](1 / 2))) Fn (0[,](1 / 2)))
138		ffn 4562	. . . . . . . 8 |- (F:(0[,]1)-->U.J -> F Fn (0[,]1))
139	85, 138	syl 12	. . . . . . 7 |- ((J e. Top /\ F e. (II Cn J)) -> F Fn (0[,]1))
140	139	3ad2antr1 1041	. . . . . 6 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> F Fn (0[,]1))
141	116	a1i 8	. . . . . 6 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} Fn (0[,](1 / 2)))
142	87	rgen 2159	. . . . . . . 8 |- A.x e. (0[,](1 / 2))(2 x. x) e. (0[,]1)
143	115, 114	rnssopab 4798	. . . . . . . 8 |- (A.x e. (0[,](1 / 2))(2 x. x) e. (0[,]1) <-> ran {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} C_ (0[,]1))
144	142, 143	mpbi 206	. . . . . . 7 |- ran {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} C_ (0[,]1)
145	144	a1i 8	. . . . . 6 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ran {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} C_ (0[,]1))
146		fnco 4521	. . . . . 6 |- ((F Fn (0[,]1) /\ {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} Fn (0[,](1 / 2)) /\ ran {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} C_ (0[,]1)) -> (F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}) Fn (0[,](1 / 2)))
147	140, 141, 145, 146	syl111anc 1100	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}) Fn (0[,](1 / 2)))
148		eqfnfv 4766	. . . . 5 |- ((((F(*p` J)G) |` (0[,](1 / 2))) Fn (0[,](1 / 2)) /\ (F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}) Fn (0[,](1 / 2))) -> (((F(*p` J)G) |` (0[,](1 / 2))) = (F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}) <-> ((0[,](1 / 2)) = (0[,](1 / 2)) /\ A.z e. (0[,](1 / 2))(((F(*p` J)G) |` (0[,](1 / 2)))` z) = ((F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})` z))))
149	137, 147, 148	syl11anc 524	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (((F(*p` J)G) |` (0[,](1 / 2))) = (F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}) <-> ((0[,](1 / 2)) = (0[,](1 / 2)) /\ A.z e. (0[,](1 / 2))(((F(*p` J)G) |` (0[,](1 / 2)))` z) = ((F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})` z))))
150	135, 149	mpbird 213	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G) |` (0[,](1 / 2))) = (F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}))
151	28, 82	sseqtri 2649	. . . . . 6 |- (0[,](1 / 2)) C_ U.II
152		stoig3 10253	. . . . . 6 |- ((II e. Top /\ (0[,](1 / 2)) C_ U.II) -> (subSp` <.(0[,](1 / 2)), II>.) e. Top)
153	1, 151, 152	mp2an 761	. . . . 5 |- (subSp` <.(0[,](1 / 2)), II>.) e. Top
154	153	a1i 8	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (subSp` <.(0[,](1 / 2)), II>.) e. Top)
155		simpr1 882	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> F e. (II Cn J))
156		iccssre 7565	. . . . . . . . . . 11 |- ((0 e. RR /\ (1 / 2) e. RR) -> (0[,](1 / 2)) C_ RR)
157	9, 15, 156	mp2an 761	. . . . . . . . . 10 |- (0[,](1 / 2)) C_ RR
158		axresscn 6420	. . . . . . . . . 10 |- RR C_ CC
159	157, 158	sstri 2626	. . . . . . . . 9 |- (0[,](1 / 2)) C_ CC
160		resopab2 4256	. . . . . . . . . 10 |- ((0[,](1 / 2)) C_ CC -> ({<.x, y>. | (x e. CC /\ y = (2 x. x))} |` (0[,](1 / 2))) = {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))})
161	160	eqcomd 1889	. . . . . . . . 9 |- ((0[,](1 / 2)) C_ CC -> {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} = ({<.x, y>. | (x e. CC /\ y = (2 x. x))} |` (0[,](1 / 2))))
162	159, 161	ax-mp 7	. . . . . . . 8 |- {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} = ({<.x, y>. | (x e. CC /\ y = (2 x. x))} |` (0[,](1 / 2)))
163		2cn 7164	. . . . . . . . . 10 |- 2 e. CC
164		eqid 1884	. . . . . . . . . . 11 |- {<.x, y>. | (x e. CC /\ y = (2 x. x))} = {<.x, y>. | (x e. CC /\ y = (2 x. x))}
165	164	mulc1cncf 8541	. . . . . . . . . 10 |- (2 e. CC -> {<.x, y>. | (x e. CC /\ y = (2 x. x))} e. (CC-cn->CC))
166	163, 165	ax-mp 7	. . . . . . . . 9 |- {<.x, y>. | (x e. CC /\ y = (2 x. x))} e. (CC-cn->CC)
167		ssid 2634	. . . . . . . . . 10 |- CC C_ CC
168		rescncf 8534	. . . . . . . . . 10 |- ((CC C_ CC /\ CC C_ CC /\ (0[,](1 / 2)) C_ CC) -> ({<.x, y>. | (x e. CC /\ y = (2 x. x))} e. (CC-cn->CC) -> ({<.x, y>. | (x e. CC /\ y = (2 x. x))} |` (0[,](1 / 2))) e. ((0[,](1 / 2))-cn->CC)))
169	167, 167, 159, 168	mp3an 1191	. . . . . . . . 9 |- ({<.x, y>. | (x e. CC /\ y = (2 x. x))} e. (CC-cn->CC) -> ({<.x, y>. | (x e. CC /\ y = (2 x. x))} |` (0[,](1 / 2))) e. ((0[,](1 / 2))-cn->CC))
170	166, 169	ax-mp 7	. . . . . . . 8 |- ({<.x, y>. | (x e. CC /\ y = (2 x. x))} |` (0[,](1 / 2))) e. ((0[,](1 / 2))-cn->CC)
171	162, 170	eqeltri 1967	. . . . . . 7 |- {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((0[,](1 / 2))-cn->CC)
172	12, 158	sstri 2626	. . . . . . . . 9 |- (0[,]1) C_ CC
173	159, 167, 172	3pm3.2i 1048	. . . . . . . 8 |- ((0[,](1 / 2)) C_ CC /\ CC C_ CC /\ (0[,]1) C_ CC)
174		iihalf1 15872	. . . . . . . . . 10 |- (z e. (0[,](1 / 2)) -> (2 x. z) e. (0[,]1))
175	128, 174	eqeltrd 1971	. . . . . . . . 9 |- (z e. (0[,](1 / 2)) -> ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}` z) e. (0[,]1))
176	175	rgen 2159	. . . . . . . 8 |- A.z e. (0[,](1 / 2))({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}` z) e. (0[,]1)
177		cncffvrn 8535	. . . . . . . 8 |- ((((0[,](1 / 2)) C_ CC /\ CC C_ CC /\ (0[,]1) C_ CC) /\ A.z e. (0[,](1 / 2))({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}` z) e. (0[,]1)) -> ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((0[,](1 / 2))-cn->CC) -> {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((0[,](1 / 2))-cn->(0[,]1))))
178	173, 176, 177	mp2an 761	. . . . . . 7 |- ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((0[,](1 / 2))-cn->CC) -> {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((0[,](1 / 2))-cn->(0[,]1)))
179	171, 178	ax-mp 7	. . . . . 6 |- {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((0[,](1 / 2))-cn->(0[,]1))
180		xpss12 4089	. . . . . . . . . 10 |- (((0[,](1 / 2)) C_ (0[,]1) /\ (0[,](1 / 2)) C_ (0[,]1)) -> ((0[,](1 / 2)) X. (0[,](1 / 2))) C_ ((0[,]1) X. (0[,]1)))
181	28, 28, 180	mp2an 761	. . . . . . . . 9 |- ((0[,](1 / 2)) X. (0[,](1 / 2))) C_ ((0[,]1) X. (0[,]1))
182		resabs1 4244	. . . . . . . . 9 |- (((0[,](1 / 2)) X. (0[,](1 / 2))) C_ ((0[,]1) X. (0[,]1)) -> (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))) = ((abs o. - ) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))))
183	181, 182	ax-mp 7	. . . . . . . 8 |- (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))) = ((abs o. - ) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))
184		eqid 1884	. . . . . . . 8 |- ((abs o. - ) |` ((0[,]1) X. (0[,]1))) = ((abs o. - ) |` ((0[,]1) X. (0[,]1)))
185		eqid 1884	. . . . . . . . . . 11 |- (abs o. - ) = (abs o. - )
186	185	cnmet 9182	. . . . . . . . . 10 |- (abs o. - ) e. Met
187		metres 9100	. . . . . . . . . 10 |- ((abs o. - ) e. Met -> ((abs o. - ) |` ((0[,]1) X. (0[,]1))) e. Met)
188	186, 187	ax-mp 7	. . . . . . . . 9 |- ((abs o. - ) |` ((0[,]1) X. (0[,]1))) e. Met
189		eqid 1884	. . . . . . . . . 10 |- (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))) = (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))
190	185	cnmetba 9181	. . . . . . . . . . . 12 |- CC = dom dom (abs o. - )
191	190	metssba2 9087	. . . . . . . . . . 11 |- (((abs o. - ) e. Met /\ (0[,]1) C_ CC) -> (0[,]1) = dom dom ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
192	186, 172, 191	mp2an 761	. . . . . . . . . 10 |- (0[,]1) = dom dom ((abs o. - ) |` ((0[,]1) X. (0[,]1)))
193		eqid 1884	. . . . . . . . . 10 |- (Open` (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))) = (Open` (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))))
194	189, 192, 41, 193	subtopmet 10256	. . . . . . . . 9 |- ((((abs o. - ) |` ((0[,]1) X. (0[,]1))) e. Met /\ (0[,](1 / 2)) C_ (0[,]1)) -> (subSp` <.(0[,](1 / 2)), II>.) = (Open` (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))))
195	188, 28, 194	mp2an 761	. . . . . . . 8 |- (subSp` <.(0[,](1 / 2)), II>.) = (Open` (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))))
196	183, 184, 195, 41	cncfmet 9183	. . . . . . 7 |- (((0[,](1 / 2)) C_ CC /\ (0[,]1) C_ CC) -> ((0[,](1 / 2))-cn->(0[,]1)) = ((subSp` <.(0[,](1 / 2)), II>.) Cn II))
197	159, 172, 196	mp2an 761	. . . . . 6 |- ((0[,](1 / 2))-cn->(0[,]1)) = ((subSp` <.(0[,](1 / 2)), II>.) Cn II)
198	179, 197	eleqtri 1969	. . . . 5 |- {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((subSp` <.(0[,](1 / 2)), II>.) Cn II)
199	155, 198	jctil 316	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((subSp` <.(0[,](1 / 2)), II>.) Cn II) /\ F e. (II Cn J)))
200		cnco 9045	. . . 4 |- ((((subSp` <.(0[,](1 / 2)), II>.) e. Top /\ II e. Top /\ J e. Top) /\ ({<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))} e. ((subSp` <.(0[,](1 / 2)), II>.) Cn II) /\ F e. (II Cn J))) -> (F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}) e. ((subSp` <.(0[,](1 / 2)), II>.) Cn J))
201	154, 2, 3, 199, 200	syl31anc 1103	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F o. {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = (2 x. x))}) e. ((subSp` <.(0[,](1 / 2)), II>.) Cn J))
202	150, 201	eqeltrd 1971	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G) |` (0[,](1 / 2))) e. ((subSp` <.(0[,](1 / 2)), II>.) Cn J))
203		pcoval2 16075	. . . . . . 7 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> ((F(*p` J)G)` z) = (G` ((2 x. z) - 1)))
204		fvres 4691	. . . . . . . 8 |- (z e. ((1 / 2)[,]1) -> (((F(*p` J)G) |` ((1 / 2)[,]1))` z) = ((F(*p` J)G)` z))
205	204	adantl 424	. . . . . . 7 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> (((F(*p` J)G) |` ((1 / 2)[,]1))` z) = ((F(*p` J)G)` z))
206		ffn 4562	. . . . . . . . . . . . 13 |- (G:(0[,]1)-->U.J -> G Fn (0[,]1))
207	93, 206	syl 12	. . . . . . . . . . . 12 |- ((J e. Top /\ G e. (II Cn J)) -> G Fn (0[,]1))
208	207	3ad2antr2 1042	. . . . . . . . . . 11 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> G Fn (0[,]1))
209	208	adantr 425	. . . . . . . . . 10 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> G Fn (0[,]1))
210		fnfun 4510	. . . . . . . . . 10 |- (G Fn (0[,]1) -> Fun G)
211	209, 210	syl 12	. . . . . . . . 9 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> Fun G)
212		oprex 4907	. . . . . . . . . . . 12 |- ((2 x. x) - 1) e. _V
213		eqid 1884	. . . . . . . . . . . 12 |- {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} = {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}
214	212, 213	fnopab2 4549	. . . . . . . . . . 11 |- {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} Fn ((1 / 2)[,]1)
215		fnfun 4510	. . . . . . . . . . 11 |- ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} Fn ((1 / 2)[,]1) -> Fun {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})
216	214, 215	ax-mp 7	. . . . . . . . . 10 |- Fun {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}
217	216	a1i 8	. . . . . . . . 9 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> Fun {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})
218	212, 213	dmopab2 4550	. . . . . . . . . . . 12 |- dom {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} = ((1 / 2)[,]1)
219	218	eleq2i 1961	. . . . . . . . . . 11 |- (z e. dom {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} <-> z e. ((1 / 2)[,]1))
220	219	biimpri 169	. . . . . . . . . 10 |- (z e. ((1 / 2)[,]1) -> z e. dom {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})
221	220	adantl 424	. . . . . . . . 9 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> z e. dom {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})
222		fvco 4736	. . . . . . . . 9 |- ((Fun G /\ Fun {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} /\ z e. dom {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}) -> ((G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})` z) = (G` ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}` z)))
223	211, 217, 221, 222	syl111anc 1100	. . . . . . . 8 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> ((G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})` z) = (G` ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}` z)))
224	126	opreq1d 4897	. . . . . . . . . . 11 |- (x = z -> ((2 x. x) - 1) = ((2 x. z) - 1))
225		oprex 4907	. . . . . . . . . . 11 |- ((2 x. z) - 1) e. _V
226	224, 213, 225	fvopab4 4743	. . . . . . . . . 10 |- (z e. ((1 / 2)[,]1) -> ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}` z) = ((2 x. z) - 1))
227	226	adantl 424	. . . . . . . . 9 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}` z) = ((2 x. z) - 1))
228	227	fveq2d 4685	. . . . . . . 8 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> (G` ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}` z)) = (G` ((2 x. z) - 1)))
229	223, 228	eqtrd 1925	. . . . . . 7 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> ((G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})` z) = (G` ((2 x. z) - 1)))
230	203, 205, 229	3eqtr4d 1937	. . . . . 6 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ z e. ((1 / 2)[,]1)) -> (((F(*p` J)G) |` ((1 / 2)[,]1))` z) = ((G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})` z))
231	230	r19.21aiva 2176	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> A.z e. ((1 / 2)[,]1)(((F(*p` J)G) |` ((1 / 2)[,]1))` z) = ((G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})` z))
232		eqid 1884	. . . . 5 |- ((1 / 2)[,]1) = ((1 / 2)[,]1)
233	231, 232	jctil 316	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (((1 / 2)[,]1) = ((1 / 2)[,]1) /\ A.z e. ((1 / 2)[,]1)(((F(*p` J)G) |` ((1 / 2)[,]1))` z) = ((G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})` z)))
234		fnssres 4526	. . . . . 6 |- (((F(*p` J)G) Fn (0[,]1) /\ ((1 / 2)[,]1) C_ (0[,]1)) -> ((F(*p` J)G) |` ((1 / 2)[,]1)) Fn ((1 / 2)[,]1))
235	234, 79, 59	sylancl 525	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G) |` ((1 / 2)[,]1)) Fn ((1 / 2)[,]1))
236	214	a1i 8	. . . . . 6 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} Fn ((1 / 2)[,]1))
237	95	rgen 2159	. . . . . . . 8 |- A.x e. ((1 / 2)[,]1)((2 x. x) - 1) e. (0[,]1)
238	213, 212	rnssopab 4798	. . . . . . . 8 |- (A.x e. ((1 / 2)[,]1)((2 x. x) - 1) e. (0[,]1) <-> ran {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} C_ (0[,]1))
239	237, 238	mpbi 206	. . . . . . 7 |- ran {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} C_ (0[,]1)
240	239	a1i 8	. . . . . 6 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ran {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} C_ (0[,]1))
241		fnco 4521	. . . . . 6 |- ((G Fn (0[,]1) /\ {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} Fn ((1 / 2)[,]1) /\ ran {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} C_ (0[,]1)) -> (G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}) Fn ((1 / 2)[,]1))
242	208, 236, 240, 241	syl111anc 1100	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}) Fn ((1 / 2)[,]1))
243		eqfnfv 4766	. . . . 5 |- ((((F(*p` J)G) |` ((1 / 2)[,]1)) Fn ((1 / 2)[,]1) /\ (G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}) Fn ((1 / 2)[,]1)) -> (((F(*p` J)G) |` ((1 / 2)[,]1)) = (G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}) <-> (((1 / 2)[,]1) = ((1 / 2)[,]1) /\ A.z e. ((1 / 2)[,]1)(((F(*p` J)G) |` ((1 / 2)[,]1))` z) = ((G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})` z))))
244	235, 242, 243	syl11anc 524	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (((F(*p` J)G) |` ((1 / 2)[,]1)) = (G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}) <-> (((1 / 2)[,]1) = ((1 / 2)[,]1) /\ A.z e. ((1 / 2)[,]1)(((F(*p` J)G) |` ((1 / 2)[,]1))` z) = ((G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})` z))))
245	233, 244	mpbird 213	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G) |` ((1 / 2)[,]1)) = (G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}))
246	59, 82	sseqtri 2649	. . . . . 6 |- ((1 / 2)[,]1) C_ U.II
247		stoig3 10253	. . . . . 6 |- ((II e. Top /\ ((1 / 2)[,]1) C_ U.II) -> (subSp` <.((1 / 2)[,]1), II>.) e. Top)
248	1, 246, 247	mp2an 761	. . . . 5 |- (subSp` <.((1 / 2)[,]1), II>.) e. Top
249	248	a1i 8	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (subSp` <.((1 / 2)[,]1), II>.) e. Top)
250		simpr2 883	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> G e. (II Cn J))
251		iccssre 7565	. . . . . . . . . . 11 |- (((1 / 2) e. RR /\ 1 e. RR) -> ((1 / 2)[,]1) C_ RR)
252	15, 10, 251	mp2an 761	. . . . . . . . . 10 |- ((1 / 2)[,]1) C_ RR
253	252, 158	sstri 2626	. . . . . . . . 9 |- ((1 / 2)[,]1) C_ CC
254		resopab2 4256	. . . . . . . . 9 |- (((1 / 2)[,]1) C_ CC -> ({<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} |` ((1 / 2)[,]1)) = {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))})
255	253, 254	ax-mp 7	. . . . . . . 8 |- ({<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} |` ((1 / 2)[,]1)) = {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}
256		eqid 1884	. . . . . . . . . 10 |- (Open` (abs o. - )) = (Open` (abs o. - ))
257	10	elisseti 2301	. . . . . . . . . 10 |- 1 e. _V
258		eqid 1884	. . . . . . . . . 10 |- {<.x, z>. | (x e. CC /\ z = (2 x. x))} = {<.x, z>. | (x e. CC /\ z = (2 x. x))}
259		eqid 1884	. . . . . . . . . 10 |- {<.x, w>. | (x e. CC /\ w = 1)} = {<.x, w>. | (x e. CC /\ w = 1)}
260		eqid 1884	. . . . . . . . . 10 |- {<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} = {<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))}
261	258	mulc1cncf 8541	. . . . . . . . . . 11 |- (2 e. CC -> {<.x, z>. | (x e. CC /\ z = (2 x. x))} e. (CC-cn->CC))
262	163, 261	ax-mp 7	. . . . . . . . . 10 |- {<.x, z>. | (x e. CC /\ z = (2 x. x))} e. (CC-cn->CC)
263		ax1cn 6422	. . . . . . . . . . 11 |- 1 e. CC
264	259	constcncf 15882	. . . . . . . . . . 11 |- (1 e. CC -> {<.x, w>. | (x e. CC /\ w = 1)} e. (CC-cn->CC))
265	263, 264	ax-mp 7	. . . . . . . . . 10 |- {<.x, w>. | (x e. CC /\ w = 1)} e. (CC-cn->CC)
266	185, 256	subcntx 15928	. . . . . . . . . 10 |- - e. (((Open` (abs o. - )) X.t (Open` (abs o. - ))) Cn (Open` (abs o. - )))
267	256, 114, 257, 258, 259, 260, 262, 265, 266	cnopropabcoc 15918	. . . . . . . . 9 |- {<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} e. (CC-cn->CC)
268		rescncf 8534	. . . . . . . . . 10 |- ((CC C_ CC /\ CC C_ CC /\ ((1 / 2)[,]1) C_ CC) -> ({<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} e. (CC-cn->CC) -> ({<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} |` ((1 / 2)[,]1)) e. (((1 / 2)[,]1)-cn->CC)))
269	167, 167, 253, 268	mp3an 1191	. . . . . . . . 9 |- ({<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} e. (CC-cn->CC) -> ({<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} |` ((1 / 2)[,]1)) e. (((1 / 2)[,]1)-cn->CC))
270	267, 269	ax-mp 7	. . . . . . . 8 |- ({<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} |` ((1 / 2)[,]1)) e. (((1 / 2)[,]1)-cn->CC)
271	255, 270	eqeltrri 1968	. . . . . . 7 |- {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. (((1 / 2)[,]1)-cn->CC)
272	253, 167, 172	3pm3.2i 1048	. . . . . . . 8 |- (((1 / 2)[,]1) C_ CC /\ CC C_ CC /\ (0[,]1) C_ CC)
273		iihalf2 15873	. . . . . . . . . 10 |- (z e. ((1 / 2)[,]1) -> ((2 x. z) - 1) e. (0[,]1))
274	226, 273	eqeltrd 1971	. . . . . . . . 9 |- (z e. ((1 / 2)[,]1) -> ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}` z) e. (0[,]1))
275	274	rgen 2159	. . . . . . . 8 |- A.z e. ((1 / 2)[,]1)({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}` z) e. (0[,]1)
276		cncffvrn 8535	. . . . . . . 8 |- (((((1 / 2)[,]1) C_ CC /\ CC C_ CC /\ (0[,]1) C_ CC) /\ A.z e. ((1 / 2)[,]1)({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}` z) e. (0[,]1)) -> ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. (((1 / 2)[,]1)-cn->CC) -> {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. (((1 / 2)[,]1)-cn->(0[,]1))))
277	272, 275, 276	mp2an 761	. . . . . . 7 |- ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. (((1 / 2)[,]1)-cn->CC) -> {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. (((1 / 2)[,]1)-cn->(0[,]1)))
278	271, 277	ax-mp 7	. . . . . 6 |- {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. (((1 / 2)[,]1)-cn->(0[,]1))
279		xpss12 4089	. . . . . . . . . 10 |- ((((1 / 2)[,]1) C_ (0[,]1) /\ ((1 / 2)[,]1) C_ (0[,]1)) -> (((1 / 2)[,]1) X. ((1 / 2)[,]1)) C_ ((0[,]1) X. (0[,]1)))
280	59, 59, 279	mp2an 761	. . . . . . . . 9 |- (((1 / 2)[,]1) X. ((1 / 2)[,]1)) C_ ((0[,]1) X. (0[,]1))
281		resabs1 4244	. . . . . . . . 9 |- ((((1 / 2)[,]1) X. ((1 / 2)[,]1)) C_ ((0[,]1) X. (0[,]1)) -> (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))) = ((abs o. - ) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))))
282	280, 281	ax-mp 7	. . . . . . . 8 |- (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))) = ((abs o. - ) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))
283		eqid 1884	. . . . . . . . . 10 |- (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))) = (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))
284		eqid 1884	. . . . . . . . . 10 |- (Open` (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))) = (Open` (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))))
285	283, 192, 41, 284	subtopmet 10256	. . . . . . . . 9 |- ((((abs o. - ) |` ((0[,]1) X. (0[,]1))) e. Met /\ ((1 / 2)[,]1) C_ (0[,]1)) -> (subSp` <.((1 / 2)[,]1), II>.) = (Open` (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))))
286	188, 59, 285	mp2an 761	. . . . . . . 8 |- (subSp` <.((1 / 2)[,]1), II>.) = (Open` (((abs o. - ) |` ((0[,]1) X. (0[,]1))) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))))
287	282, 184, 286, 41	cncfmet 9183	. . . . . . 7 |- ((((1 / 2)[,]1) C_ CC /\ (0[,]1) C_ CC) -> (((1 / 2)[,]1)-cn->(0[,]1)) = ((subSp` <.((1 / 2)[,]1), II>.) Cn II))
288	253, 172, 287	mp2an 761	. . . . . 6 |- (((1 / 2)[,]1)-cn->(0[,]1)) = ((subSp` <.((1 / 2)[,]1), II>.) Cn II)
289	278, 288	eleqtri 1969	. . . . 5 |- {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. ((subSp` <.((1 / 2)[,]1), II>.) Cn II)
290	250, 289	jctil 316	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. ((subSp` <.((1 / 2)[,]1), II>.) Cn II) /\ G e. (II Cn J)))
291		cnco 9045	. . . 4 |- ((((subSp` <.((1 / 2)[,]1), II>.) e. Top /\ II e. Top /\ J e. Top) /\ ({<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. ((subSp` <.((1 / 2)[,]1), II>.) Cn II) /\ G e. (II Cn J))) -> (G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}) e. ((subSp` <.((1 / 2)[,]1), II>.) Cn J))
292	249, 2, 3, 290, 291	syl31anc 1103	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (G o. {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}) e. ((subSp` <.((1 / 2)[,]1), II>.) Cn J))
293	245, 292	eqeltrd 1971	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G) |` ((1 / 2)[,]1)) e. ((subSp` <.((1 / 2)[,]1), II>.) Cn J))
294	82, 83	paste 15893	. 2 |- (((II e. Top /\ J e. Top) /\ ((0[,](1 / 2)) e. (Clsd` II) /\ ((1 / 2)[,]1) e. (Clsd` II) /\ ((0[,](1 / 2)) u. ((1 / 2)[,]1)) = (0[,]1)) /\ ((F(*p` J)G):(0[,]1)-->U.J /\ ((F(*p` J)G) |` (0[,](1 / 2))) e. ((subSp` <.(0[,](1 / 2)), II>.) Cn J) /\ ((F(*p` J)G) |` ((1 / 2)[,]1)) e. ((subSp` <.((1 / 2)[,]1), II>.) Cn J))) -> (F(*p` J)G) e. (II Cn J))
295	2, 3, 49, 63, 70, 106, 202, 293, 294	syl233anc 1126	1 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F(*p` J)G) e. (II Cn J))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105   u. cun 2591   C_ wss 2593  ifcif 2982  <.cop 3046  U.cuni 3177   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986  ran crn 3987   |` cres 3988   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   x. cmul 6391   - cmin 6445   / cdiv 6447   <_ cle 6448  2c2 7145  (,)cioo 7524  [,]cicc 7527  abscabs 8000  -cn->ccncf 8524  Topctop 8857  topGenctg 8860  Clsdccld 8936   Cn ccn 9028  Metcme 9066  Opencopn 9069  subSpcsubsp 10242  IIcii 15865  *pcpco 16067

This theorem is referenced by:  pcoloopf 16079  pcohtpy 16083  pcoass 16085  pcorev 16087  pi1gp 16095

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  ax-ac 5906

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-sup 5664  df-r1 5750  df-rank 5751  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-2 7154  df-rp 7232  df-n0 7309  df-z 7345  df-q 7436  df-fl 7463  df-ioo 7528  df-icc 7531  df-uz 7587  df-seq1 7721  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-clim 8235  df-cncf 8525  df-top 8861  df-topsp 8862  df-bases 8863  df-topgen 8864  df-tx 8931  df-cld 8939  df-cn 9030  df-cnp 9031  df-met 9070  df-bl 9072  df-opn 9073  df-lm 9200  df-subsp 10243  df-ii 15866  df-pco 16069

Copyright terms: Public domain