Theorem pi1gp 16095

Description: The fundamental group is a group. Proposition 1.3 of [Hatcher] p. 26.

Hypothesis

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

Assertion

Ref	Expression
pi1gp	|- ((J e. Top /\ Y e. X) -> (pi1` <.J, Y>.) e. Grp)

Proof of Theorem pi1gp

Step	Hyp	Ref	Expression
1		fvex 4689	. . 3 |- (pi1b` <.J, Y>.) e. _V
2	1	a1i 8	. 2 |- ((J e. Top /\ Y e. X) -> (pi1b` <.J, Y>.) e. _V)
3		pi1gp.1	. . 3 |- X = U.J
4	3	pi1f 16093	. 2 |- ((J e. Top /\ Y e. X) -> (pi1` <.J, Y>.):((pi1b` <.J, Y>.) X. (pi1b` <.J, Y>.))-->(pi1b` <.J, Y>.))
5	3	elpi1 16089	. . . . 5 |- ((J e. Top /\ Y e. X) -> (x e. (pi1b` <.J, Y>.) <-> E.f e. (II Cn J)(((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))))
6	3	elpi1 16089	. . . . 5 |- ((J e. Top /\ Y e. X) -> (y e. (pi1b` <.J, Y>.) <-> E.g e. (II Cn J)(((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J))))
7	3	elpi1 16089	. . . . 5 |- ((J e. Top /\ Y e. X) -> (z e. (pi1b` <.J, Y>.) <-> E.h e. (II Cn J)(((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J))))
8	5, 6, 7	3anbi123d 1168	. . . 4 |- ((J e. Top /\ Y e. X) -> ((x e. (pi1b` <.J, Y>.) /\ y e. (pi1b` <.J, Y>.) /\ z e. (pi1b` <.J, Y>.)) <-> (E.f e. (II Cn J)(((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) /\ E.g e. (II Cn J)(((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) /\ E.h e. (II Cn J)(((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)))))
9		opreq12 4891	. . . . . . . . . . . . . . . . . . . . 21 |- ((x = [f](~=ph` J) /\ y = [g](~=ph` J)) -> (x(pi1` <.J, Y>.)y) = ([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J)))
10	9	3adant3 896	. . . . . . . . . . . . . . . . . . . 20 |- ((x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> (x(pi1` <.J, Y>.)y) = ([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J)))
11		simp3 878	. . . . . . . . . . . . . . . . . . . 20 |- ((x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> z = [h](~=ph` J))
12	10, 11	opreq12d 4900	. . . . . . . . . . . . . . . . . . 19 |- ((x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J))(pi1` <.J, Y>.)[h](~=ph` J)))
13		simp1 876	. . . . . . . . . . . . . . . . . . . 20 |- ((x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> x = [f](~=ph` J))
14		opreq12 4891	. . . . . . . . . . . . . . . . . . . . 21 |- ((y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> (y(pi1` <.J, Y>.)z) = ([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)))
15	14	3adant1 894	. . . . . . . . . . . . . . . . . . . 20 |- ((x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> (y(pi1` <.J, Y>.)z) = ([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)))
16	13, 15	opreq12d 4900	. . . . . . . . . . . . . . . . . . 19 |- ((x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z)) = ([f](~=ph` J)(pi1` <.J, Y>.)([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J))))
17	12, 16	eqeq12d 1899	. . . . . . . . . . . . . . . . . 18 |- ((x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> (((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z)) <-> (([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J))(pi1` <.J, Y>.)[h](~=ph` J)) = ([f](~=ph` J)(pi1` <.J, Y>.)([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)))))
18		simpll 448	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> J e. Top)
19		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) -> f e. (II Cn J))
20		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) -> g e. (II Cn J))
21		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y) -> h e. (II Cn J))
22	19, 20, 21	3anim123i 1053	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) -> (f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J)))
23	22	adantl 424	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J)))
24		eqtr3 1907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((f` 1) = Y /\ (g` 0) = Y) -> (f` 1) = (g` 0))
25	24	3ad2antr2 1042	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((f` 1) = Y /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y)) -> (f` 1) = (g` 0))
26	25	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y)) -> (f` 1) = (g` 0))
27	26	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) -> (f` 1) = (g` 0))
28		eqtr3 1907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((g` 1) = Y /\ (h` 0) = Y) -> (g` 1) = (h` 0))
29	28	3ad2antr2 1042	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((g` 1) = Y /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) -> (g` 1) = (h` 0))
30	29	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) -> (g` 1) = (h` 0))
31	30	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) -> (g` 1) = (h` 0))
32	27, 31	jca 310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) -> ((f` 1) = (g` 0) /\ (g` 1) = (h` 0)))
33	32	adantl 424	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((f` 1) = (g` 0) /\ (g` 1) = (h` 0)))
34		pcoass 16085	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ (f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J)) /\ ((f` 1) = (g` 0) /\ (g` 1) = (h` 0))) -> ((f(*p` J)g)(*p` J)h)(~=ph` J)(f(*p` J)(g(*p` J)h)))
35	18, 23, 33, 34	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((f(*p` J)g)(*p` J)h)(~=ph` J)(f(*p` J)(g(*p` J)h)))
36		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f(*p` J)(g(*p` J)h)) e. _V
37	36	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (f(*p` J)(g(*p` J)h)) e. _V)
38		phtpcer 16062	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (J e. Top -> Er (~=ph` J))
39	38	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> Er (~=ph` J))
40		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> J e. Top)
41		simprl1 921	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> f e. (II Cn J))
42		simprr1 924	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> g e. (II Cn J))
43	26	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> (f` 1) = (g` 0))
44		pcocn 16076	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((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))
45	40, 41, 42, 43, 44	syl13anc 1102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> (f(*p` J)g) e. (II Cn J))
46	45	3adantr3 1037	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (f(*p` J)g) e. (II Cn J))
47		simpr31 966	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> h e. (II Cn J))
48		pco1 16078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J e. Top /\ (f e. (II Cn J) /\ g e. (II Cn J) /\ (f` 1) = (g` 0))) -> ((f(*p` J)g)` 1) = (g` 1))
49	40, 41, 42, 43, 48	syl13anc 1102	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> ((f(*p` J)g)` 1) = (g` 1))
50		simprr3 926	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> (g` 1) = Y)
51	49, 50	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> ((f(*p` J)g)` 1) = Y)
52	51	3adantr3 1037	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((f(*p` J)g)` 1) = Y)
53		simpr32 967	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (h` 0) = Y)
54	52, 53	eqtr4d 1928	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((f(*p` J)g)` 1) = (h` 0))
55		pcocn 16076	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Top /\ ((f(*p` J)g) e. (II Cn J) /\ h e. (II Cn J) /\ ((f(*p` J)g)` 1) = (h` 0))) -> ((f(*p` J)g)(*p` J)h) e. (II Cn J))
56	18, 46, 47, 54, 55	syl13anc 1102	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((f(*p` J)g)(*p` J)h) e. (II Cn J))
57		phtpcdm 16061	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (J e. Top -> dom (~=ph` J) = (II Cn J))
58	57	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> dom (~=ph` J) = (II Cn J))
59	56, 58	eleqtrrd 1974	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((f(*p` J)g)(*p` J)h) e. dom (~=ph` J))
60		erthdmg 15730	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f(*p` J)(g(*p` J)h)) e. _V /\ Er (~=ph` J) /\ ((f(*p` J)g)(*p` J)h) e. dom (~=ph` J)) -> ([((f(*p` J)g)(*p` J)h)](~=ph` J) = [(f(*p` J)(g(*p` J)h))](~=ph` J) <-> ((f(*p` J)g)(*p` J)h)(~=ph` J)(f(*p` J)(g(*p` J)h))))
61	37, 39, 59, 60	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ([((f(*p` J)g)(*p` J)h)](~=ph` J) = [(f(*p` J)(g(*p` J)h))](~=ph` J) <-> ((f(*p` J)g)(*p` J)h)(~=ph` J)(f(*p` J)(g(*p` J)h))))
62	35, 61	mpbird 213	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> [((f(*p` J)g)(*p` J)h)](~=ph` J) = [(f(*p` J)(g(*p` J)h))](~=ph` J))
63	3	pi1val 16094	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y)) -> ([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J)) = [(f(*p` J)g)](~=ph` J))
64	63	3adant3r3 1079	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J)) = [(f(*p` J)g)](~=ph` J))
65	64	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J))(pi1` <.J, Y>.)[h](~=ph` J)) = ([(f(*p` J)g)](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)))
66		pco0 16077	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J e. Top /\ (f e. (II Cn J) /\ g e. (II Cn J) /\ (f` 1) = (g` 0))) -> ((f(*p` J)g)` 0) = (f` 0))
67	40, 41, 42, 43, 66	syl13anc 1102	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> ((f(*p` J)g)` 0) = (f` 0))
68		simprl2 922	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> (f` 0) = Y)
69	67, 68	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> ((f(*p` J)g)` 0) = Y)
70	45, 69, 51	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> ((f(*p` J)g) e. (II Cn J) /\ ((f(*p` J)g)` 0) = Y /\ ((f(*p` J)g)` 1) = Y))
71	3	pi1val 16094	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ Y e. X) /\ ((f(*p` J)g) e. (II Cn J) /\ ((f(*p` J)g)` 0) = Y /\ ((f(*p` J)g)` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) -> ([(f(*p` J)g)](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)) = [((f(*p` J)g)(*p` J)h)](~=ph` J))
72	71	3expia 1069	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ Y e. X) /\ ((f(*p` J)g) e. (II Cn J) /\ ((f(*p` J)g)` 0) = Y /\ ((f(*p` J)g)` 1) = Y)) -> ((h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y) -> ([(f(*p` J)g)](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)) = [((f(*p` J)g)(*p` J)h)](~=ph` J)))
73	70, 72	syldan 516	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y))) -> ((h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y) -> ([(f(*p` J)g)](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)) = [((f(*p` J)g)(*p` J)h)](~=ph` J)))
74	73	exp32 408	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ Y e. X) -> ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) -> ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) -> ((h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y) -> ([(f(*p` J)g)](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)) = [((f(*p` J)g)(*p` J)h)](~=ph` J)))))
75	74	3imp2 1083	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ([(f(*p` J)g)](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)) = [((f(*p` J)g)(*p` J)h)](~=ph` J))
76	65, 75	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J))(pi1` <.J, Y>.)[h](~=ph` J)) = [((f(*p` J)g)(*p` J)h)](~=ph` J))
77	3	pi1val 16094	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ Y e. X) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) -> ([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)) = [(g(*p` J)h)](~=ph` J))
78	77	3adant3r1 1077	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J)) = [(g(*p` J)h)](~=ph` J))
79	78	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ([f](~=ph` J)(pi1` <.J, Y>.)([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J))) = ([f](~=ph` J)(pi1` <.J, Y>.)[(g(*p` J)h)](~=ph` J)))
80		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> J e. Top)
81		simprl1 921	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> g e. (II Cn J))
82		simprr1 924	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> h e. (II Cn J))
83	30	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (g` 1) = (h` 0))
84		pcocn 16076	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J e. Top /\ (g e. (II Cn J) /\ h e. (II Cn J) /\ (g` 1) = (h` 0))) -> (g(*p` J)h) e. (II Cn J))
85	80, 81, 82, 83, 84	syl13anc 1102	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (g(*p` J)h) e. (II Cn J))
86		pco0 16077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J e. Top /\ (g e. (II Cn J) /\ h e. (II Cn J) /\ (g` 1) = (h` 0))) -> ((g(*p` J)h)` 0) = (g` 0))
87	80, 81, 82, 83, 86	syl13anc 1102	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((g(*p` J)h)` 0) = (g` 0))
88		simprl2 922	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (g` 0) = Y)
89	87, 88	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((g(*p` J)h)` 0) = Y)
90		pco1 16078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J e. Top /\ (g e. (II Cn J) /\ h e. (II Cn J) /\ (g` 1) = (h` 0))) -> ((g(*p` J)h)` 1) = (h` 1))
91	80, 81, 82, 83, 90	syl13anc 1102	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((g(*p` J)h)` 1) = (h` 1))
92		simprr3 926	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (h` 1) = Y)
93	91, 92	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((g(*p` J)h)` 1) = Y)
94	85, 89, 93	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ Y e. X) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((g(*p` J)h) e. (II Cn J) /\ ((g(*p` J)h)` 0) = Y /\ ((g(*p` J)h)` 1) = Y))
95	94	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ((g(*p` J)h) e. (II Cn J) /\ ((g(*p` J)h)` 0) = Y /\ ((g(*p` J)h)` 1) = Y))
96	3	pi1val 16094	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ ((g(*p` J)h) e. (II Cn J) /\ ((g(*p` J)h)` 0) = Y /\ ((g(*p` J)h)` 1) = Y)) -> ([f](~=ph` J)(pi1` <.J, Y>.)[(g(*p` J)h)](~=ph` J)) = [(f(*p` J)(g(*p` J)h))](~=ph` J))
97	96	3expa 1067	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) /\ ((g(*p` J)h) e. (II Cn J) /\ ((g(*p` J)h)` 0) = Y /\ ((g(*p` J)h)` 1) = Y)) -> ([f](~=ph` J)(pi1` <.J, Y>.)[(g(*p` J)h)](~=ph` J)) = [(f(*p` J)(g(*p` J)h))](~=ph` J))
98	95, 97	syldan 516	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) /\ ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ([f](~=ph` J)(pi1` <.J, Y>.)[(g(*p` J)h)](~=ph` J)) = [(f(*p` J)(g(*p` J)h))](~=ph` J))
99	98	exp43 415	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ Y e. X) -> ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) -> ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) -> ((h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y) -> ([f](~=ph` J)(pi1` <.J, Y>.)[(g(*p` J)h)](~=ph` J)) = [(f(*p` J)(g(*p` J)h))](~=ph` J)))))
100	99	3imp2 1083	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ([f](~=ph` J)(pi1` <.J, Y>.)[(g(*p` J)h)](~=ph` J)) = [(f(*p` J)(g(*p` J)h))](~=ph` J))
101	79, 100	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> ([f](~=ph` J)(pi1` <.J, Y>.)([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J))) = [(f(*p` J)(g(*p` J)h))](~=ph` J))
102	62, 76, 101	3eqtr4d 1937	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y))) -> (([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J))(pi1` <.J, Y>.)[h](~=ph` J)) = ([f](~=ph` J)(pi1` <.J, Y>.)([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J))))
103		an6 1177	. . . . . . . . . . . . . . . . . . . . 21 |- (((f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ ((g` 0) = Y /\ (g` 1) = Y) /\ ((h` 0) = Y /\ (h` 1) = Y))) <-> ((f e. (II Cn J) /\ ((f` 0) = Y /\ (f` 1) = Y)) /\ (g e. (II Cn J) /\ ((g` 0) = Y /\ (g` 1) = Y)) /\ (h e. (II Cn J) /\ ((h` 0) = Y /\ (h` 1) = Y))))
104		3anass 862	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) <-> (f e. (II Cn J) /\ ((f` 0) = Y /\ (f` 1) = Y)))
105		3anass 862	. . . . . . . . . . . . . . . . . . . . . 22 |- ((g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) <-> (g e. (II Cn J) /\ ((g` 0) = Y /\ (g` 1) = Y)))
106		3anass 862	. . . . . . . . . . . . . . . . . . . . . 22 |- ((h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y) <-> (h e. (II Cn J) /\ ((h` 0) = Y /\ (h` 1) = Y)))
107	104, 105, 106	3anbi123i 1056	. . . . . . . . . . . . . . . . . . . . 21 |- (((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)) <-> ((f e. (II Cn J) /\ ((f` 0) = Y /\ (f` 1) = Y)) /\ (g e. (II Cn J) /\ ((g` 0) = Y /\ (g` 1) = Y)) /\ (h e. (II Cn J) /\ ((h` 0) = Y /\ (h` 1) = Y))))
108	103, 107	bitr4i 193	. . . . . . . . . . . . . . . . . . . 20 |- (((f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ ((g` 0) = Y /\ (g` 1) = Y) /\ ((h` 0) = Y /\ (h` 1) = Y))) <-> ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ (g e. (II Cn J) /\ (g` 0) = Y /\ (g` 1) = Y) /\ (h e. (II Cn J) /\ (h` 0) = Y /\ (h` 1) = Y)))
109	102, 108	sylan2b 501	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ Y e. X) /\ ((f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ ((g` 0) = Y /\ (g` 1) = Y) /\ ((h` 0) = Y /\ (h` 1) = Y)))) -> (([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J))(pi1` <.J, Y>.)[h](~=ph` J)) = ([f](~=ph` J)(pi1` <.J, Y>.)([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J))))
110	109	anassrs 489	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J))) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ ((g` 0) = Y /\ (g` 1) = Y) /\ ((h` 0) = Y /\ (h` 1) = Y))) -> (([f](~=ph` J)(pi1` <.J, Y>.)[g](~=ph` J))(pi1` <.J, Y>.)[h](~=ph` J)) = ([f](~=ph` J)(pi1` <.J, Y>.)([g](~=ph` J)(pi1` <.J, Y>.)[h](~=ph` J))))
111	17, 110	syl5cbir 228	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J))) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ ((g` 0) = Y /\ (g` 1) = Y) /\ ((h` 0) = Y /\ (h` 1) = Y))) -> ((x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))
112	111	impr 422	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J))) /\ ((((f` 0) = Y /\ (f` 1) = Y) /\ ((g` 0) = Y /\ (g` 1) = Y) /\ ((h` 0) = Y /\ (h` 1) = Y)) /\ (x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J)))) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z)))
113		an6 1177	. . . . . . . . . . . . . . . 16 |- (((((f` 0) = Y /\ (f` 1) = Y) /\ ((g` 0) = Y /\ (g` 1) = Y) /\ ((h` 0) = Y /\ (h` 1) = Y)) /\ (x = [f](~=ph` J) /\ y = [g](~=ph` J) /\ z = [h](~=ph` J))) <-> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) /\ (((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) /\ (((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J))))
114	112, 113	sylan2br 502	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J))) /\ ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) /\ (((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) /\ (((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)))) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z)))
115	114	3exp2 1086	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ g e. (II Cn J) /\ h e. (II Cn J))) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ((((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> ((((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
116	115	3exp2 1086	. . . . . . . . . . . . 13 |- ((J e. Top /\ Y e. X) -> (f e. (II Cn J) -> (g e. (II Cn J) -> (h e. (II Cn J) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ((((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> ((((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z)))))))))
117	116	imp41 395	. . . . . . . . . . . 12 |- (((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ g e. (II Cn J)) /\ h e. (II Cn J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ((((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> ((((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
118	117	com34 40	. . . . . . . . . . 11 |- (((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ g e. (II Cn J)) /\ h e. (II Cn J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ((((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
119	118	com23 36	. . . . . . . . . 10 |- (((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ g e. (II Cn J)) /\ h e. (II Cn J)) -> ((((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ((((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
120	119	r19.23adva 2216	. . . . . . . . 9 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ g e. (II Cn J)) -> (E.h e. (II Cn J)(((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ((((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
121	120	com24 41	. . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ g e. (II Cn J)) -> ((((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> (E.h e. (II Cn J)(((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
122	121	r19.23adva 2216	. . . . . . 7 |- (((J e. Top /\ Y e. X) /\ f e. (II Cn J)) -> (E.g e. (II Cn J)(((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> (E.h e. (II Cn J)(((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
123	122	com23 36	. . . . . 6 |- (((J e. Top /\ Y e. X) /\ f e. (II Cn J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> (E.g e. (II Cn J)(((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> (E.h e. (II Cn J)(((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
124	123	r19.23adva 2216	. . . . 5 |- ((J e. Top /\ Y e. X) -> (E.f e. (II Cn J)(((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> (E.g e. (II Cn J)(((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) -> (E.h e. (II Cn J)(((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))))
125	124	3impd 1082	. . . 4 |- ((J e. Top /\ Y e. X) -> ((E.f e. (II Cn J)(((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) /\ E.g e. (II Cn J)(((g` 0) = Y /\ (g` 1) = Y) /\ y = [g](~=ph` J)) /\ E.h e. (II Cn J)(((h` 0) = Y /\ (h` 1) = Y) /\ z = [h](~=ph` J))) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))
126	8, 125	sylbid 220	. . 3 |- ((J e. Top /\ Y e. X) -> ((x e. (pi1b` <.J, Y>.) /\ y e. (pi1b` <.J, Y>.) /\ z e. (pi1b` <.J, Y>.)) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z))))
127	126	imp 377	. 2 |- (((J e. Top /\ Y e. X) /\ (x e. (pi1b` <.J, Y>.) /\ y e. (pi1b` <.J, Y>.) /\ z e. (pi1b` <.J, Y>.))) -> ((x(pi1` <.J, Y>.)y)(pi1` <.J, Y>.)z) = (x(pi1` <.J, Y>.)(y(pi1` <.J, Y>.)z)))
128		iitop 15867	. . . . 5 |- II e. Top
129		iiuni 15868	. . . . . . . 8 |- (0[,]1) = U.II
130	129, 3	cnconst 9057	. . . . . . 7 |- (((II e. Top /\ J e. Top) /\ (Y e. X /\ ((0[,]1) X. {Y}):(0[,]1)-->{Y})) -> ((0[,]1) X. {Y}) e. (II Cn J))
131	130	ancom1s 548	. . . . . 6 |- (((J e. Top /\ II e. Top) /\ (Y e. X /\ ((0[,]1) X. {Y}):(0[,]1)-->{Y})) -> ((0[,]1) X. {Y}) e. (II Cn J))
132		fconstg 4604	. . . . . . 7 |- (Y e. X -> ((0[,]1) X. {Y}):(0[,]1)-->{Y})
133	132	ancli 320	. . . . . 6 |- (Y e. X -> (Y e. X /\ ((0[,]1) X. {Y}):(0[,]1)-->{Y}))
134	131, 133	sylan2 500	. . . . 5 |- (((J e. Top /\ II e. Top) /\ Y e. X) -> ((0[,]1) X. {Y}) e. (II Cn J))
135	128, 134	mpanl2 771	. . . 4 |- ((J e. Top /\ Y e. X) -> ((0[,]1) X. {Y}) e. (II Cn J))
136		0re 6603	. . . . . . 7 |- 0 e. RR
137		1re 6598	. . . . . . 7 |- 1 e. RR
138		lt01 6871	. . . . . . . 8 |- 0 < 1
139	136, 137, 138	ltleii 6756	. . . . . . 7 |- 0 <_ 1
140		lbicc2 7573	. . . . . . 7 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 0 e. (0[,]1))
141	136, 137, 139, 140	mp3an 1191	. . . . . 6 |- 0 e. (0[,]1)
142		fvconst2g 4820	. . . . . 6 |- ((Y e. X /\ 0 e. (0[,]1)) -> (((0[,]1) X. {Y})` 0) = Y)
143	141, 142	mpan2 760	. . . . 5 |- (Y e. X -> (((0[,]1) X. {Y})` 0) = Y)
144	143	adantl 424	. . . 4 |- ((J e. Top /\ Y e. X) -> (((0[,]1) X. {Y})` 0) = Y)
145		ubicc2 7574	. . . . . . 7 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 1 e. (0[,]1))
146	136, 137, 139, 145	mp3an 1191	. . . . . 6 |- 1 e. (0[,]1)
147		fvconst2g 4820	. . . . . 6 |- ((Y e. X /\ 1 e. (0[,]1)) -> (((0[,]1) X. {Y})` 1) = Y)
148	146, 147	mpan2 760	. . . . 5 |- (Y e. X -> (((0[,]1) X. {Y})` 1) = Y)
149	148	adantl 424	. . . 4 |- ((J e. Top /\ Y e. X) -> (((0[,]1) X. {Y})` 1) = Y)
150	135, 144, 149	3jca 1050	. . 3 |- ((J e. Top /\ Y e. X) -> (((0[,]1) X. {Y}) e. (II Cn J) /\ (((0[,]1) X. {Y})` 0) = Y /\ (((0[,]1) X. {Y})` 1) = Y))
151	3	elpi1i 16090	. . 3 |- (((J e. Top /\ Y e. X) /\ (((0[,]1) X. {Y}) e. (II Cn J) /\ (((0[,]1) X. {Y})` 0) = Y /\ (((0[,]1) X. {Y})` 1) = Y)) -> [((0[,]1) X. {Y})](~=ph` J) e. (pi1b` <.J, Y>.))
152	150, 151	mpdan 768	. 2 |- ((J e. Top /\ Y e. X) -> [((0[,]1) X. {Y})](~=ph` J) e. (pi1b` <.J, Y>.))
153	150	adantr 425	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> (((0[,]1) X. {Y}) e. (II Cn J) /\ (((0[,]1) X. {Y})` 0) = Y /\ (((0[,]1) X. {Y})` 1) = Y))
154	3	pi1val 16094	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ Y e. X) /\ (((0[,]1) X. {Y}) e. (II Cn J) /\ (((0[,]1) X. {Y})` 0) = Y /\ (((0[,]1) X. {Y})` 1) = Y) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [(((0[,]1) X. {Y})(*p` J)f)](~=ph` J))
155	154	3expa 1067	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ Y e. X) /\ (((0[,]1) X. {Y}) e. (II Cn J) /\ (((0[,]1) X. {Y})` 0) = Y /\ (((0[,]1) X. {Y})` 1) = Y)) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [(((0[,]1) X. {Y})(*p` J)f)](~=ph` J))
156	155	an1rs 547	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) /\ (((0[,]1) X. {Y}) e. (II Cn J) /\ (((0[,]1) X. {Y})` 0) = Y /\ (((0[,]1) X. {Y})` 1) = Y)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [(((0[,]1) X. {Y})(*p` J)f)](~=ph` J))
157	153, 156	mpdan 768	. . . . . . . . . . . . 13 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [(((0[,]1) X. {Y})(*p` J)f)](~=ph` J))
158		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- ((0[,]1) X. {Y}) = ((0[,]1) X. {Y})
159	158	pcopt 16084	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ f e. (II Cn J) /\ (f` 0) = Y) -> (((0[,]1) X. {Y})(*p` J)f)(~=ph` J)f)
160	159	3expb 1068	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> (((0[,]1) X. {Y})(*p` J)f)(~=ph` J)f)
161	160	adantlr 429	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> (((0[,]1) X. {Y})(*p` J)f)(~=ph` J)f)
162	161	3adantr3 1037	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> (((0[,]1) X. {Y})(*p` J)f)(~=ph` J)f)
163		visset 2295	. . . . . . . . . . . . . . . 16 |- f e. _V
164	163	a1i 8	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> f e. _V)
165	38	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> Er (~=ph` J))
166		simpll 448	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> J e. Top)
167	135	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> ((0[,]1) X. {Y}) e. (II Cn J))
168		simprl 450	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> f e. (II Cn J))
169	148	ad2antlr 441	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> (((0[,]1) X. {Y})` 1) = Y)
170		simprr 451	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> (f` 0) = Y)
171	169, 170	eqtr4d 1928	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> (((0[,]1) X. {Y})` 1) = (f` 0))
172		pcocn 16076	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ (((0[,]1) X. {Y}) e. (II Cn J) /\ f e. (II Cn J) /\ (((0[,]1) X. {Y})` 1) = (f` 0))) -> (((0[,]1) X. {Y})(*p` J)f) e. (II Cn J))
173	166, 167, 168, 171, 172	syl13anc 1102	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y)) -> (((0[,]1) X. {Y})(*p` J)f) e. (II Cn J))
174	173	3adantr3 1037	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> (((0[,]1) X. {Y})(*p` J)f) e. (II Cn J))
175	57	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> dom (~=ph` J) = (II Cn J))
176	174, 175	eleqtrrd 1974	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> (((0[,]1) X. {Y})(*p` J)f) e. dom (~=ph` J))
177		erthdmg 15730	. . . . . . . . . . . . . . 15 |- ((f e. _V /\ Er (~=ph` J) /\ (((0[,]1) X. {Y})(*p` J)f) e. dom (~=ph` J)) -> ([(((0[,]1) X. {Y})(*p` J)f)](~=ph` J) = [f](~=ph` J) <-> (((0[,]1) X. {Y})(*p` J)f)(~=ph` J)f))
178	164, 165, 176, 177	syl111anc 1100	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([(((0[,]1) X. {Y})(*p` J)f)](~=ph` J) = [f](~=ph` J) <-> (((0[,]1) X. {Y})(*p` J)f)(~=ph` J)f))
179	162, 178	mpbird 213	. . . . . . . . . . . . 13 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> [(((0[,]1) X. {Y})(*p` J)f)](~=ph` J) = [f](~=ph` J))
180	157, 179	eqtrd 1925	. . . . . . . . . . . 12 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [f](~=ph` J))
181	180	expcom 403	. . . . . . . . . . 11 |- ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) -> ((J e. Top /\ Y e. X) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [f](~=ph` J)))
182	181	3expb 1068	. . . . . . . . . 10 |- ((f e. (II Cn J) /\ ((f` 0) = Y /\ (f` 1) = Y)) -> ((J e. Top /\ Y e. X) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [f](~=ph` J)))
183	182	impcom 378	. . . . . . . . 9 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ ((f` 0) = Y /\ (f` 1) = Y))) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [f](~=ph` J))
184	183	anassrs 489	. . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ ((f` 0) = Y /\ (f` 1) = Y)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [f](~=ph` J))
185	184	adantrr 431	. . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [f](~=ph` J))
186		opreq2 4890	. . . . . . . . 9 |- (x = [f](~=ph` J) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)x) = ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)))
187		id 73	. . . . . . . . 9 |- (x = [f](~=ph` J) -> x = [f](~=ph` J))
188	186, 187	eqeq12d 1899	. . . . . . . 8 |- (x = [f](~=ph` J) -> (([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)x) = x <-> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [f](~=ph` J)))
189	188	ad2antll 443	. . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> (([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)x) = x <-> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [f](~=ph` J)))
190	185, 189	mpbird 213	. . . . . 6 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)x) = x)
191	190	ex 402	. . . . 5 |- (((J e. Top /\ Y e. X) /\ f e. (II Cn J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)x) = x))
192	191	r19.23adva 2216	. . . 4 |- ((J e. Top /\ Y e. X) -> (E.f e. (II Cn J)(((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)x) = x))
193	5, 192	sylbid 220	. . 3 |- ((J e. Top /\ Y e. X) -> (x e. (pi1b` <.J, Y>.) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)x) = x))
194	193	imp 377	. 2 |- (((J e. Top /\ Y e. X) /\ x e. (pi1b` <.J, Y>.)) -> ([((0[,]1) X. {Y})](~=ph` J)(pi1` <.J, Y>.)x) = x)
195		simpll 448	. . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> (J e. Top /\ Y e. X))
196	129, 3	cnf 9038	. . . . . . . . . . . . 13 |- ((II e. Top /\ J e. Top /\ f e. (II Cn J)) -> f:(0[,]1)-->X)
197	128, 196	mp3an1 1178	. . . . . . . . . . . 12 |- ((J e. Top /\ f e. (II Cn J)) -> f:(0[,]1)-->X)
198		ffn 4562	. . . . . . . . . . . 12 |- (f:(0[,]1)-->X -> f Fn (0[,]1))
199		iirev 15871	. . . . . . . . . . . . 13 |- (u e. (0[,]1) -> (1 - u) e. (0[,]1))
200		eqid 1884	. . . . . . . . . . . . 13 |- {<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))} = {<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))}
201		eqid 1884	. . . . . . . . . . . . 13 |- {<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} = {<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}
202	199, 200, 201	fnopabco 15711	. . . . . . . . . . . 12 |- (f Fn (0[,]1) -> {<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} = (f o. {<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))}))
203	197, 198, 202	3syl 24	. . . . . . . . . . 11 |- ((J e. Top /\ f e. (II Cn J)) -> {<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} = (f o. {<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))}))
204	128	a1i 8	. . . . . . . . . . . 12 |- ((J e. Top /\ f e. (II Cn J)) -> II e. Top)
205		simpl 346	. . . . . . . . . . . 12 |- ((J e. Top /\ f e. (II Cn J)) -> J e. Top)
206		simpr 350	. . . . . . . . . . . . 13 |- ((J e. Top /\ f e. (II Cn J)) -> f e. (II Cn J))
207		iccssre 7565	. . . . . . . . . . . . . . . 16 |- ((0 e. RR /\ 1 e. RR) -> (0[,]1) C_ RR)
208	136, 137, 207	mp2an 761	. . . . . . . . . . . . . . 15 |- (0[,]1) C_ RR
209		axresscn 6420	. . . . . . . . . . . . . . 15 |- RR C_ CC
210	208, 209	sstri 2626	. . . . . . . . . . . . . 14 |- (0[,]1) C_ CC
211		eqid 1884	. . . . . . . . . . . . . 14 |- {<.u, v>. | (u e. CC /\ v = (1 - u))} = {<.u, v>. | (u e. CC /\ v = (1 - u))}
212		ax1cn 6422	. . . . . . . . . . . . . . 15 |- 1 e. CC
213	211	sub2cncf 15886	. . . . . . . . . . . . . . 15 |- (1 e. CC -> {<.u, v>. | (u e. CC /\ v = (1 - u))} e. (CC-cn->CC))
214	212, 213	ax-mp 7	. . . . . . . . . . . . . 14 |- {<.u, v>. | (u e. CC /\ v = (1 - u))} e. (CC-cn->CC)
215		df-ii 15866	. . . . . . . . . . . . . 14 |- II = (Open` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
216	210, 210, 211, 200, 199, 214, 215, 215	cncfres 15895	. . . . . . . . . . . . 13 |- {<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))} e. (II Cn II)
217	206, 216	jctil 316	. . . . . . . . . . . 12 |- ((J e. Top /\ f e. (II Cn J)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))} e. (II Cn II) /\ f e. (II Cn J)))
218		cnco 9045	. . . . . . . . . . . 12 |- (((II e. Top /\ II e. Top /\ J e. Top) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))} e. (II Cn II) /\ f e. (II Cn J))) -> (f o. {<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))}) e. (II Cn J))
219	204, 204, 205, 217, 218	syl31anc 1103	. . . . . . . . . . 11 |- ((J e. Top /\ f e. (II Cn J)) -> (f o. {<.u, v>. | (u e. (0[,]1) /\ v = (1 - u))}) e. (II Cn J))
220	203, 219	eqeltrd 1971	. . . . . . . . . 10 |- ((J e. Top /\ f e. (II Cn J)) -> {<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J))
221	220	adantlr 429	. . . . . . . . 9 |- (((J e. Top /\ Y e. X) /\ f e. (II Cn J)) -> {<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J))
222	221	adantr 425	. . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> {<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J))
223		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (u = 0 -> (1 - u) = (1 - 0))
224	212	subid1i 6552	. . . . . . . . . . . . . . . 16 |- (1 - 0) = 1
225	223, 224	syl6eq 1944	. . . . . . . . . . . . . . 15 |- (u = 0 -> (1 - u) = 1)
226	225	fveq2d 4685	. . . . . . . . . . . . . 14 |- (u = 0 -> (f` (1 - u)) = (f` 1))
227		fvex 4689	. . . . . . . . . . . . . 14 |- (f` 1) e. _V
228	226, 201, 227	fvopab4 4743	. . . . . . . . . . . . 13 |- (0 e. (0[,]1) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = (f` 1))
229	141, 228	ax-mp 7	. . . . . . . . . . . 12 |- ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = (f` 1)
230	229	eqeq1i 1891	. . . . . . . . . . 11 |- (({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y <-> (f` 1) = Y)
231	230	biimpri 169	. . . . . . . . . 10 |- ((f` 1) = Y -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y)
232	231	ad2antlr 441	. . . . . . . . 9 |- ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y)
233	232	adantl 424	. . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y)
234		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (u = 1 -> (1 - u) = (1 - 1))
235	212	subidi 6551	. . . . . . . . . . . . . . . 16 |- (1 - 1) = 0
236	234, 235	syl6eq 1944	. . . . . . . . . . . . . . 15 |- (u = 1 -> (1 - u) = 0)
237	236	fveq2d 4685	. . . . . . . . . . . . . 14 |- (u = 1 -> (f` (1 - u)) = (f` 0))
238		fvex 4689	. . . . . . . . . . . . . 14 |- (f` 0) e. _V
239	237, 201, 238	fvopab4 4743	. . . . . . . . . . . . 13 |- (1 e. (0[,]1) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = (f` 0))
240	146, 239	ax-mp 7	. . . . . . . . . . . 12 |- ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = (f` 0)
241	240	eqeq1i 1891	. . . . . . . . . . 11 |- (({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y <-> (f` 0) = Y)
242	241	biimpri 169	. . . . . . . . . 10 |- ((f` 0) = Y -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y)
243	242	ad2antrr 440	. . . . . . . . 9 |- ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y)
244	243	adantl 424	. . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y)
245	3	elpi1i 16090	. . . . . . . 8 |- (((J e. Top /\ Y e. X) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y)) -> [{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J) e. (pi1b` <.J, Y>.))
246	195, 222, 233, 244, 245	syl13anc 1102	. . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> [{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J) e. (pi1b` <.J, Y>.))
247		opreq2 4890	. . . . . . . . 9 |- (x = [f](~=ph` J) -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)x) = ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)))
248	221	3ad2antr1 1041	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> {<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J))
249	231	3ad2ant3 899	. . . . . . . . . . . . . . 15 |- ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y)
250	249	adantl 424	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y)
251	242	3ad2ant2 898	. . . . . . . . . . . . . . 15 |- ((f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y)
252	251	adantl 424	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y)
253	248, 250, 252	3jca 1050	. . . . . . . . . . . . 13 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y))
254	3	pi1val 16094	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)](~=ph` J))
255	254	3com23 1074	. . . . . . . . . . . . 13 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 0) = Y /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = Y)) -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)](~=ph` J))
256	253, 255	mpd3an3 1192	. . . . . . . . . . . 12 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)](~=ph` J))
257	201, 158	pcorev 16087	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ f e. (II Cn J) /\ (f` 1) = Y) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)(~=ph` J)((0[,]1) X. {Y}))
258	257	3adant3r2 1078	. . . . . . . . . . . . . 14 |- ((J e. Top /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)(~=ph` J)((0[,]1) X. {Y}))
259	258	adantlr 429	. . . . . . . . . . . . 13 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)(~=ph` J)((0[,]1) X. {Y}))
260		oprex 4907	. . . . . . . . . . . . . . . 16 |- (0[,]1) e. _V
261		snex 3492	. . . . . . . . . . . . . . . 16 |- {Y} e. _V
262	260, 261	xpex 4096	. . . . . . . . . . . . . . 15 |- ((0[,]1) X. {Y}) e. _V
263	262	a1i 8	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ((0[,]1) X. {Y}) e. _V)
264		simpll 448	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> J e. Top)
265		simpr1 882	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> f e. (II Cn J))
266	240	a1i 8	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = (f` 0))
267		pcocn 16076	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} e. (II Cn J) /\ f e. (II Cn J) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}` 1) = (f` 0))) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f) e. (II Cn J))
268	264, 248, 265, 266, 267	syl13anc 1102	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f) e. (II Cn J))
269	268, 175	eleqtrrd 1974	. . . . . . . . . . . . . 14 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f) e. dom (~=ph` J))
270		erthdmg 15730	. . . . . . . . . . . . . 14 |- ((((0[,]1) X. {Y}) e. _V /\ Er (~=ph` J) /\ ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f) e. dom (~=ph` J)) -> ([({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)](~=ph` J) = [((0[,]1) X. {Y})](~=ph` J) <-> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)(~=ph` J)((0[,]1) X. {Y})))
271	263, 165, 269, 270	syl111anc 1100	. . . . . . . . . . . . 13 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)](~=ph` J) = [((0[,]1) X. {Y})](~=ph` J) <-> ({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)(~=ph` J)((0[,]1) X. {Y})))
272	259, 271	mpbird 213	. . . . . . . . . . . 12 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> [({<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))} (*p` J)f)](~=ph` J) = [((0[,]1) X. {Y})](~=ph` J))
273	256, 272	eqtrd 1925	. . . . . . . . . . 11 |- (((J e. Top /\ Y e. X) /\ (f e. (II Cn J) /\ (f` 0) = Y /\ (f` 1) = Y)) -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [((0[,]1) X. {Y})](~=ph` J))
274	273	3exp2 1086	. . . . . . . . . 10 |- ((J e. Top /\ Y e. X) -> (f e. (II Cn J) -> ((f` 0) = Y -> ((f` 1) = Y -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [((0[,]1) X. {Y})](~=ph` J)))))
275	274	imp43 397	. . . . . . . . 9 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ ((f` 0) = Y /\ (f` 1) = Y)) -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)[f](~=ph` J)) = [((0[,]1) X. {Y})](~=ph` J))
276	247, 275	sylan9eqr 1951	. . . . . . . 8 |- (((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ ((f` 0) = Y /\ (f` 1) = Y)) /\ x = [f](~=ph` J)) -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J))
277	276	anasss 488	. . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J))
278		opreq1 4889	. . . . . . . . 9 |- (n = [{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J) -> (n(pi1` <.J, Y>.)x) = ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)x))
279	278	eqeq1d 1892	. . . . . . . 8 |- (n = [{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J) -> ((n(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J) <-> ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J)))
280	279	rcla4ev 2381	. . . . . . 7 |- (([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J) e. (pi1b` <.J, Y>.) /\ ([{<.u, v>. | (u e. (0[,]1) /\ v = (f` (1 - u)))}](~=ph` J)(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J)) -> E.n e. (pi1b` <.J, Y>.)(n(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J))
281	246, 277, 280	syl11anc 524	. . . . . 6 |- ((((J e. Top /\ Y e. X) /\ f e. (II Cn J)) /\ (((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J))) -> E.n e. (pi1b` <.J, Y>.)(n(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J))
282	281	ex 402	. . . . 5 |- (((J e. Top /\ Y e. X) /\ f e. (II Cn J)) -> ((((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> E.n e. (pi1b` <.J, Y>.)(n(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J)))
283	282	r19.23adva 2216	. . . 4 |- ((J e. Top /\ Y e. X) -> (E.f e. (II Cn J)(((f` 0) = Y /\ (f` 1) = Y) /\ x = [f](~=ph` J)) -> E.n e. (pi1b` <.J, Y>.)(n(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J)))
284	5, 283	sylbid 220	. . 3 |- ((J e. Top /\ Y e. X) -> (x e. (pi1b` <.J, Y>.) -> E.n e. (pi1b` <.J, Y>.)(n(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J)))
285	284	imp 377	. 2 |- (((J e. Top /\ Y e. X) /\ x e. (pi1b` <.J, Y>.)) -> E.n e. (pi1b` <.J, Y>.)(n(pi1` <.J, Y>.)x) = [((0[,]1) X. {Y})](~=ph` J))
286	2, 4, 127, 152, 194, 285	isgrpda 16033	1 |- ((J e. Top /\ Y e. X) -> (pi1` <.J, Y>.) e. Grp)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wrex 2106  _Vcvv 2292   C_ wss 2593  {csn 3044  <.cop 3046  U.cuni 3177   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986   o. ccom 3990   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  Er wer 5315  [cec 5316  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   - cmin 6445   <_ cle 6448  [,]cicc 7527  -cn->ccncf 8524  Topctop 8857   Cn ccn 9028  Grpcgr 9311  IIcii 15865  ~=phcphtpc 16044  pi1bcpi1b 16066  *pcpco 16067  pi1cpi1 16068

This theorem is referenced by:  pi1set 16096

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-3 7155  df-4 7156  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-grp 9316  df-subsp 10243  df-ii 15866  df-phtpy 16045  df-phtpc 16057  df-pco 16069  df-pi1b 16070  df-pi1 16071

Copyright terms: Public domain