Theorem pcopt 16084

Description: Concatenation with a point does not affect homotopy class.

Hypothesis

Ref	Expression
pcopt.1	|- P = ((0[,]1) X. {Y})

Assertion

Ref	Expression
pcopt	|- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> (P(*p` J)F)(~=ph` J)F)

Proof of Theorem pcopt

Step	Hyp	Ref	Expression
1		simp3 878	. . . . . . 7 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> (F` 0) = Y)
2	1	eqcomd 1889	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> Y = (F` 0))
3	2	sneqd 3056	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> {Y} = {(F` 0)})
4		xpeq2 4017	. . . . 5 |- ({Y} = {(F` 0)} -> ((0[,]1) X. {Y}) = ((0[,]1) X. {(F` 0)}))
5	3, 4	syl 12	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> ((0[,]1) X. {Y}) = ((0[,]1) X. {(F` 0)}))
6		pcopt.1	. . . 4 |- P = ((0[,]1) X. {Y})
7	5, 6	syl5eq 1940	. . 3 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> P = ((0[,]1) X. {(F` 0)}))
8	7	opreq1d 4897	. 2 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> (P(*p` J)F) = (((0[,]1) X. {(F` 0)})(*p` J)F))
9		simpl 346	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J)) -> J e. Top)
10		iitop 15867	. . . . . . . 8 |- II e. Top
11	10	a1i 8	. . . . . . 7 |- ((J e. Top /\ F e. (II Cn J)) -> II e. Top)
12		ffvelrn 4787	. . . . . . . 8 |- ((F:(0[,]1)-->U.J /\ 0 e. (0[,]1)) -> (F` 0) e. U.J)
13		iiuni 15868	. . . . . . . . . 10 |- (0[,]1) = U.II
14		eqid 1884	. . . . . . . . . 10 |- U.J = U.J
15	13, 14	cnf 9038	. . . . . . . . 9 |- ((II e. Top /\ J e. Top /\ F e. (II Cn J)) -> F:(0[,]1)-->U.J)
16	10, 15	mp3an1 1178	. . . . . . . 8 |- ((J e. Top /\ F e. (II Cn J)) -> F:(0[,]1)-->U.J)
17		0re 6603	. . . . . . . . 9 |- 0 e. RR
18		1re 6598	. . . . . . . . 9 |- 1 e. RR
19		lt01 6871	. . . . . . . . . 10 |- 0 < 1
20	17, 18, 19	ltleii 6756	. . . . . . . . 9 |- 0 <_ 1
21		lbicc2 7573	. . . . . . . . 9 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 0 e. (0[,]1))
22	17, 18, 20, 21	mp3an 1191	. . . . . . . 8 |- 0 e. (0[,]1)
23	12, 16, 22	sylancl 525	. . . . . . 7 |- ((J e. Top /\ F e. (II Cn J)) -> (F` 0) e. U.J)
24		fvex 4689	. . . . . . . . 9 |- (F` 0) e. _V
25	24	fconst 4602	. . . . . . . 8 |- ((0[,]1) X. {(F` 0)}):(0[,]1)-->{(F` 0)}
26	25	a1i 8	. . . . . . 7 |- ((J e. Top /\ F e. (II Cn J)) -> ((0[,]1) X. {(F` 0)}):(0[,]1)-->{(F` 0)})
27	13, 14	cnconst 9057	. . . . . . 7 |- (((II e. Top /\ J e. Top) /\ ((F` 0) e. U.J /\ ((0[,]1) X. {(F` 0)}):(0[,]1)-->{(F` 0)})) -> ((0[,]1) X. {(F` 0)}) e. (II Cn J))
28	11, 9, 23, 26, 27	syl22anc 1101	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J)) -> ((0[,]1) X. {(F` 0)}) e. (II Cn J))
29		simpr 350	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J)) -> F e. (II Cn J))
30		ubicc2 7574	. . . . . . . . 9 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 1 e. (0[,]1))
31	17, 18, 20, 30	mp3an 1191	. . . . . . . 8 |- 1 e. (0[,]1)
32	24	fvconst2 4822	. . . . . . . 8 |- (1 e. (0[,]1) -> (((0[,]1) X. {(F` 0)})` 1) = (F` 0))
33	31, 32	ax-mp 7	. . . . . . 7 |- (((0[,]1) X. {(F` 0)})` 1) = (F` 0)
34	33	a1i 8	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J)) -> (((0[,]1) X. {(F` 0)})` 1) = (F` 0))
35		pcoval 16073	. . . . . 6 |- ((J e. Top /\ (((0[,]1) X. {(F` 0)}) e. (II Cn J) /\ F e. (II Cn J) /\ (((0[,]1) X. {(F` 0)})` 1) = (F` 0))) -> (((0[,]1) X. {(F` 0)})(*p` J)F) = {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (((0[,]1) X. {(F` 0)})` (2 x. x)), (F` ((2 x. x) - 1))))})
36	9, 28, 29, 34, 35	syl13anc 1102	. . . . 5 |- ((J e. Top /\ F e. (II Cn J)) -> (((0[,]1) X. {(F` 0)})(*p` J)F) = {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (((0[,]1) X. {(F` 0)})` (2 x. x)), (F` ((2 x. x) - 1))))})
37		ffn 4562	. . . . . . 7 |- (F:(0[,]1)-->U.J -> F Fn (0[,]1))
38		exmid 717	. . . . . . . . . 10 |- (x <_ (1 / 2) \/ -. x <_ (1 / 2))
39	22	jctr 315	. . . . . . . . . . . 12 |- (x <_ (1 / 2) -> (x <_ (1 / 2) /\ 0 e. (0[,]1)))
40	39	a1i 8	. . . . . . . . . . 11 |- (x e. (0[,]1) -> (x <_ (1 / 2) -> (x <_ (1 / 2) /\ 0 e. (0[,]1))))
41		elicc2 7560	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ 1 e. RR) -> (x e. (0[,]1) <-> (x e. RR /\ 0 <_ x /\ x <_ 1)))
42	17, 18, 41	mp2an 761	. . . . . . . . . . . . 13 |- (x e. (0[,]1) <-> (x e. RR /\ 0 <_ x /\ x <_ 1))
43		2re 7163	. . . . . . . . . . . . . . . . 17 |- 2 e. RR
44		2ne0 7174	. . . . . . . . . . . . . . . . 17 |- 2 =/= 0
45	43, 44	rereccli 6979	. . . . . . . . . . . . . . . 16 |- (1 / 2) e. RR
46		ltnle 6680	. . . . . . . . . . . . . . . 16 |- (((1 / 2) e. RR /\ x e. RR) -> ((1 / 2) < x <-> -. x <_ (1 / 2)))
47	45, 46	mpan 759	. . . . . . . . . . . . . . 15 |- (x e. RR -> ((1 / 2) < x <-> -. x <_ (1 / 2)))
48	47	3ad2ant1 897	. . . . . . . . . . . . . 14 |- ((x e. RR /\ 0 <_ x /\ x <_ 1) -> ((1 / 2) < x <-> -. x <_ (1 / 2)))
49		ltle 6690	. . . . . . . . . . . . . . . . 17 |- (((1 / 2) e. RR /\ x e. RR) -> ((1 / 2) < x -> (1 / 2) <_ x))
50	45, 49	mpan 759	. . . . . . . . . . . . . . . 16 |- (x e. RR -> ((1 / 2) < x -> (1 / 2) <_ x))
51	50	3ad2ant1 897	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ 0 <_ x /\ x <_ 1) -> ((1 / 2) < x -> (1 / 2) <_ x))
52		elicc2 7560	. . . . . . . . . . . . . . . . . . . . 21 |- (((1 / 2) e. RR /\ 1 e. RR) -> (x e. ((1 / 2)[,]1) <-> (x e. RR /\ (1 / 2) <_ x /\ x <_ 1)))
53	45, 18, 52	mp2an 761	. . . . . . . . . . . . . . . . . . . 20 |- (x e. ((1 / 2)[,]1) <-> (x e. RR /\ (1 / 2) <_ x /\ x <_ 1))
54		iihalf2 15873	. . . . . . . . . . . . . . . . . . . 20 |- (x e. ((1 / 2)[,]1) -> ((2 x. x) - 1) e. (0[,]1))
55	53, 54	sylbir 218	. . . . . . . . . . . . . . . . . . 19 |- ((x e. RR /\ (1 / 2) <_ x /\ x <_ 1) -> ((2 x. x) - 1) e. (0[,]1))
56	55	3expa 1067	. . . . . . . . . . . . . . . . . 18 |- (((x e. RR /\ (1 / 2) <_ x) /\ x <_ 1) -> ((2 x. x) - 1) e. (0[,]1))
57	56	an1rs 547	. . . . . . . . . . . . . . . . 17 |- (((x e. RR /\ x <_ 1) /\ (1 / 2) <_ x) -> ((2 x. x) - 1) e. (0[,]1))
58	57	ex 402	. . . . . . . . . . . . . . . 16 |- ((x e. RR /\ x <_ 1) -> ((1 / 2) <_ x -> ((2 x. x) - 1) e. (0[,]1)))
59	58	3adant2 895	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ 0 <_ x /\ x <_ 1) -> ((1 / 2) <_ x -> ((2 x. x) - 1) e. (0[,]1)))
60	51, 59	syld 30	. . . . . . . . . . . . . 14 |- ((x e. RR /\ 0 <_ x /\ x <_ 1) -> ((1 / 2) < x -> ((2 x. x) - 1) e. (0[,]1)))
61	48, 60	sylbird 222	. . . . . . . . . . . . 13 |- ((x e. RR /\ 0 <_ x /\ x <_ 1) -> (-. x <_ (1 / 2) -> ((2 x. x) - 1) e. (0[,]1)))
62	42, 61	sylbi 216	. . . . . . . . . . . 12 |- (x e. (0[,]1) -> (-. x <_ (1 / 2) -> ((2 x. x) - 1) e. (0[,]1)))
63	62	ancld 322	. . . . . . . . . . 11 |- (x e. (0[,]1) -> (-. x <_ (1 / 2) -> (-. x <_ (1 / 2) /\ ((2 x. x) - 1) e. (0[,]1))))
64	40, 63	orim12d 624	. . . . . . . . . 10 |- (x e. (0[,]1) -> ((x <_ (1 / 2) \/ -. x <_ (1 / 2)) -> ((x <_ (1 / 2) /\ 0 e. (0[,]1)) \/ (-. x <_ (1 / 2) /\ ((2 x. x) - 1) e. (0[,]1)))))
65	38, 64	mpi 55	. . . . . . . . 9 |- (x e. (0[,]1) -> ((x <_ (1 / 2) /\ 0 e. (0[,]1)) \/ (-. x <_ (1 / 2) /\ ((2 x. x) - 1) e. (0[,]1))))
66		ifel 3006	. . . . . . . . 9 |- (if(x <_ (1 / 2), 0, ((2 x. x) - 1)) e. (0[,]1) <-> ((x <_ (1 / 2) /\ 0 e. (0[,]1)) \/ (-. x <_ (1 / 2) /\ ((2 x. x) - 1) e. (0[,]1))))
67	65, 66	sylibr 217	. . . . . . . 8 |- (x e. (0[,]1) -> if(x <_ (1 / 2), 0, ((2 x. x) - 1)) e. (0[,]1))
68		eqid 1884	. . . . . . . 8 |- {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))} = {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}
69		eqid 1884	. . . . . . . 8 |- {<.x, y>. | (x e. (0[,]1) /\ y = (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1))))} = {<.x, y>. | (x e. (0[,]1) /\ y = (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1))))}
70	67, 68, 69	fnopabco 15711	. . . . . . 7 |- (F Fn (0[,]1) -> {<.x, y>. | (x e. (0[,]1) /\ y = (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1))))} = (F o. {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}))
71	16, 37, 70	3syl 24	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J)) -> {<.x, y>. | (x e. (0[,]1) /\ y = (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1))))} = (F o. {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}))
72		simpl1 879	. . . . . . . . . . . . . . 15 |- (((x e. RR /\ 0 <_ x /\ x <_ 1) /\ x <_ (1 / 2)) -> x e. RR)
73		simpl2 880	. . . . . . . . . . . . . . 15 |- (((x e. RR /\ 0 <_ x /\ x <_ 1) /\ x <_ (1 / 2)) -> 0 <_ x)
74		simpr 350	. . . . . . . . . . . . . . 15 |- (((x e. RR /\ 0 <_ x /\ x <_ 1) /\ x <_ (1 / 2)) -> x <_ (1 / 2))
75	72, 73, 74	3jca 1050	. . . . . . . . . . . . . 14 |- (((x e. RR /\ 0 <_ x /\ x <_ 1) /\ x <_ (1 / 2)) -> (x e. RR /\ 0 <_ x /\ x <_ (1 / 2)))
76	75, 42	sylanb 498	. . . . . . . . . . . . 13 |- ((x e. (0[,]1) /\ x <_ (1 / 2)) -> (x e. RR /\ 0 <_ x /\ x <_ (1 / 2)))
77		elicc2 7560	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ (1 / 2) e. RR) -> (x e. (0[,](1 / 2)) <-> (x e. RR /\ 0 <_ x /\ x <_ (1 / 2))))
78	17, 45, 77	mp2an 761	. . . . . . . . . . . . 13 |- (x e. (0[,](1 / 2)) <-> (x e. RR /\ 0 <_ x /\ x <_ (1 / 2)))
79	76, 78	sylibr 217	. . . . . . . . . . . 12 |- ((x e. (0[,]1) /\ x <_ (1 / 2)) -> x e. (0[,](1 / 2)))
80		iihalf1 15872	. . . . . . . . . . . 12 |- (x e. (0[,](1 / 2)) -> (2 x. x) e. (0[,]1))
81	24	fvconst2 4822	. . . . . . . . . . . 12 |- ((2 x. x) e. (0[,]1) -> (((0[,]1) X. {(F` 0)})` (2 x. x)) = (F` 0))
82	79, 80, 81	3syl 24	. . . . . . . . . . 11 |- ((x e. (0[,]1) /\ x <_ (1 / 2)) -> (((0[,]1) X. {(F` 0)})` (2 x. x)) = (F` 0))
83	82	ifeq1da 15693	. . . . . . . . . 10 |- (x e. (0[,]1) -> if(x <_ (1 / 2), (((0[,]1) X. {(F` 0)})` (2 x. x)), (F` ((2 x. x) - 1))) = if(x <_ (1 / 2), (F` 0), (F` ((2 x. x) - 1))))
84		fvif 15692	. . . . . . . . . 10 |- (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1))) = if(x <_ (1 / 2), (F` 0), (F` ((2 x. x) - 1)))
85	83, 84	syl6eqr 1946	. . . . . . . . 9 |- (x e. (0[,]1) -> if(x <_ (1 / 2), (((0[,]1) X. {(F` 0)})` (2 x. x)), (F` ((2 x. x) - 1))) = (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1))))
86	85	eqeq2d 1895	. . . . . . . 8 |- (x e. (0[,]1) -> (y = if(x <_ (1 / 2), (((0[,]1) X. {(F` 0)})` (2 x. x)), (F` ((2 x. x) - 1))) <-> y = (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1)))))
87	86	pm5.32i 707	. . . . . . 7 |- ((x e. (0[,]1) /\ y = if(x <_ (1 / 2), (((0[,]1) X. {(F` 0)})` (2 x. x)), (F` ((2 x. x) - 1)))) <-> (x e. (0[,]1) /\ y = (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1)))))
88	87	opabbii 3402	. . . . . 6 |- {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (((0[,]1) X. {(F` 0)})` (2 x. x)), (F` ((2 x. x) - 1))))} = {<.x, y>. | (x e. (0[,]1) /\ y = (F` if(x <_ (1 / 2), 0, ((2 x. x) - 1))))}
89	71, 88	syl5eq 1940	. . . . 5 |- ((J e. Top /\ F e. (II Cn J)) -> {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), (((0[,]1) X. {(F` 0)})` (2 x. x)), (F` ((2 x. x) - 1))))} = (F o. {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}))
90	36, 89	eqtrd 1925	. . . 4 |- ((J e. Top /\ F e. (II Cn J)) -> (((0[,]1) X. {(F` 0)})(*p` J)F) = (F o. {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}))
91		elicc2 7560	. . . . . . . . 9 |- ((0 e. RR /\ 1 e. RR) -> ((1 / 2) e. (0[,]1) <-> ((1 / 2) e. RR /\ 0 <_ (1 / 2) /\ (1 / 2) <_ 1)))
92	17, 18, 91	mp2an 761	. . . . . . . 8 |- ((1 / 2) e. (0[,]1) <-> ((1 / 2) e. RR /\ 0 <_ (1 / 2) /\ (1 / 2) <_ 1))
93		halfgt0 7215	. . . . . . . . 9 |- 0 < (1 / 2)
94	17, 45, 93	ltleii 6756	. . . . . . . 8 |- 0 <_ (1 / 2)
95		halflt1 7216	. . . . . . . . 9 |- (1 / 2) < 1
96	45, 18, 95	ltleii 6756	. . . . . . . 8 |- (1 / 2) <_ 1
97	92, 45, 94, 96	mpbir3an 1052	. . . . . . 7 |- (1 / 2) e. (0[,]1)
98	17	elisseti 2301	. . . . . . 7 |- 0 e. _V
99		oprex 4907	. . . . . . 7 |- ((2 x. x) - 1) e. _V
100		dfii2 15869	. . . . . . 7 |- II = (subSp` <.(0[,]1), (topGen` ran (,))>.)
101		eqid 1884	. . . . . . 7 |- (subSp` <.(0[,](1 / 2)), (topGen` ran (,))>.) = (subSp` <.(0[,](1 / 2)), (topGen` ran (,))>.)
102		eqid 1884	. . . . . . 7 |- (subSp` <.((1 / 2)[,]1), (topGen` ran (,))>.) = (subSp` <.((1 / 2)[,]1), (topGen` ran (,))>.)
103		opreq2 4890	. . . . . . . . 9 |- (x = (1 / 2) -> (2 x. x) = (2 x. (1 / 2)))
104	103	opreq1d 4897	. . . . . . . 8 |- (x = (1 / 2) -> ((2 x. x) - 1) = ((2 x. (1 / 2)) - 1))
105		2cn 7164	. . . . . . . . . 10 |- 2 e. CC
106	45	recni 6467	. . . . . . . . . 10 |- (1 / 2) e. CC
107	105, 106	mulcli 6474	. . . . . . . . 9 |- (2 x. (1 / 2)) e. CC
108		ax1cn 6422	. . . . . . . . 9 |- 1 e. CC
109		0cn 6481	. . . . . . . . 9 |- 0 e. CC
110	108	addid1i 6483	. . . . . . . . . 10 |- (1 + 0) = 1
111	105, 44	recidi 6916	. . . . . . . . . 10 |- (2 x. (1 / 2)) = 1
112	110, 111	eqtr4i 1911	. . . . . . . . 9 |- (1 + 0) = (2 x. (1 / 2))
113	107, 108, 109, 112	subaddrii 6529	. . . . . . . 8 |- ((2 x. (1 / 2)) - 1) = 0
114	104, 113	syl6req 1945	. . . . . . 7 |- (x = (1 / 2) -> 0 = ((2 x. x) - 1))
115		eqid 1884	. . . . . . 7 |- {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = 0)} = {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = 0)}
116		eqid 1884	. . . . . . 7 |- {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} = {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))}
117		iccssre 7565	. . . . . . . . . 10 |- ((0 e. RR /\ (1 / 2) e. RR) -> (0[,](1 / 2)) C_ RR)
118	17, 45, 117	mp2an 761	. . . . . . . . 9 |- (0[,](1 / 2)) C_ RR
119		axresscn 6420	. . . . . . . . 9 |- RR C_ CC
120	118, 119	sstri 2626	. . . . . . . 8 |- (0[,](1 / 2)) C_ CC
121		iccssre 7565	. . . . . . . . . 10 |- ((0 e. RR /\ 1 e. RR) -> (0[,]1) C_ RR)
122	17, 18, 121	mp2an 761	. . . . . . . . 9 |- (0[,]1) C_ RR
123	122, 119	sstri 2626	. . . . . . . 8 |- (0[,]1) C_ CC
124		eqid 1884	. . . . . . . 8 |- {<.x, y>. | (x e. CC /\ y = 0)} = {<.x, y>. | (x e. CC /\ y = 0)}
125	22	a1i 8	. . . . . . . 8 |- (x e. (0[,](1 / 2)) -> 0 e. (0[,]1))
126	124	constcncf 15882	. . . . . . . . 9 |- (0 e. CC -> {<.x, y>. | (x e. CC /\ y = 0)} e. (CC-cn->CC))
127	109, 126	ax-mp 7	. . . . . . . 8 |- {<.x, y>. | (x e. CC /\ y = 0)} e. (CC-cn->CC)
128		eqid 1884	. . . . . . . . . . 11 |- ((abs o. - ) |` (RR X. RR)) = ((abs o. - ) |` (RR X. RR))
129	128	remet 9188	. . . . . . . . . 10 |- ((abs o. - ) |` (RR X. RR)) e. Met
130		eqid 1884	. . . . . . . . . . 11 |- (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))) = (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))
131	128	remetba 9187	. . . . . . . . . . 11 |- RR = dom dom ((abs o. - ) |` (RR X. RR))
132		eqid 1884	. . . . . . . . . . . 12 |- (Open` ((abs o. - ) |` (RR X. RR))) = (Open` ((abs o. - ) |` (RR X. RR)))
133	128, 132	tgioo 9193	. . . . . . . . . . 11 |- (topGen` ran (,)) = (Open` ((abs o. - ) |` (RR X. RR)))
134		eqid 1884	. . . . . . . . . . 11 |- (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))) = (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))))
135	130, 131, 133, 134	subtopmet 10256	. . . . . . . . . 10 |- ((((abs o. - ) |` (RR X. RR)) e. Met /\ (0[,](1 / 2)) C_ RR) -> (subSp` <.(0[,](1 / 2)), (topGen` ran (,))>.) = (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))))
136	129, 118, 135	mp2an 761	. . . . . . . . 9 |- (subSp` <.(0[,](1 / 2)), (topGen` ran (,))>.) = (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))))
137		xpss12 4089	. . . . . . . . . . . 12 |- (((0[,](1 / 2)) C_ RR /\ (0[,](1 / 2)) C_ RR) -> ((0[,](1 / 2)) X. (0[,](1 / 2))) C_ (RR X. RR))
138	137	anidms 480	. . . . . . . . . . 11 |- ((0[,](1 / 2)) C_ RR -> ((0[,](1 / 2)) X. (0[,](1 / 2))) C_ (RR X. RR))
139	118, 138	ax-mp 7	. . . . . . . . . 10 |- ((0[,](1 / 2)) X. (0[,](1 / 2))) C_ (RR X. RR)
140		resabs1 4244	. . . . . . . . . . 11 |- (((0[,](1 / 2)) X. (0[,](1 / 2))) C_ (RR X. RR) -> (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))) = ((abs o. - ) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))))
141	140	fveq2d 4685	. . . . . . . . . 10 |- (((0[,](1 / 2)) X. (0[,](1 / 2))) C_ (RR X. RR) -> (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))) = (Open` ((abs o. - ) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))))
142	139, 141	ax-mp 7	. . . . . . . . 9 |- (Open` (((abs o. - ) |` (RR X. RR)) |` ((0[,](1 / 2)) X. (0[,](1 / 2))))) = (Open` ((abs o. - ) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))))
143	136, 142	eqtri 1908	. . . . . . . 8 |- (subSp` <.(0[,](1 / 2)), (topGen` ran (,))>.) = (Open` ((abs o. - ) |` ((0[,](1 / 2)) X. (0[,](1 / 2)))))
144		df-ii 15866	. . . . . . . 8 |- II = (Open` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
145	120, 123, 124, 115, 125, 127, 143, 144	cncfres 15895	. . . . . . 7 |- {<.x, y>. | (x e. (0[,](1 / 2)) /\ y = 0)} e. ((subSp` <.(0[,](1 / 2)), (topGen` ran (,))>.) Cn II)
146		iccssre 7565	. . . . . . . . . 10 |- (((1 / 2) e. RR /\ 1 e. RR) -> ((1 / 2)[,]1) C_ RR)
147	45, 18, 146	mp2an 761	. . . . . . . . 9 |- ((1 / 2)[,]1) C_ RR
148	147, 119	sstri 2626	. . . . . . . 8 |- ((1 / 2)[,]1) C_ CC
149		eqid 1884	. . . . . . . 8 |- {<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} = {<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))}
150		eqid 1884	. . . . . . . . . . . 12 |- {<.x, v>. | (x e. CC /\ v = (2 x. x))} = {<.x, v>. | (x e. CC /\ v = (2 x. x))}
151		mulcl 6456	. . . . . . . . . . . . 13 |- ((2 e. CC /\ x e. CC) -> (2 x. x) e. CC)
152	105, 151	mpan 759	. . . . . . . . . . . 12 |- (x e. CC -> (2 x. x) e. CC)
153	150, 152	fopab 4800	. . . . . . . . . . 11 |- {<.x, v>. | (x e. CC /\ v = (2 x. x))}:CC-->CC
154		frn 4569	. . . . . . . . . . 11 |- ({<.x, v>. | (x e. CC /\ v = (2 x. x))}:CC-->CC -> ran {<.x, v>. | (x e. CC /\ v = (2 x. x))} C_ CC)
155	153, 154	ax-mp 7	. . . . . . . . . 10 |- ran {<.x, v>. | (x e. CC /\ v = (2 x. x))} C_ CC
156		oprex 4907	. . . . . . . . . . 11 |- (2 x. x) e. _V
157		oprex 4907	. . . . . . . . . . 11 |- (w - 1) e. _V
158		opreq1 4889	. . . . . . . . . . 11 |- (w = (2 x. x) -> (w - 1) = ((2 x. x) - 1))
159		eqid 1884	. . . . . . . . . . 11 |- {<.w, z>. | (w e. CC /\ z = (w - 1))} = {<.w, z>. | (w e. CC /\ z = (w - 1))}
160	156, 157, 99, 158, 150, 159, 149	fopabco 4805	. . . . . . . . . 10 |- (ran {<.x, v>. | (x e. CC /\ v = (2 x. x))} C_ CC -> ({<.w, z>. | (w e. CC /\ z = (w - 1))} o. {<.x, v>. | (x e. CC /\ v = (2 x. x))}) = {<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))})
161	155, 160	ax-mp 7	. . . . . . . . 9 |- ({<.w, z>. | (w e. CC /\ z = (w - 1))} o. {<.x, v>. | (x e. CC /\ v = (2 x. x))}) = {<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))}
162		ssid 2634	. . . . . . . . . . 11 |- CC C_ CC
163	162, 162, 162	3pm3.2i 1048	. . . . . . . . . 10 |- (CC C_ CC /\ CC C_ CC /\ CC C_ CC)
164	150	mulc1cncf 8541	. . . . . . . . . . . 12 |- (2 e. CC -> {<.x, v>. | (x e. CC /\ v = (2 x. x))} e. (CC-cn->CC))
165	105, 164	ax-mp 7	. . . . . . . . . . 11 |- {<.x, v>. | (x e. CC /\ v = (2 x. x))} e. (CC-cn->CC)
166	159	sub1cncf 15885	. . . . . . . . . . . 12 |- (1 e. CC -> {<.w, z>. | (w e. CC /\ z = (w - 1))} e. (CC-cn->CC))
167	108, 166	ax-mp 7	. . . . . . . . . . 11 |- {<.w, z>. | (w e. CC /\ z = (w - 1))} e. (CC-cn->CC)
168	165, 167	pm3.2i 307	. . . . . . . . . 10 |- ({<.x, v>. | (x e. CC /\ v = (2 x. x))} e. (CC-cn->CC) /\ {<.w, z>. | (w e. CC /\ z = (w - 1))} e. (CC-cn->CC))
169		cncfco 15887	. . . . . . . . . 10 |- (((CC C_ CC /\ CC C_ CC /\ CC C_ CC) /\ ({<.x, v>. | (x e. CC /\ v = (2 x. x))} e. (CC-cn->CC) /\ {<.w, z>. | (w e. CC /\ z = (w - 1))} e. (CC-cn->CC))) -> ({<.w, z>. | (w e. CC /\ z = (w - 1))} o. {<.x, v>. | (x e. CC /\ v = (2 x. x))}) e. (CC-cn->CC))
170	163, 168, 169	mp2an 761	. . . . . . . . 9 |- ({<.w, z>. | (w e. CC /\ z = (w - 1))} o. {<.x, v>. | (x e. CC /\ v = (2 x. x))}) e. (CC-cn->CC)
171	161, 170	eqeltrri 1968	. . . . . . . 8 |- {<.x, y>. | (x e. CC /\ y = ((2 x. x) - 1))} e. (CC-cn->CC)
172		eqid 1884	. . . . . . . . . . 11 |- (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))) = (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))
173		eqid 1884	. . . . . . . . . . 11 |- (Open` (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))) = (Open` (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))))
174	172, 131, 133, 173	subtopmet 10256	. . . . . . . . . 10 |- ((((abs o. - ) |` (RR X. RR)) e. Met /\ ((1 / 2)[,]1) C_ RR) -> (subSp` <.((1 / 2)[,]1), (topGen` ran (,))>.) = (Open` (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))))
175	129, 147, 174	mp2an 761	. . . . . . . . 9 |- (subSp` <.((1 / 2)[,]1), (topGen` ran (,))>.) = (Open` (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))))
176		xpss12 4089	. . . . . . . . . . . 12 |- ((((1 / 2)[,]1) C_ RR /\ ((1 / 2)[,]1) C_ RR) -> (((1 / 2)[,]1) X. ((1 / 2)[,]1)) C_ (RR X. RR))
177	176	anidms 480	. . . . . . . . . . 11 |- (((1 / 2)[,]1) C_ RR -> (((1 / 2)[,]1) X. ((1 / 2)[,]1)) C_ (RR X. RR))
178	147, 177	ax-mp 7	. . . . . . . . . 10 |- (((1 / 2)[,]1) X. ((1 / 2)[,]1)) C_ (RR X. RR)
179		resabs1 4244	. . . . . . . . . . 11 |- ((((1 / 2)[,]1) X. ((1 / 2)[,]1)) C_ (RR X. RR) -> (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))) = ((abs o. - ) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))))
180	179	fveq2d 4685	. . . . . . . . . 10 |- ((((1 / 2)[,]1) X. ((1 / 2)[,]1)) C_ (RR X. RR) -> (Open` (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))) = (Open` ((abs o. - ) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))))
181	178, 180	ax-mp 7	. . . . . . . . 9 |- (Open` (((abs o. - ) |` (RR X. RR)) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1)))) = (Open` ((abs o. - ) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))))
182	175, 181	eqtri 1908	. . . . . . . 8 |- (subSp` <.((1 / 2)[,]1), (topGen` ran (,))>.) = (Open` ((abs o. - ) |` (((1 / 2)[,]1) X. ((1 / 2)[,]1))))
183	148, 123, 149, 116, 54, 171, 182, 144	cncfres 15895	. . . . . . 7 |- {<.x, y>. | (x e. ((1 / 2)[,]1) /\ y = ((2 x. x) - 1))} e. ((subSp` <.((1 / 2)[,]1), (topGen` ran (,))>.) Cn II)
184	17, 18, 97, 98, 99, 68, 100, 101, 102, 114, 115, 116, 10, 145, 183	piececn 15894	. . . . . 6 |- {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))} e. (II Cn II)
185		breq1 3341	. . . . . . . . . . 11 |- (x = 0 -> (x <_ (1 / 2) <-> 0 <_ (1 / 2)))
186	185	ifbid 2996	. . . . . . . . . 10 |- (x = 0 -> if(x <_ (1 / 2), 0, ((2 x. x) - 1)) = if(0 <_ (1 / 2), 0, ((2 x. x) - 1)))
187		opreq2 4890	. . . . . . . . . . . 12 |- (x = 0 -> (2 x. x) = (2 x. 0))
188	187	opreq1d 4897	. . . . . . . . . . 11 |- (x = 0 -> ((2 x. x) - 1) = ((2 x. 0) - 1))
189	188	ifeq2d 2994	. . . . . . . . . 10 |- (x = 0 -> if(0 <_ (1 / 2), 0, ((2 x. x) - 1)) = if(0 <_ (1 / 2), 0, ((2 x. 0) - 1)))
190	186, 189	eqtrd 1925	. . . . . . . . 9 |- (x = 0 -> if(x <_ (1 / 2), 0, ((2 x. x) - 1)) = if(0 <_ (1 / 2), 0, ((2 x. 0) - 1)))
191		oprex 4907	. . . . . . . . . 10 |- ((2 x. 0) - 1) e. _V
192	98, 191	ifex 3031	. . . . . . . . 9 |- if(0 <_ (1 / 2), 0, ((2 x. 0) - 1)) e. _V
193	190, 68, 192	fvopab4 4743	. . . . . . . 8 |- (0 e. (0[,]1) -> ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 0) = if(0 <_ (1 / 2), 0, ((2 x. 0) - 1)))
194	22, 193	ax-mp 7	. . . . . . 7 |- ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 0) = if(0 <_ (1 / 2), 0, ((2 x. 0) - 1))
195		iftrue 2989	. . . . . . . 8 |- (0 <_ (1 / 2) -> if(0 <_ (1 / 2), 0, ((2 x. 0) - 1)) = 0)
196	94, 195	ax-mp 7	. . . . . . 7 |- if(0 <_ (1 / 2), 0, ((2 x. 0) - 1)) = 0
197	194, 196	eqtri 1908	. . . . . 6 |- ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 0) = 0
198		breq1 3341	. . . . . . . . . . 11 |- (x = 1 -> (x <_ (1 / 2) <-> 1 <_ (1 / 2)))
199	198	ifbid 2996	. . . . . . . . . 10 |- (x = 1 -> if(x <_ (1 / 2), 0, ((2 x. x) - 1)) = if(1 <_ (1 / 2), 0, ((2 x. x) - 1)))
200		opreq2 4890	. . . . . . . . . . . 12 |- (x = 1 -> (2 x. x) = (2 x. 1))
201	200	opreq1d 4897	. . . . . . . . . . 11 |- (x = 1 -> ((2 x. x) - 1) = ((2 x. 1) - 1))
202	201	ifeq2d 2994	. . . . . . . . . 10 |- (x = 1 -> if(1 <_ (1 / 2), 0, ((2 x. x) - 1)) = if(1 <_ (1 / 2), 0, ((2 x. 1) - 1)))
203	199, 202	eqtrd 1925	. . . . . . . . 9 |- (x = 1 -> if(x <_ (1 / 2), 0, ((2 x. x) - 1)) = if(1 <_ (1 / 2), 0, ((2 x. 1) - 1)))
204		oprex 4907	. . . . . . . . . 10 |- ((2 x. 1) - 1) e. _V
205	98, 204	ifex 3031	. . . . . . . . 9 |- if(1 <_ (1 / 2), 0, ((2 x. 1) - 1)) e. _V
206	203, 68, 205	fvopab4 4743	. . . . . . . 8 |- (1 e. (0[,]1) -> ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 1) = if(1 <_ (1 / 2), 0, ((2 x. 1) - 1)))
207	31, 206	ax-mp 7	. . . . . . 7 |- ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 1) = if(1 <_ (1 / 2), 0, ((2 x. 1) - 1))
208	45, 18	ltnlei 6754	. . . . . . . . 9 |- ((1 / 2) < 1 <-> -. 1 <_ (1 / 2))
209	95, 208	mpbi 206	. . . . . . . 8 |- -. 1 <_ (1 / 2)
210		iffalse 2991	. . . . . . . 8 |- (-. 1 <_ (1 / 2) -> if(1 <_ (1 / 2), 0, ((2 x. 1) - 1)) = ((2 x. 1) - 1))
211	209, 210	ax-mp 7	. . . . . . 7 |- if(1 <_ (1 / 2), 0, ((2 x. 1) - 1)) = ((2 x. 1) - 1)
212	105, 108	mulcli 6474	. . . . . . . 8 |- (2 x. 1) e. CC
213	108	2timesi 7187	. . . . . . . . 9 |- (2 x. 1) = (1 + 1)
214	213	eqcomi 1888	. . . . . . . 8 |- (1 + 1) = (2 x. 1)
215	212, 108, 108, 214	subaddrii 6529	. . . . . . 7 |- ((2 x. 1) - 1) = 1
216	207, 211, 215	3eqtri 1912	. . . . . 6 |- ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 1) = 1
217	184, 197, 216	3pm3.2i 1048	. . . . 5 |- ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))} e. (II Cn II) /\ ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 0) = 0 /\ ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 1) = 1)
218		reparpht 16065	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))} e. (II Cn II) /\ ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 0) = 0 /\ ({<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))}` 1) = 1)) -> (F o. {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))})(~=ph` J)F)
219	217, 218	mpan2 760	. . . 4 |- ((J e. Top /\ F e. (II Cn J)) -> (F o. {<.x, y>. | (x e. (0[,]1) /\ y = if(x <_ (1 / 2), 0, ((2 x. x) - 1)))})(~=ph` J)F)
220	90, 219	eqbrtrd 3357	. . 3 |- ((J e. Top /\ F e. (II Cn J)) -> (((0[,]1) X. {(F` 0)})(*p` J)F)(~=ph` J)F)
221	220	3adant3 896	. 2 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> (((0[,]1) X. {(F` 0)})(*p` J)F)(~=ph` J)F)
222	8, 221	eqbrtrd 3357	1 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 0) = Y) -> (P(*p` J)F)(~=ph` J)F)

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

This theorem is referenced by:  pi1gp 16095

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  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-phtpy 16045  df-phtpc 16057  df-pco 16069

Copyright terms: Public domain