Theorem phtpycom 16050

Description: Given a homotopy from F to G, produce a homotopy from G to F.

Hypothesis

Ref	Expression
phtpycom.1	|- K = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (xH(1 - y)))}

Assertion

Ref	Expression
phtpycom	|- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> (H e. (F(PHtpy` J)G) -> K e. (G(PHtpy` J)F)))

Distinct variable groups:   x,J,y,z   x,F,y,z   x,H,y,z   x,G,y,z

Proof of Theorem phtpycom

Step	Hyp	Ref	Expression
1		iitop 15867	. . . . . . . . . 10 |- II e. Top
2		eqid 1884	. . . . . . . . . . 11 |- (II X.t II) = (II X.t II)
3	2	txtop 8934	. . . . . . . . . 10 |- ((II e. Top /\ II e. Top) -> (II X.t II) e. Top)
4	1, 1, 3	mp2an 761	. . . . . . . . 9 |- (II X.t II) e. Top
5		iiuni 15868	. . . . . . . . . . . . 13 |- (0[,]1) = U.II
6	2, 5, 5	txuni 8935	. . . . . . . . . . . 12 |- ((II e. Top /\ II e. Top) -> U.(II X.t II) = ((0[,]1) X. (0[,]1)))
7	1, 1, 6	mp2an 761	. . . . . . . . . . 11 |- U.(II X.t II) = ((0[,]1) X. (0[,]1))
8	7	eqcomi 1888	. . . . . . . . . 10 |- ((0[,]1) X. (0[,]1)) = U.(II X.t II)
9		eqid 1884	. . . . . . . . . 10 |- U.J = U.J
10	8, 9	cnf 9038	. . . . . . . . 9 |- (((II X.t II) e. Top /\ J e. Top /\ H e. ((II X.t II) Cn J)) -> H:((0[,]1) X. (0[,]1))-->U.J)
11	4, 10	mp3an1 1178	. . . . . . . 8 |- ((J e. Top /\ H e. ((II X.t II) Cn J)) -> H:((0[,]1) X. (0[,]1))-->U.J)
12		ffn 4562	. . . . . . . 8 |- (H:((0[,]1) X. (0[,]1))-->U.J -> H Fn ((0[,]1) X. (0[,]1)))
13		opelxpi 4040	. . . . . . . . . 10 |- ((x e. (0[,]1) /\ (1 - y) e. (0[,]1)) -> <.x, (1 - y)>. e. ((0[,]1) X. (0[,]1)))
14		iirev 15871	. . . . . . . . . 10 |- (y e. (0[,]1) -> (1 - y) e. (0[,]1))
15	13, 14	sylan2 500	. . . . . . . . 9 |- ((x e. (0[,]1) /\ y e. (0[,]1)) -> <.x, (1 - y)>. e. ((0[,]1) X. (0[,]1)))
16		id 73	. . . . . . . . . . . . . . 15 |- (s = x -> s = x)
17		eqid 1884	. . . . . . . . . . . . . . 15 |- {<.s, t>. | (s e. (0[,]1) /\ t = s)} = {<.s, t>. | (s e. (0[,]1) /\ t = s)}
18		visset 2295	. . . . . . . . . . . . . . 15 |- x e. _V
19	16, 17, 18	fvopab4 4743	. . . . . . . . . . . . . 14 |- (x e. (0[,]1) -> ({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x) = x)
20	19	adantr 425	. . . . . . . . . . . . 13 |- ((x e. (0[,]1) /\ y e. (0[,]1)) -> ({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x) = x)
21		opreq2 4890	. . . . . . . . . . . . . . 15 |- (s = y -> (1 - s) = (1 - y))
22		eqid 1884	. . . . . . . . . . . . . . 15 |- {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))} = {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}
23		oprex 4907	. . . . . . . . . . . . . . 15 |- (1 - y) e. _V
24	21, 22, 23	fvopab4 4743	. . . . . . . . . . . . . 14 |- (y e. (0[,]1) -> ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y) = (1 - y))
25	24	adantl 424	. . . . . . . . . . . . 13 |- ((x e. (0[,]1) /\ y e. (0[,]1)) -> ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y) = (1 - y))
26	20, 25	opeq12d 3166	. . . . . . . . . . . 12 |- ((x e. (0[,]1) /\ y e. (0[,]1)) -> <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>. = <.x, (1 - y)>.)
27	26	eqeq2d 1895	. . . . . . . . . . 11 |- ((x e. (0[,]1) /\ y e. (0[,]1)) -> (w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>. <-> w = <.x, (1 - y)>.))
28	27	pm5.32i 707	. . . . . . . . . 10 |- (((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.) <-> ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.x, (1 - y)>.))
29	28	oprabbii 4923	. . . . . . . . 9 |- {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)} = {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.x, (1 - y)>.)}
30		phtpycom.1	. . . . . . . . . 10 |- K = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (xH(1 - y)))}
31		df-opr 4886	. . . . . . . . . . . . 13 |- (xH(1 - y)) = (H` <.x, (1 - y)>.)
32	31	eqeq2i 1894	. . . . . . . . . . . 12 |- (z = (xH(1 - y)) <-> z = (H` <.x, (1 - y)>.))
33	32	anbi2i 538	. . . . . . . . . . 11 |- (((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (xH(1 - y))) <-> ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (H` <.x, (1 - y)>.)))
34	33	oprabbii 4923	. . . . . . . . . 10 |- {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (xH(1 - y)))} = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (H` <.x, (1 - y)>.))}
35	30, 34	eqtri 1908	. . . . . . . . 9 |- K = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (H` <.x, (1 - y)>.))}
36	15, 29, 35	oprabco 10159	. . . . . . . 8 |- (H Fn ((0[,]1) X. (0[,]1)) -> K = (H o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)}))
37	11, 12, 36	3syl 24	. . . . . . 7 |- ((J e. Top /\ H e. ((II X.t II) Cn J)) -> K = (H o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)}))
38	4	a1i 8	. . . . . . . 8 |- ((J e. Top /\ H e. ((II X.t II) Cn J)) -> (II X.t II) e. Top)
39		simpl 346	. . . . . . . 8 |- ((J e. Top /\ H e. ((II X.t II) Cn J)) -> J e. Top)
40		simpr 350	. . . . . . . . 9 |- ((J e. Top /\ H e. ((II X.t II) Cn J)) -> H e. ((II X.t II) Cn J))
41	1, 1	pm3.2i 307	. . . . . . . . . 10 |- (II e. Top /\ II e. Top)
42		df-id 3586	. . . . . . . . . . . . . . 15 |- _I = {<.s, t>. | s = t}
43		equcom 1488	. . . . . . . . . . . . . . . 16 |- (s = t <-> t = s)
44	43	opabbii 3402	. . . . . . . . . . . . . . 15 |- {<.s, t>. | s = t} = {<.s, t>. | t = s}
45	42, 44	eqtri 1908	. . . . . . . . . . . . . 14 |- _I = {<.s, t>. | t = s}
46		reseq1 4218	. . . . . . . . . . . . . 14 |- ( _I = {<.s, t>. | t = s} -> ( _I |` (0[,]1)) = ({<.s, t>. | t = s} |` (0[,]1)))
47	45, 46	ax-mp 7	. . . . . . . . . . . . 13 |- ( _I |` (0[,]1)) = ({<.s, t>. | t = s} |` (0[,]1))
48		resopab 4252	. . . . . . . . . . . . 13 |- ({<.s, t>. | t = s} |` (0[,]1)) = {<.s, t>. | (s e. (0[,]1) /\ t = s)}
49	47, 48	eqtr2i 1909	. . . . . . . . . . . 12 |- {<.s, t>. | (s e. (0[,]1) /\ t = s)} = ( _I |` (0[,]1))
50	5	idcn 9042	. . . . . . . . . . . . 13 |- (II e. Top -> ( _I |` (0[,]1)) e. (II Cn II))
51	1, 50	ax-mp 7	. . . . . . . . . . . 12 |- ( _I |` (0[,]1)) e. (II Cn II)
52	49, 51	eqeltri 1967	. . . . . . . . . . 11 |- {<.s, t>. | (s e. (0[,]1) /\ t = s)} e. (II Cn II)
53		0re 6603	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
54		1re 6598	. . . . . . . . . . . . . . . . 17 |- 1 e. RR
55		iccssre 7565	. . . . . . . . . . . . . . . . 17 |- ((0 e. RR /\ 1 e. RR) -> (0[,]1) C_ RR)
56	53, 54, 55	mp2an 761	. . . . . . . . . . . . . . . 16 |- (0[,]1) C_ RR
57		axresscn 6420	. . . . . . . . . . . . . . . 16 |- RR C_ CC
58	56, 57	sstri 2626	. . . . . . . . . . . . . . 15 |- (0[,]1) C_ CC
59		ssid 2634	. . . . . . . . . . . . . . 15 |- CC C_ CC
60	58, 59, 58	3pm3.2i 1048	. . . . . . . . . . . . . 14 |- ((0[,]1) C_ CC /\ CC C_ CC /\ (0[,]1) C_ CC)
61		opreq2 4890	. . . . . . . . . . . . . . . . 17 |- (s = w -> (1 - s) = (1 - w))
62		oprex 4907	. . . . . . . . . . . . . . . . 17 |- (1 - w) e. _V
63	61, 22, 62	fvopab4 4743	. . . . . . . . . . . . . . . 16 |- (w e. (0[,]1) -> ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` w) = (1 - w))
64		iirev 15871	. . . . . . . . . . . . . . . 16 |- (w e. (0[,]1) -> (1 - w) e. (0[,]1))
65	63, 64	eqeltrd 1971	. . . . . . . . . . . . . . 15 |- (w e. (0[,]1) -> ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` w) e. (0[,]1))
66	65	rgen 2159	. . . . . . . . . . . . . 14 |- A.w e. (0[,]1)({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` w) e. (0[,]1)
67	60, 66	pm3.2i 307	. . . . . . . . . . . . 13 |- (((0[,]1) C_ CC /\ CC C_ CC /\ (0[,]1) C_ CC) /\ A.w e. (0[,]1)({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` w) e. (0[,]1))
68		resopab2 4256	. . . . . . . . . . . . . . 15 |- ((0[,]1) C_ CC -> ({<.s, t>. | (s e. CC /\ t = (1 - s))} |` (0[,]1)) = {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))})
69	58, 68	ax-mp 7	. . . . . . . . . . . . . 14 |- ({<.s, t>. | (s e. CC /\ t = (1 - s))} |` (0[,]1)) = {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}
70		ax1cn 6422	. . . . . . . . . . . . . . . 16 |- 1 e. CC
71		eqid 1884	. . . . . . . . . . . . . . . . 17 |- {<.s, t>. | (s e. CC /\ t = (1 - s))} = {<.s, t>. | (s e. CC /\ t = (1 - s))}
72	71	sub2cncf 15886	. . . . . . . . . . . . . . . 16 |- (1 e. CC -> {<.s, t>. | (s e. CC /\ t = (1 - s))} e. (CC-cn->CC))
73	70, 72	ax-mp 7	. . . . . . . . . . . . . . 15 |- {<.s, t>. | (s e. CC /\ t = (1 - s))} e. (CC-cn->CC)
74		rescncf 8534	. . . . . . . . . . . . . . . 16 |- ((CC C_ CC /\ CC C_ CC /\ (0[,]1) C_ CC) -> ({<.s, t>. | (s e. CC /\ t = (1 - s))} e. (CC-cn->CC) -> ({<.s, t>. | (s e. CC /\ t = (1 - s))} |` (0[,]1)) e. ((0[,]1)-cn->CC)))
75	59, 59, 58, 74	mp3an 1191	. . . . . . . . . . . . . . 15 |- ({<.s, t>. | (s e. CC /\ t = (1 - s))} e. (CC-cn->CC) -> ({<.s, t>. | (s e. CC /\ t = (1 - s))} |` (0[,]1)) e. ((0[,]1)-cn->CC))
76	73, 75	ax-mp 7	. . . . . . . . . . . . . 14 |- ({<.s, t>. | (s e. CC /\ t = (1 - s))} |` (0[,]1)) e. ((0[,]1)-cn->CC)
77	69, 76	eqeltrri 1968	. . . . . . . . . . . . 13 |- {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))} e. ((0[,]1)-cn->CC)
78		cncffvrn 8535	. . . . . . . . . . . . 13 |- ((((0[,]1) C_ CC /\ CC C_ CC /\ (0[,]1) C_ CC) /\ A.w e. (0[,]1)({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` w) e. (0[,]1)) -> ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))} e. ((0[,]1)-cn->CC) -> {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))} e. ((0[,]1)-cn->(0[,]1))))
79	67, 77, 78	mp2 54	. . . . . . . . . . . 12 |- {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))} e. ((0[,]1)-cn->(0[,]1))
80		eqid 1884	. . . . . . . . . . . . . 14 |- ((abs o. - ) |` ((0[,]1) X. (0[,]1))) = ((abs o. - ) |` ((0[,]1) X. (0[,]1)))
81		df-ii 15866	. . . . . . . . . . . . . 14 |- II = (Open` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
82	80, 80, 81, 81	cncfmet 9183	. . . . . . . . . . . . 13 |- (((0[,]1) C_ CC /\ (0[,]1) C_ CC) -> ((0[,]1)-cn->(0[,]1)) = (II Cn II))
83	58, 58, 82	mp2an 761	. . . . . . . . . . . 12 |- ((0[,]1)-cn->(0[,]1)) = (II Cn II)
84	79, 83	eleqtri 1969	. . . . . . . . . . 11 |- {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))} e. (II Cn II)
85	52, 84	pm3.2i 307	. . . . . . . . . 10 |- ({<.s, t>. | (s e. (0[,]1) /\ t = s)} e. (II Cn II) /\ {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))} e. (II Cn II))
86		eqid 1884	. . . . . . . . . . 11 |- {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)} = {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)}
87	2, 2, 5, 5, 86	2txcn 10229	. . . . . . . . . 10 |- (((II e. Top /\ II e. Top) /\ (II e. Top /\ II e. Top) /\ ({<.s, t>. | (s e. (0[,]1) /\ t = s)} e. (II Cn II) /\ {<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))} e. (II Cn II))) -> {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)} e. ((II X.t II) Cn (II X.t II)))
88	41, 41, 85, 87	mp3an 1191	. . . . . . . . 9 |- {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)} e. ((II X.t II) Cn (II X.t II))
89	40, 88	jctil 316	. . . . . . . 8 |- ((J e. Top /\ H e. ((II X.t II) Cn J)) -> ({<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)} e. ((II X.t II) Cn (II X.t II)) /\ H e. ((II X.t II) Cn J)))
90		cnco 9045	. . . . . . . 8 |- ((((II X.t II) e. Top /\ (II X.t II) e. Top /\ J e. Top) /\ ({<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)} e. ((II X.t II) Cn (II X.t II)) /\ H e. ((II X.t II) Cn J))) -> (H o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)}) e. ((II X.t II) Cn J))
91	38, 38, 39, 89, 90	syl31anc 1103	. . . . . . 7 |- ((J e. Top /\ H e. ((II X.t II) Cn J)) -> (H o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = <.({<.s, t>. | (s e. (0[,]1) /\ t = s)}` x), ({<.s, t>. | (s e. (0[,]1) /\ t = (1 - s))}` y)>.)}) e. ((II X.t II) Cn J))
92	37, 91	eqeltrd 1971	. . . . . 6 |- ((J e. Top /\ H e. ((II X.t II) Cn J)) -> K e. ((II X.t II) Cn J))
93	92	3ad2antl1 1038	. . . . 5 |- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ H e. ((II X.t II) Cn J)) -> K e. ((II X.t II) Cn J))
94	93	ad2ant2r 445	. . . 4 |- ((((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) /\ (H e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))))) -> K e. ((II X.t II) Cn J))
95		opreq1 4889	. . . . . . . . . . . . . . . 16 |- (s = t -> (sH0) = (tH0))
96		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (s = t -> (F` s) = (F` t))
97	95, 96	eqeq12d 1899	. . . . . . . . . . . . . . 15 |- (s = t -> ((sH0) = (F` s) <-> (tH0) = (F` t)))
98		opreq1 4889	. . . . . . . . . . . . . . . 16 |- (s = t -> (sH1) = (tH1))
99		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (s = t -> (G` s) = (G` t))
100	98, 99	eqeq12d 1899	. . . . . . . . . . . . . . 15 |- (s = t -> ((sH1) = (G` s) <-> (tH1) = (G` t)))
101	97, 100	anbi12d 690	. . . . . . . . . . . . . 14 |- (s = t -> (((sH0) = (F` s) /\ (sH1) = (G` s)) <-> ((tH0) = (F` t) /\ (tH1) = (G` t))))
102		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (s = t -> (0Hs) = (0Ht))
103	102	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (s = t -> ((0Hs) = (F` 0) <-> (0Ht) = (F` 0)))
104		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (s = t -> (1Hs) = (1Ht))
105	104	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (s = t -> ((1Hs) = (F` 1) <-> (1Ht) = (F` 1)))
106	103, 105	anbi12d 690	. . . . . . . . . . . . . 14 |- (s = t -> (((0Hs) = (F` 0) /\ (1Hs) = (F` 1)) <-> ((0Ht) = (F` 0) /\ (1Ht) = (F` 1))))
107	101, 106	anbi12d 690	. . . . . . . . . . . . 13 |- (s = t -> ((((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))) <-> (((tH0) = (F` t) /\ (tH1) = (G` t)) /\ ((0Ht) = (F` 0) /\ (1Ht) = (F` 1)))))
108	107	rcla4v 2376	. . . . . . . . . . . 12 |- (t e. (0[,]1) -> (A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))) -> (((tH0) = (F` t) /\ (tH1) = (G` t)) /\ ((0Ht) = (F` 0) /\ (1Ht) = (F` 1)))))
109	108	imdistani 491	. . . . . . . . . . 11 |- ((t e. (0[,]1) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1)))) -> (t e. (0[,]1) /\ (((tH0) = (F` t) /\ (tH1) = (G` t)) /\ ((0Ht) = (F` 0) /\ (1Ht) = (F` 1)))))
110		lt01 6871	. . . . . . . . . . . . . . . . . . . 20 |- 0 < 1
111	53, 54, 110	ltleii 6756	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 1
112		lbicc2 7573	. . . . . . . . . . . . . . . . . . 19 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 0 e. (0[,]1))
113	53, 54, 111, 112	mp3an 1191	. . . . . . . . . . . . . . . . . 18 |- 0 e. (0[,]1)
114		oprex 4907	. . . . . . . . . . . . . . . . . . 19 |- (tH(1 - 0)) e. _V
115		opreq1 4889	. . . . . . . . . . . . . . . . . . 19 |- (x = t -> (xH(1 - y)) = (tH(1 - y)))
116		opreq2 4890	. . . . . . . . . . . . . . . . . . . 20 |- (y = 0 -> (1 - y) = (1 - 0))
117	116	opreq2d 4898	. . . . . . . . . . . . . . . . . . 19 |- (y = 0 -> (tH(1 - y)) = (tH(1 - 0)))
118	114, 115, 117, 30	oprabval2 4957	. . . . . . . . . . . . . . . . . 18 |- ((t e. (0[,]1) /\ 0 e. (0[,]1)) -> (tK0) = (tH(1 - 0)))
119	113, 118	mpan2 760	. . . . . . . . . . . . . . . . 17 |- (t e. (0[,]1) -> (tK0) = (tH(1 - 0)))
120	70	subid1i 6552	. . . . . . . . . . . . . . . . . 18 |- (1 - 0) = 1
121	120	opreq2i 4893	. . . . . . . . . . . . . . . . 17 |- (tH(1 - 0)) = (tH1)
122	119, 121	syl6eq 1944	. . . . . . . . . . . . . . . 16 |- (t e. (0[,]1) -> (tK0) = (tH1))
123	122	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (t e. (0[,]1) -> ((tK0) = (G` t) <-> (tH1) = (G` t)))
124		ubicc2 7574	. . . . . . . . . . . . . . . . . . 19 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 1 e. (0[,]1))
125	53, 54, 111, 124	mp3an 1191	. . . . . . . . . . . . . . . . . 18 |- 1 e. (0[,]1)
126		oprex 4907	. . . . . . . . . . . . . . . . . . 19 |- (tH(1 - 1)) e. _V
127		opreq2 4890	. . . . . . . . . . . . . . . . . . . 20 |- (y = 1 -> (1 - y) = (1 - 1))
128	127	opreq2d 4898	. . . . . . . . . . . . . . . . . . 19 |- (y = 1 -> (tH(1 - y)) = (tH(1 - 1)))
129	126, 115, 128, 30	oprabval2 4957	. . . . . . . . . . . . . . . . . 18 |- ((t e. (0[,]1) /\ 1 e. (0[,]1)) -> (tK1) = (tH(1 - 1)))
130	125, 129	mpan2 760	. . . . . . . . . . . . . . . . 17 |- (t e. (0[,]1) -> (tK1) = (tH(1 - 1)))
131	70	subidi 6551	. . . . . . . . . . . . . . . . . 18 |- (1 - 1) = 0
132	131	opreq2i 4893	. . . . . . . . . . . . . . . . 17 |- (tH(1 - 1)) = (tH0)
133	130, 132	syl6eq 1944	. . . . . . . . . . . . . . . 16 |- (t e. (0[,]1) -> (tK1) = (tH0))
134	133	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (t e. (0[,]1) -> ((tK1) = (F` t) <-> (tH0) = (F` t)))
135	123, 134	anbi12d 690	. . . . . . . . . . . . . 14 |- (t e. (0[,]1) -> (((tK0) = (G` t) /\ (tK1) = (F` t)) <-> ((tH1) = (G` t) /\ (tH0) = (F` t))))
136	135	biimpar 461	. . . . . . . . . . . . 13 |- ((t e. (0[,]1) /\ ((tH1) = (G` t) /\ (tH0) = (F` t))) -> ((tK0) = (G` t) /\ (tK1) = (F` t)))
137	136	ancom2s 545	. . . . . . . . . . . 12 |- ((t e. (0[,]1) /\ ((tH0) = (F` t) /\ (tH1) = (G` t))) -> ((tK0) = (G` t) /\ (tK1) = (F` t)))
138	137	adantrr 431	. . . . . . . . . . 11 |- ((t e. (0[,]1) /\ (((tH0) = (F` t) /\ (tH1) = (G` t)) /\ ((0Ht) = (F` 0) /\ (1Ht) = (F` 1)))) -> ((tK0) = (G` t) /\ (tK1) = (F` t)))
139	109, 138	syl 12	. . . . . . . . . 10 |- ((t e. (0[,]1) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1)))) -> ((tK0) = (G` t) /\ (tK1) = (F` t)))
140	139	adantl 424	. . . . . . . . 9 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ (t e. (0[,]1) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))))) -> ((tK0) = (G` t) /\ (tK1) = (F` t)))
141		oprex 4907	. . . . . . . . . . . . . . . . . . 19 |- (0H(1 - t)) e. _V
142		opreq1 4889	. . . . . . . . . . . . . . . . . . 19 |- (x = 0 -> (xH(1 - y)) = (0H(1 - y)))
143		opreq2 4890	. . . . . . . . . . . . . . . . . . . 20 |- (y = t -> (1 - y) = (1 - t))
144	143	opreq2d 4898	. . . . . . . . . . . . . . . . . . 19 |- (y = t -> (0H(1 - y)) = (0H(1 - t)))
145	141, 142, 144, 30	oprabval2 4957	. . . . . . . . . . . . . . . . . 18 |- ((0 e. (0[,]1) /\ t e. (0[,]1)) -> (0Kt) = (0H(1 - t)))
146	113, 145	mpan 759	. . . . . . . . . . . . . . . . 17 |- (t e. (0[,]1) -> (0Kt) = (0H(1 - t)))
147	146	ad2antlr 441	. . . . . . . . . . . . . . . 16 |- ((((F` 0) = (G` 0) /\ t e. (0[,]1)) /\ (0H(1 - t)) = (F` 0)) -> (0Kt) = (0H(1 - t)))
148		eqtr 1904	. . . . . . . . . . . . . . . . . 18 |- (((0H(1 - t)) = (F` 0) /\ (F` 0) = (G` 0)) -> (0H(1 - t)) = (G` 0))
149	148	ancoms 484	. . . . . . . . . . . . . . . . 17 |- (((F` 0) = (G` 0) /\ (0H(1 - t)) = (F` 0)) -> (0H(1 - t)) = (G` 0))
150	149	adantlr 429	. . . . . . . . . . . . . . . 16 |- ((((F` 0) = (G` 0) /\ t e. (0[,]1)) /\ (0H(1 - t)) = (F` 0)) -> (0H(1 - t)) = (G` 0))
151	147, 150	eqtrd 1925	. . . . . . . . . . . . . . 15 |- ((((F` 0) = (G` 0) /\ t e. (0[,]1)) /\ (0H(1 - t)) = (F` 0)) -> (0Kt) = (G` 0))
152	151	adantrr 431	. . . . . . . . . . . . . 14 |- ((((F` 0) = (G` 0) /\ t e. (0[,]1)) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1))) -> (0Kt) = (G` 0))
153	152	adantllr 433	. . . . . . . . . . . . 13 |- (((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ t e. (0[,]1)) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1))) -> (0Kt) = (G` 0))
154		oprex 4907	. . . . . . . . . . . . . . . . . . 19 |- (1H(1 - t)) e. _V
155		opreq1 4889	. . . . . . . . . . . . . . . . . . 19 |- (x = 1 -> (xH(1 - y)) = (1H(1 - y)))
156	143	opreq2d 4898	. . . . . . . . . . . . . . . . . . 19 |- (y = t -> (1H(1 - y)) = (1H(1 - t)))
157	154, 155, 156, 30	oprabval2 4957	. . . . . . . . . . . . . . . . . 18 |- ((1 e. (0[,]1) /\ t e. (0[,]1)) -> (1Kt) = (1H(1 - t)))
158	125, 157	mpan 759	. . . . . . . . . . . . . . . . 17 |- (t e. (0[,]1) -> (1Kt) = (1H(1 - t)))
159	158	ad2antlr 441	. . . . . . . . . . . . . . . 16 |- ((((F` 1) = (G` 1) /\ t e. (0[,]1)) /\ (1H(1 - t)) = (F` 1)) -> (1Kt) = (1H(1 - t)))
160		eqtr 1904	. . . . . . . . . . . . . . . . . 18 |- (((1H(1 - t)) = (F` 1) /\ (F` 1) = (G` 1)) -> (1H(1 - t)) = (G` 1))
161	160	ancoms 484	. . . . . . . . . . . . . . . . 17 |- (((F` 1) = (G` 1) /\ (1H(1 - t)) = (F` 1)) -> (1H(1 - t)) = (G` 1))
162	161	adantlr 429	. . . . . . . . . . . . . . . 16 |- ((((F` 1) = (G` 1) /\ t e. (0[,]1)) /\ (1H(1 - t)) = (F` 1)) -> (1H(1 - t)) = (G` 1))
163	159, 162	eqtrd 1925	. . . . . . . . . . . . . . 15 |- ((((F` 1) = (G` 1) /\ t e. (0[,]1)) /\ (1H(1 - t)) = (F` 1)) -> (1Kt) = (G` 1))
164	163	adantrl 430	. . . . . . . . . . . . . 14 |- ((((F` 1) = (G` 1) /\ t e. (0[,]1)) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1))) -> (1Kt) = (G` 1))
165	164	adantlll 432	. . . . . . . . . . . . 13 |- (((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ t e. (0[,]1)) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1))) -> (1Kt) = (G` 1))
166	153, 165	jca 310	. . . . . . . . . . . 12 |- (((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ t e. (0[,]1)) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1))) -> ((0Kt) = (G` 0) /\ (1Kt) = (G` 1)))
167	166	adantrl 430	. . . . . . . . . . 11 |- (((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ t e. (0[,]1)) /\ ((((1 - t)H0) = (F` (1 - t)) /\ ((1 - t)H1) = (G` (1 - t))) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1)))) -> ((0Kt) = (G` 0) /\ (1Kt) = (G` 1)))
168	167	anasss 488	. . . . . . . . . 10 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ (t e. (0[,]1) /\ ((((1 - t)H0) = (F` (1 - t)) /\ ((1 - t)H1) = (G` (1 - t))) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1))))) -> ((0Kt) = (G` 0) /\ (1Kt) = (G` 1)))
169		iirev 15871	. . . . . . . . . . . 12 |- (t e. (0[,]1) -> (1 - t) e. (0[,]1))
170		opreq1 4889	. . . . . . . . . . . . . . . 16 |- (s = (1 - t) -> (sH0) = ((1 - t)H0))
171		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (s = (1 - t) -> (F` s) = (F` (1 - t)))
172	170, 171	eqeq12d 1899	. . . . . . . . . . . . . . 15 |- (s = (1 - t) -> ((sH0) = (F` s) <-> ((1 - t)H0) = (F` (1 - t))))
173		opreq1 4889	. . . . . . . . . . . . . . . 16 |- (s = (1 - t) -> (sH1) = ((1 - t)H1))
174		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (s = (1 - t) -> (G` s) = (G` (1 - t)))
175	173, 174	eqeq12d 1899	. . . . . . . . . . . . . . 15 |- (s = (1 - t) -> ((sH1) = (G` s) <-> ((1 - t)H1) = (G` (1 - t))))
176	172, 175	anbi12d 690	. . . . . . . . . . . . . 14 |- (s = (1 - t) -> (((sH0) = (F` s) /\ (sH1) = (G` s)) <-> (((1 - t)H0) = (F` (1 - t)) /\ ((1 - t)H1) = (G` (1 - t)))))
177		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (s = (1 - t) -> (0Hs) = (0H(1 - t)))
178	177	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (s = (1 - t) -> ((0Hs) = (F` 0) <-> (0H(1 - t)) = (F` 0)))
179		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (s = (1 - t) -> (1Hs) = (1H(1 - t)))
180	179	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (s = (1 - t) -> ((1Hs) = (F` 1) <-> (1H(1 - t)) = (F` 1)))
181	178, 180	anbi12d 690	. . . . . . . . . . . . . 14 |- (s = (1 - t) -> (((0Hs) = (F` 0) /\ (1Hs) = (F` 1)) <-> ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1))))
182	176, 181	anbi12d 690	. . . . . . . . . . . . 13 |- (s = (1 - t) -> ((((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))) <-> ((((1 - t)H0) = (F` (1 - t)) /\ ((1 - t)H1) = (G` (1 - t))) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1)))))
183	182	rcla4v 2376	. . . . . . . . . . . 12 |- ((1 - t) e. (0[,]1) -> (A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))) -> ((((1 - t)H0) = (F` (1 - t)) /\ ((1 - t)H1) = (G` (1 - t))) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1)))))
184	169, 183	syl 12	. . . . . . . . . . 11 |- (t e. (0[,]1) -> (A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))) -> ((((1 - t)H0) = (F` (1 - t)) /\ ((1 - t)H1) = (G` (1 - t))) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1)))))
185	184	imdistani 491	. . . . . . . . . 10 |- ((t e. (0[,]1) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1)))) -> (t e. (0[,]1) /\ ((((1 - t)H0) = (F` (1 - t)) /\ ((1 - t)H1) = (G` (1 - t))) /\ ((0H(1 - t)) = (F` 0) /\ (1H(1 - t)) = (F` 1)))))
186	168, 185	sylan2 500	. . . . . . . . 9 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ (t e. (0[,]1) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))))) -> ((0Kt) = (G` 0) /\ (1Kt) = (G` 1)))
187	140, 186	jca 310	. . . . . . . 8 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ (t e. (0[,]1) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))))) -> (((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1))))
188	187	ancom2s 545	. . . . . . 7 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ (A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))) /\ t e. (0[,]1))) -> (((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1))))
189	188	anassrs 489	. . . . . 6 |- (((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1)))) /\ t e. (0[,]1)) -> (((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1))))
190	189	r19.21aiva 2176	. . . . 5 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1)))) -> A.t e. (0[,]1)(((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1))))
191	190	ad2ant2l 444	. . . 4 |- ((((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) /\ (H e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))))) -> A.t e. (0[,]1)(((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1))))
192	94, 191	jca 310	. . 3 |- ((((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) /\ (H e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))))) -> (K e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1)))))
193	192	ex 402	. 2 |- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> ((H e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1)))) -> (K e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1))))))
194		isphtpy 16048	. 2 |- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> (H e. (F(PHtpy` J)G) <-> (H e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sH0) = (F` s) /\ (sH1) = (G` s)) /\ ((0Hs) = (F` 0) /\ (1Hs) = (F` 1))))))
195		isphtpy 16048	. . 3 |- (((J e. Top /\ G e. (II Cn J) /\ F e. (II Cn J)) /\ ((G` 0) = (F` 0) /\ (G` 1) = (F` 1))) -> (K e. (G(PHtpy` J)F) <-> (K e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1))))))
196		simp1 876	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) -> J e. Top)
197		simp3 878	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) -> G e. (II Cn J))
198		simp2 877	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) -> F e. (II Cn J))
199	196, 197, 198	3jca 1050	. . 3 |- ((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) -> (J e. Top /\ G e. (II Cn J) /\ F e. (II Cn J)))
200		eqcom 1886	. . . . 5 |- ((F` 0) = (G` 0) <-> (G` 0) = (F` 0))
201		eqcom 1886	. . . . 5 |- ((F` 1) = (G` 1) <-> (G` 1) = (F` 1))
202	200, 201	anbi12i 540	. . . 4 |- (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) <-> ((G` 0) = (F` 0) /\ (G` 1) = (F` 1)))
203	202	biimpi 168	. . 3 |- (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) -> ((G` 0) = (F` 0) /\ (G` 1) = (F` 1)))
204	195, 199, 203	syl2an 503	. 2 |- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> (K e. (G(PHtpy` J)F) <-> (K e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tK0) = (G` t) /\ (tK1) = (F` t)) /\ ((0Kt) = (G` 0) /\ (1Kt) = (G` 1))))))
205	193, 194, 204	3imtr4d 602	1 |- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> (H e. (F(PHtpy` J)G) -> K e. (G(PHtpy` J)F)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105   C_ wss 2593  <.cop 3046  U.cuni 3177   class class class wbr 3338  {copab 3395   _I cid 3582   X. cxp 3984   |` cres 3988   o. ccom 3990   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  {copab2 4885  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   - cmin 6445   <_ cle 6448  [,]cicc 7527  abscabs 8000  -cn->ccncf 8524  Topctop 8857   X.t ctx 8930   Cn ccn 9028  IIcii 15865  PHtpycphtpy 16043

This theorem is referenced by:  phtpcer 16062

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-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-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-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-icc 7531  df-seq1 7721  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-cncf 8525  df-top 8861  df-bases 8863  df-topgen 8864  df-tx 8931  df-cn 9030  df-cnp 9031  df-met 9070  df-bl 9072  df-opn 9073  df-ii 15866  df-phtpy 16045

Copyright terms: Public domain