Theorem pi1fval 16092

Description: The value of the fundamental group concatenation operation.

Hypothesis

Ref	Expression
pi1fval.1	|- X = U.J

Assertion

Ref	Expression
pi1fval	|- ((J e. Top /\ Y e. X) -> (pi1` <.J, Y>.) = {<.<.f, g>., h>. | E.m e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)}E.n e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))})

Distinct variable groups:   f,J,g,h,m,n,t   f,Y,g,h,m,n,t

Proof of Theorem pi1fval

Step	Hyp	Ref	Expression
1		oprex 4907	. . . . 5 |- (II Cn J) e. _V
2	1	rabex 3461	. . . 4 |- {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} e. _V
3		elsn 3058	. . . . . . . . 9 |- (f e. {[m](~=ph` J)} <-> f = [m](~=ph` J))
4		elsn 3058	. . . . . . . . 9 |- (g e. {[n](~=ph` J)} <-> g = [n](~=ph` J))
5	3, 4	anbi12i 540	. . . . . . . 8 |- ((f e. {[m](~=ph` J)} /\ g e. {[n](~=ph` J)}) <-> (f = [m](~=ph` J) /\ g = [n](~=ph` J)))
6	5	anbi1i 539	. . . . . . 7 |- (((f e. {[m](~=ph` J)} /\ g e. {[n](~=ph` J)}) /\ h = [(m(*p` J)n)](~=ph` J)) <-> ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J)))
7	6	oprabbii 4923	. . . . . 6 |- {<.<.f, g>., h>. | ((f e. {[m](~=ph` J)} /\ g e. {[n](~=ph` J)}) /\ h = [(m(*p` J)n)](~=ph` J))} = {<.<.f, g>., h>. | ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))}
8		snex 3492	. . . . . . 7 |- {[m](~=ph` J)} e. _V
9		snex 3492	. . . . . . 7 |- {[n](~=ph` J)} e. _V
10		eqid 1884	. . . . . . 7 |- {<.<.f, g>., h>. | ((f e. {[m](~=ph` J)} /\ g e. {[n](~=ph` J)}) /\ h = [(m(*p` J)n)](~=ph` J))} = {<.<.f, g>., h>. | ((f e. {[m](~=ph` J)} /\ g e. {[n](~=ph` J)}) /\ h = [(m(*p` J)n)](~=ph` J))}
11	8, 9, 10	oprabex2 4950	. . . . . 6 |- {<.<.f, g>., h>. | ((f e. {[m](~=ph` J)} /\ g e. {[n](~=ph` J)}) /\ h = [(m(*p` J)n)](~=ph` J))} e. _V
12	7, 11	eqeltrri 1968	. . . . 5 |- {<.<.f, g>., h>. | ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))} e. _V
13	2, 12	oprabrexex2 15709	. . . 4 |- {<.<.f, g>., h>. | E.n e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))} e. _V
14	2, 13	oprabrexex2 15709	. . 3 |- {<.<.f, g>., h>. | E.m e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)}E.n e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))} e. _V
15		opreq2 4890	. . . . . 6 |- (j = J -> (II Cn j) = (II Cn J))
16		rabeq 2289	. . . . . 6 |- ((II Cn j) = (II Cn J) -> {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)} = {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)})
17	15, 16	syl 12	. . . . 5 |- (j = J -> {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)} = {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)})
18		fveq2 4681	. . . . . . . . . 10 |- (j = J -> (~=ph` j) = (~=ph` J))
19		eceq1 5335	. . . . . . . . . 10 |- ((~=ph` j) = (~=ph` J) -> [m](~=ph` j) = [m](~=ph` J))
20	18, 19	syl 12	. . . . . . . . 9 |- (j = J -> [m](~=ph` j) = [m](~=ph` J))
21	20	eqeq2d 1895	. . . . . . . 8 |- (j = J -> (f = [m](~=ph` j) <-> f = [m](~=ph` J)))
22		eceq1 5335	. . . . . . . . . 10 |- ((~=ph` j) = (~=ph` J) -> [n](~=ph` j) = [n](~=ph` J))
23	18, 22	syl 12	. . . . . . . . 9 |- (j = J -> [n](~=ph` j) = [n](~=ph` J))
24	23	eqeq2d 1895	. . . . . . . 8 |- (j = J -> (g = [n](~=ph` j) <-> g = [n](~=ph` J)))
25	21, 24	anbi12d 690	. . . . . . 7 |- (j = J -> ((f = [m](~=ph` j) /\ g = [n](~=ph` j)) <-> (f = [m](~=ph` J) /\ g = [n](~=ph` J))))
26		eceq1 5335	. . . . . . . . . 10 |- ((~=ph` j) = (~=ph` J) -> [(m(*p` j)n)](~=ph` j) = [(m(*p` j)n)](~=ph` J))
27	18, 26	syl 12	. . . . . . . . 9 |- (j = J -> [(m(*p` j)n)](~=ph` j) = [(m(*p` j)n)](~=ph` J))
28		fveq2 4681	. . . . . . . . . . 11 |- (j = J -> (*p` j) = (*p` J))
29	28	opreqd 4899	. . . . . . . . . 10 |- (j = J -> (m(*p` j)n) = (m(*p` J)n))
30		eceq2 5336	. . . . . . . . . 10 |- ((m(*p` j)n) = (m(*p` J)n) -> [(m(*p` j)n)](~=ph` J) = [(m(*p` J)n)](~=ph` J))
31	29, 30	syl 12	. . . . . . . . 9 |- (j = J -> [(m(*p` j)n)](~=ph` J) = [(m(*p` J)n)](~=ph` J))
32	27, 31	eqtrd 1925	. . . . . . . 8 |- (j = J -> [(m(*p` j)n)](~=ph` j) = [(m(*p` J)n)](~=ph` J))
33	32	eqeq2d 1895	. . . . . . 7 |- (j = J -> (h = [(m(*p` j)n)](~=ph` j) <-> h = [(m(*p` J)n)](~=ph` J)))
34	25, 33	anbi12d 690	. . . . . 6 |- (j = J -> (((f = [m](~=ph` j) /\ g = [n](~=ph` j)) /\ h = [(m(*p` j)n)](~=ph` j)) <-> ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))))
35	17, 34	rexeqbidv 2275	. . . . 5 |- (j = J -> (E.n e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` j) /\ g = [n](~=ph` j)) /\ h = [(m(*p` j)n)](~=ph` j)) <-> E.n e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))))
36	17, 35	rexeqbidv 2275	. . . 4 |- (j = J -> (E.m e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)}E.n e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` j) /\ g = [n](~=ph` j)) /\ h = [(m(*p` j)n)](~=ph` j)) <-> E.m e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)}E.n e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))))
37	36	oprabbidv 4922	. . 3 |- (j = J -> {<.<.f, g>., h>. | E.m e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)}E.n e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` j) /\ g = [n](~=ph` j)) /\ h = [(m(*p` j)n)](~=ph` j))} = {<.<.f, g>., h>. | E.m e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)}E.n e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))})
38		unieq 3185	. . . 4 |- (j = J -> U.j = U.J)
39		pi1fval.1	. . . 4 |- X = U.J
40	38, 39	syl6eqr 1946	. . 3 |- (j = J -> U.j = X)
41		eqeq2 1893	. . . . . . 7 |- (y = Y -> ((t` 0) = y <-> (t` 0) = Y))
42		eqeq2 1893	. . . . . . 7 |- (y = Y -> ((t` 1) = y <-> (t` 1) = Y))
43	41, 42	anbi12d 690	. . . . . 6 |- (y = Y -> (((t` 0) = y /\ (t` 1) = y) <-> ((t` 0) = Y /\ (t` 1) = Y)))
44	43	rabbidv 2287	. . . . 5 |- (y = Y -> {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)} = {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)})
45	44	rexeqdv 2270	. . . . 5 |- (y = Y -> (E.n e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J)) <-> E.n e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))))
46	44, 45	rexeqbidv 2275	. . . 4 |- (y = Y -> (E.m e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)}E.n e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J)) <-> E.m e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)}E.n e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))))
47	46	oprabbidv 4922	. . 3 |- (y = Y -> {<.<.f, g>., h>. | E.m e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)}E.n e. {t e. (II Cn J) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))} = {<.<.f, g>., h>. | E.m e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)}E.n e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))})
48		df-pi1 16071	. . 3 |- pi1 = {<.<.j, y>., p>. | ((j e. Top /\ y e. U.j) /\ p = {<.<.f, g>., h>. | E.m e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)}E.n e. {t e. (II Cn j) | ((t` 0) = y /\ (t` 1) = y)} ((f = [m](~=ph` j) /\ g = [n](~=ph` j)) /\ h = [(m(*p` j)n)](~=ph` j))})}
49	14, 37, 40, 47, 48	oprabval2a 15707	. 2 |- ((J e. Top /\ Y e. X) -> (Jpi1Y) = {<.<.f, g>., h>. | E.m e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)}E.n e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))})
50		df-opr 4886	. 2 |- (Jpi1Y) = (pi1` <.J, Y>.)
51	49, 50	syl5eqr 1942	1 |- ((J e. Top /\ Y e. X) -> (pi1` <.J, Y>.) = {<.<.f, g>., h>. | E.m e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)}E.n e. {t e. (II Cn J) | ((t` 0) = Y /\ (t` 1) = Y)} ((f = [m](~=ph` J) /\ g = [n](~=ph` J)) /\ h = [(m(*p` J)n)](~=ph` J))})

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  E.wrex 2106  {crab 2108  _Vcvv 2292  {csn 3044  <.cop 3046  U.cuni 3177  ` cfv 3998  (class class class)co 4884  {copab2 4885  [cec 5316  0cc0 6386  1c1 6387  Topctop 8857   Cn ccn 9028  IIcii 15865  ~=phcphtpc 16044  *pcpco 16067  pi1cpi1 16068

This theorem is referenced by:  pi1f 16093  pi1val 16094

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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  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-ral 2109  df-rex 2110  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-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  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-fv 4014  df-opr 4886  df-oprab 4887  df-ec 5320  df-pi1 16071

Copyright terms: Public domain