Theorem iscatd2 16342

Description: Version of iscatd 16334 with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypotheses

Ref	Expression
iscatd2.b	|- ( ph -> B = ( Base ` C ) )
iscatd2.h	|- ( ph -> H = ( Hom ` C ) )
iscatd2.o	|- ( ph -> .x. = (comp ` C ) )
iscatd2.c	|- ( ph -> C e. V )
iscatd2.ps	|- ( ps <-> ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
iscatd2.1	|- ( ( ph /\ y e. B ) -> .1. e. ( y H y ) )
iscatd2.2	|- ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
iscatd2.3	|- ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
iscatd2.4	|- ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
iscatd2.5	|- ( ( ph /\ ps ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )

Assertion

Ref	Expression
iscatd2	|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> .1. ) ) )

Distinct variable groups:   f, g, k, w, x, z, .1.   y, f, B, g, k, w, x, z   C, g, k, w, y, z   f, H, g, k, w, x, y, z   ph, f, g, k, w, x, y, z   .x. , f, g, k, w, x, y, z

Allowed substitution hints:   ps( x, y, z, w, f, g, k)   C( x, f)   .1. ( y)   V( x, y, z, w, f, g, k)

Proof of Theorem iscatd2

Dummy variables a r are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iscatd2.b	. . 3 |- ( ph -> B = ( Base ` C ) )
2		iscatd2.h	. . 3 |- ( ph -> H = ( Hom ` C ) )
3		iscatd2.o	. . 3 |- ( ph -> .x. = (comp ` C ) )
4		iscatd2.c	. . 3 |- ( ph -> C e. V )
5		iscatd2.1	. . 3 |- ( ( ph /\ y e. B ) -> .1. e. ( y H y ) )
6		ne0i 3921	. . . . . . 7 |- ( .1. e. ( y H y ) -> ( y H y ) =/= (/) )
7	5, 6	syl 17	. . . . . 6 |- ( ( ph /\ y e. B ) -> ( y H y ) =/= (/) )
8	7	3ad2antr1 1226	. . . . 5 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> ( y H y ) =/= (/) )
9		n0 3931	. . . . 5 |- ( ( y H y ) =/= (/) <-> E. g g e. ( y H y ) )
10	8, 9	sylib 208	. . . 4 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> E. g g e. ( y H y ) )
11		n0 3931	. . . . 5 |- ( ( y H y ) =/= (/) <-> E. k k e. ( y H y ) )
12	8, 11	sylib 208	. . . 4 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> E. k k e. ( y H y ) )
13		eeanv 2182	. . . . 5 |- ( E. g E. k ( g e. ( y H y ) /\ k e. ( y H y ) ) <-> ( E. g g e. ( y H y ) /\ E. k k e. ( y H y ) ) )
14		simpll 790	. . . . . . . 8 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> ph )
15		simplr2 1104	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> a e. B )
16		simplr1 1103	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> y e. B )
17	15, 16	jca 554	. . . . . . . 8 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> ( a e. B /\ y e. B ) )
18		simplr3 1105	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> r e. ( a H y ) )
19		simprl 794	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> g e. ( y H y ) )
20		simprr 796	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> k e. ( y H y ) )
21	18, 19, 20	3jca 1242	. . . . . . . 8 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) )
22		iscatd2.ps	. . . . . . . . . . . . . . 15 |- ( ps <-> ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
23		simplll 798	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> x = a )
24	23	eleq1d 2686	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( x e. B <-> a e. B ) )
25	24	anbi1d 741	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( x e. B /\ y e. B ) <-> ( a e. B /\ y e. B ) ) )
26		simpllr 799	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> z = y )
27	26	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( z e. B <-> y e. B ) )
28		simplr 792	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> w = y )
29	28	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( w e. B <-> y e. B ) )
30	27, 29	anbi12d 747	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( z e. B /\ w e. B ) <-> ( y e. B /\ y e. B ) ) )
31		anidm 676	. . . . . . . . . . . . . . . . 17 |- ( ( y e. B /\ y e. B ) <-> y e. B )
32	30, 31	syl6bb 276	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( z e. B /\ w e. B ) <-> y e. B ) )
33		simpr 477	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> f = r )
34	23	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( x H y ) = ( a H y ) )
35	33, 34	eleq12d 2695	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( f e. ( x H y ) <-> r e. ( a H y ) ) )
36	26	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( y H z ) = ( y H y ) )
37	36	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( g e. ( y H z ) <-> g e. ( y H y ) ) )
38	26, 28	oveq12d 6668	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( z H w ) = ( y H y ) )
39	38	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( k e. ( z H w ) <-> k e. ( y H y ) ) )
40	35, 37, 39	3anbi123d 1399	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) <-> ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) )
41	25, 32, 40	3anbi123d 1399	. . . . . . . . . . . . . . 15 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( a e. B /\ y e. B ) /\ y e. B /\ ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) ) )
42	22, 41	syl5bb 272	. . . . . . . . . . . . . 14 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ps <-> ( ( a e. B /\ y e. B ) /\ y e. B /\ ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) ) )
43	42	anbi2d 740	. . . . . . . . . . . . 13 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( ph /\ ps ) <-> ( ph /\ ( ( a e. B /\ y e. B ) /\ y e. B /\ ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) ) ) )
44	23	opeq1d 4408	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> <. x , y >. = <. a , y >. )
45	44	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( <. x , y >. .x. y ) = ( <. a , y >. .x. y ) )
46		eqidd 2623	. . . . . . . . . . . . . . 15 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> .1. = .1. )
47	45, 46, 33	oveq123d 6671	. . . . . . . . . . . . . 14 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( .1. ( <. x , y >. .x. y ) f ) = ( .1. ( <. a , y >. .x. y ) r ) )
48	47, 33	eqeq12d 2637	. . . . . . . . . . . . 13 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( .1. ( <. x , y >. .x. y ) f ) = f <-> ( .1. ( <. a , y >. .x. y ) r ) = r ) )
49	43, 48	imbi12d 334	. . . . . . . . . . . 12 |- ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f ) <-> ( ( ph /\ ( ( a e. B /\ y e. B ) /\ y e. B /\ ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r ) ) )
50	49	sbiedv 2410	. . . . . . . . . . 11 |- ( ( ( x = a /\ z = y ) /\ w = y ) -> ( [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f ) <-> ( ( ph /\ ( ( a e. B /\ y e. B ) /\ y e. B /\ ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r ) ) )
51	50	sbiedv 2410	. . . . . . . . . 10 |- ( ( x = a /\ z = y ) -> ( [ y / w ] [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f ) <-> ( ( ph /\ ( ( a e. B /\ y e. B ) /\ y e. B /\ ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r ) ) )
52	51	sbiedv 2410	. . . . . . . . 9 |- ( x = a -> ( [ y / z ] [ y / w ] [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f ) <-> ( ( ph /\ ( ( a e. B /\ y e. B ) /\ y e. B /\ ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r ) ) )
53		iscatd2.2	. . . . . . . . . . . 12 |- ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
54	53	sbt 2419	. . . . . . . . . . 11 |- [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
55	54	sbt 2419	. . . . . . . . . 10 |- [ y / w ] [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
56	55	sbt 2419	. . . . . . . . 9 |- [ y / z ] [ y / w ] [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
57	52, 56	chvarv 2263	. . . . . . . 8 |- ( ( ph /\ ( ( a e. B /\ y e. B ) /\ y e. B /\ ( r e. ( a H y ) /\ g e. ( y H y ) /\ k e. ( y H y ) ) ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r )
58	14, 17, 16, 21, 57	syl13anc 1328	. . . . . . 7 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r )
59	58	ex 450	. . . . . 6 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> ( ( g e. ( y H y ) /\ k e. ( y H y ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r ) )
60	59	exlimdvv 1862	. . . . 5 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> ( E. g E. k ( g e. ( y H y ) /\ k e. ( y H y ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r ) )
61	13, 60	syl5bir 233	. . . 4 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> ( ( E. g g e. ( y H y ) /\ E. k k e. ( y H y ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r ) )
62	10, 12, 61	mp2and 715	. . 3 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r )
63	7	3ad2antr1 1226	. . . . 5 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( y H y ) =/= (/) )
64		n0 3931	. . . . 5 |- ( ( y H y ) =/= (/) <-> E. f f e. ( y H y ) )
65	63, 64	sylib 208	. . . 4 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> E. f f e. ( y H y ) )
66		simpr2 1068	. . . . . 6 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> a e. B )
67	7	ralrimiva 2966	. . . . . . 7 |- ( ph -> A. y e. B ( y H y ) =/= (/) )
68	67	adantr 481	. . . . . 6 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> A. y e. B ( y H y ) =/= (/) )
69		id 22	. . . . . . . . 9 |- ( y = a -> y = a )
70	69, 69	oveq12d 6668	. . . . . . . 8 |- ( y = a -> ( y H y ) = ( a H a ) )
71	70	neeq1d 2853	. . . . . . 7 |- ( y = a -> ( ( y H y ) =/= (/) <-> ( a H a ) =/= (/) ) )
72	71	rspcv 3305	. . . . . 6 |- ( a e. B -> ( A. y e. B ( y H y ) =/= (/) -> ( a H a ) =/= (/) ) )
73	66, 68, 72	sylc 65	. . . . 5 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( a H a ) =/= (/) )
74		n0 3931	. . . . 5 |- ( ( a H a ) =/= (/) <-> E. k k e. ( a H a ) )
75	73, 74	sylib 208	. . . 4 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> E. k k e. ( a H a ) )
76		eeanv 2182	. . . . 5 |- ( E. f E. k ( f e. ( y H y ) /\ k e. ( a H a ) ) <-> ( E. f f e. ( y H y ) /\ E. k k e. ( a H a ) ) )
77		simpll 790	. . . . . . . 8 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> ph )
78		simplr1 1103	. . . . . . . 8 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> y e. B )
79		simplr2 1104	. . . . . . . 8 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> a e. B )
80		simprl 794	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> f e. ( y H y ) )
81		simplr3 1105	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> r e. ( y H a ) )
82		simprr 796	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> k e. ( a H a ) )
83	80, 81, 82	3jca 1242	. . . . . . . 8 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) )
84		simplll 798	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> x = y )
85	84	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( x e. B <-> y e. B ) )
86	85	anbi1d 741	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( x e. B /\ y e. B ) <-> ( y e. B /\ y e. B ) ) )
87	86, 31	syl6bb 276	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( x e. B /\ y e. B ) <-> y e. B ) )
88		simpllr 799	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> z = a )
89	88	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( z e. B <-> a e. B ) )
90		simplr 792	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> w = a )
91	90	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( w e. B <-> a e. B ) )
92	89, 91	anbi12d 747	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( z e. B /\ w e. B ) <-> ( a e. B /\ a e. B ) ) )
93		anidm 676	. . . . . . . . . . . . . . . . 17 |- ( ( a e. B /\ a e. B ) <-> a e. B )
94	92, 93	syl6bb 276	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( z e. B /\ w e. B ) <-> a e. B ) )
95	84	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( x H y ) = ( y H y ) )
96	95	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( f e. ( x H y ) <-> f e. ( y H y ) ) )
97		simpr 477	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> g = r )
98	88	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( y H z ) = ( y H a ) )
99	97, 98	eleq12d 2695	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( g e. ( y H z ) <-> r e. ( y H a ) ) )
100	88, 90	oveq12d 6668	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( z H w ) = ( a H a ) )
101	100	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( k e. ( z H w ) <-> k e. ( a H a ) ) )
102	96, 99, 101	3anbi123d 1399	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) <-> ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) )
103	87, 94, 102	3anbi123d 1399	. . . . . . . . . . . . . . 15 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( y e. B /\ a e. B /\ ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) ) )
104	22, 103	syl5bb 272	. . . . . . . . . . . . . 14 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ps <-> ( y e. B /\ a e. B /\ ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) ) )
105	104	anbi2d 740	. . . . . . . . . . . . 13 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( ph /\ ps ) <-> ( ph /\ ( y e. B /\ a e. B /\ ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) ) ) )
106	88	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( <. y , y >. .x. z ) = ( <. y , y >. .x. a ) )
107		eqidd 2623	. . . . . . . . . . . . . . 15 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> .1. = .1. )
108	106, 97, 107	oveq123d 6671	. . . . . . . . . . . . . 14 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( g ( <. y , y >. .x. z ) .1. ) = ( r ( <. y , y >. .x. a ) .1. ) )
109	108, 97	eqeq12d 2637	. . . . . . . . . . . . 13 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( g ( <. y , y >. .x. z ) .1. ) = g <-> ( r ( <. y , y >. .x. a ) .1. ) = r ) )
110	105, 109	imbi12d 334	. . . . . . . . . . . 12 |- ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g ) <-> ( ( ph /\ ( y e. B /\ a e. B /\ ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r ) ) )
111	110	sbiedv 2410	. . . . . . . . . . 11 |- ( ( ( x = y /\ z = a ) /\ w = a ) -> ( [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g ) <-> ( ( ph /\ ( y e. B /\ a e. B /\ ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r ) ) )
112	111	sbiedv 2410	. . . . . . . . . 10 |- ( ( x = y /\ z = a ) -> ( [ a / w ] [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g ) <-> ( ( ph /\ ( y e. B /\ a e. B /\ ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r ) ) )
113	112	sbiedv 2410	. . . . . . . . 9 |- ( x = y -> ( [ a / z ] [ a / w ] [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g ) <-> ( ( ph /\ ( y e. B /\ a e. B /\ ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r ) ) )
114		iscatd2.3	. . . . . . . . . . . 12 |- ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
115	114	sbt 2419	. . . . . . . . . . 11 |- [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
116	115	sbt 2419	. . . . . . . . . 10 |- [ a / w ] [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
117	116	sbt 2419	. . . . . . . . 9 |- [ a / z ] [ a / w ] [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
118	113, 117	chvarv 2263	. . . . . . . 8 |- ( ( ph /\ ( y e. B /\ a e. B /\ ( f e. ( y H y ) /\ r e. ( y H a ) /\ k e. ( a H a ) ) ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r )
119	77, 78, 79, 83, 118	syl13anc 1328	. . . . . . 7 |- ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r )
120	119	ex 450	. . . . . 6 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( ( f e. ( y H y ) /\ k e. ( a H a ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r ) )
121	120	exlimdvv 1862	. . . . 5 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( E. f E. k ( f e. ( y H y ) /\ k e. ( a H a ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r ) )
122	76, 121	syl5bir 233	. . . 4 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( ( E. f f e. ( y H y ) /\ E. k k e. ( a H a ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r ) )
123	65, 75, 122	mp2and 715	. . 3 |- ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r )
124	67	3ad2ant1 1082	. . . . . 6 |- ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> A. y e. B ( y H y ) =/= (/) )
125		simp23 1096	. . . . . 6 |- ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> z e. B )
126		id 22	. . . . . . . . 9 |- ( y = z -> y = z )
127	126, 126	oveq12d 6668	. . . . . . . 8 |- ( y = z -> ( y H y ) = ( z H z ) )
128	127	neeq1d 2853	. . . . . . 7 |- ( y = z -> ( ( y H y ) =/= (/) <-> ( z H z ) =/= (/) ) )
129	128	rspccva 3308	. . . . . 6 |- ( ( A. y e. B ( y H y ) =/= (/) /\ z e. B ) -> ( z H z ) =/= (/) )
130	124, 125, 129	syl2anc 693	. . . . 5 |- ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> ( z H z ) =/= (/) )
131		n0 3931	. . . . 5 |- ( ( z H z ) =/= (/) <-> E. k k e. ( z H z ) )
132	130, 131	sylib 208	. . . 4 |- ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> E. k k e. ( z H z ) )
133		eleq1 2689	. . . . . . . . . . . 12 |- ( x = y -> ( x e. B <-> y e. B ) )
134	133	3anbi1d 1403	. . . . . . . . . . 11 |- ( x = y -> ( ( x e. B /\ a e. B /\ z e. B ) <-> ( y e. B /\ a e. B /\ z e. B ) ) )
135		oveq1 6657	. . . . . . . . . . . . . 14 |- ( x = y -> ( x H a ) = ( y H a ) )
136	135	eleq2d 2687	. . . . . . . . . . . . 13 |- ( x = y -> ( r e. ( x H a ) <-> r e. ( y H a ) ) )
137	136	anbi1d 741	. . . . . . . . . . . 12 |- ( x = y -> ( ( r e. ( x H a ) /\ g e. ( a H z ) ) <-> ( r e. ( y H a ) /\ g e. ( a H z ) ) ) )
138	137	anbi1d 741	. . . . . . . . . . 11 |- ( x = y -> ( ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) <-> ( ( r e. ( y H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) )
139	134, 138	anbi12d 747	. . . . . . . . . 10 |- ( x = y -> ( ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) <-> ( ( y e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( y H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) )
140	139	anbi2d 740	. . . . . . . . 9 |- ( x = y -> ( ( ph /\ ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) <-> ( ph /\ ( ( y e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( y H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) ) )
141		opeq1 4402	. . . . . . . . . . . 12 |- ( x = y -> <. x , a >. = <. y , a >. )
142	141	oveq1d 6665	. . . . . . . . . . 11 |- ( x = y -> ( <. x , a >. .x. z ) = ( <. y , a >. .x. z ) )
143	142	oveqd 6667	. . . . . . . . . 10 |- ( x = y -> ( g ( <. x , a >. .x. z ) r ) = ( g ( <. y , a >. .x. z ) r ) )
144		oveq1 6657	. . . . . . . . . 10 |- ( x = y -> ( x H z ) = ( y H z ) )
145	143, 144	eleq12d 2695	. . . . . . . . 9 |- ( x = y -> ( ( g ( <. x , a >. .x. z ) r ) e. ( x H z ) <-> ( g ( <. y , a >. .x. z ) r ) e. ( y H z ) ) )
146	140, 145	imbi12d 334	. . . . . . . 8 |- ( x = y -> ( ( ( ph /\ ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) -> ( g ( <. x , a >. .x. z ) r ) e. ( x H z ) ) <-> ( ( ph /\ ( ( y e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( y H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) -> ( g ( <. y , a >. .x. z ) r ) e. ( y H z ) ) ) )
147		df-3an 1039	. . . . . . . . . . . . . . 15 |- ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
148	22, 147	bitri 264	. . . . . . . . . . . . . 14 |- ( ps <-> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
149		simpll 790	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> y = a )
150	149	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( y e. B <-> a e. B ) )
151	150	anbi2d 740	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( x e. B /\ y e. B ) <-> ( x e. B /\ a e. B ) ) )
152		simplr 792	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> w = z )
153	152	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( w e. B <-> z e. B ) )
154	153	anbi2d 740	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( z e. B /\ w e. B ) <-> ( z e. B /\ z e. B ) ) )
155		anidm 676	. . . . . . . . . . . . . . . . . 18 |- ( ( z e. B /\ z e. B ) <-> z e. B )
156	154, 155	syl6bb 276	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( z e. B /\ w e. B ) <-> z e. B ) )
157	151, 156	anbi12d 747	. . . . . . . . . . . . . . . 16 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) <-> ( ( x e. B /\ a e. B ) /\ z e. B ) ) )
158		df-3an 1039	. . . . . . . . . . . . . . . 16 |- ( ( x e. B /\ a e. B /\ z e. B ) <-> ( ( x e. B /\ a e. B ) /\ z e. B ) )
159	157, 158	syl6bbr 278	. . . . . . . . . . . . . . 15 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) <-> ( x e. B /\ a e. B /\ z e. B ) ) )
160		simpr 477	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> f = r )
161	149	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( x H y ) = ( x H a ) )
162	160, 161	eleq12d 2695	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( f e. ( x H y ) <-> r e. ( x H a ) ) )
163	149	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( y H z ) = ( a H z ) )
164	163	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( g e. ( y H z ) <-> g e. ( a H z ) ) )
165	152	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( z H w ) = ( z H z ) )
166	165	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( k e. ( z H w ) <-> k e. ( z H z ) ) )
167	162, 164, 166	3anbi123d 1399	. . . . . . . . . . . . . . . 16 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) <-> ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H z ) ) ) )
168		df-3an 1039	. . . . . . . . . . . . . . . 16 |- ( ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H z ) ) <-> ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) )
169	167, 168	syl6bb 276	. . . . . . . . . . . . . . 15 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) <-> ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) )
170	159, 169	anbi12d 747	. . . . . . . . . . . . . 14 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) )
171	148, 170	syl5bb 272	. . . . . . . . . . . . 13 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ps <-> ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) )
172	171	anbi2d 740	. . . . . . . . . . . 12 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( ph /\ ps ) <-> ( ph /\ ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) ) )
173	149	opeq2d 4409	. . . . . . . . . . . . . . 15 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> <. x , y >. = <. x , a >. )
174	173	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( <. x , y >. .x. z ) = ( <. x , a >. .x. z ) )
175		eqidd 2623	. . . . . . . . . . . . . 14 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> g = g )
176	174, 175, 160	oveq123d 6671	. . . . . . . . . . . . 13 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , a >. .x. z ) r ) )
177	176	eleq1d 2686	. . . . . . . . . . . 12 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) <-> ( g ( <. x , a >. .x. z ) r ) e. ( x H z ) ) )
178	172, 177	imbi12d 334	. . . . . . . . . . 11 |- ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) <-> ( ( ph /\ ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) -> ( g ( <. x , a >. .x. z ) r ) e. ( x H z ) ) ) )
179	178	sbiedv 2410	. . . . . . . . . 10 |- ( ( y = a /\ w = z ) -> ( [ r / f ] ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) <-> ( ( ph /\ ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) -> ( g ( <. x , a >. .x. z ) r ) e. ( x H z ) ) ) )
180	179	sbiedv 2410	. . . . . . . . 9 |- ( y = a -> ( [ z / w ] [ r / f ] ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) <-> ( ( ph /\ ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) -> ( g ( <. x , a >. .x. z ) r ) e. ( x H z ) ) ) )
181		iscatd2.4	. . . . . . . . . . 11 |- ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
182	181	sbt 2419	. . . . . . . . . 10 |- [ r / f ] ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
183	182	sbt 2419	. . . . . . . . 9 |- [ z / w ] [ r / f ] ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
184	180, 183	chvarv 2263	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( x H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) -> ( g ( <. x , a >. .x. z ) r ) e. ( x H z ) )
185	146, 184	chvarv 2263	. . . . . . 7 |- ( ( ph /\ ( ( y e. B /\ a e. B /\ z e. B ) /\ ( ( r e. ( y H a ) /\ g e. ( a H z ) ) /\ k e. ( z H z ) ) ) ) -> ( g ( <. y , a >. .x. z ) r ) e. ( y H z ) )
186	185	exp45 642	. . . . . 6 |- ( ph -> ( ( y e. B /\ a e. B /\ z e. B ) -> ( ( r e. ( y H a ) /\ g e. ( a H z ) ) -> ( k e. ( z H z ) -> ( g ( <. y , a >. .x. z ) r ) e. ( y H z ) ) ) ) )
187	186	3imp 1256	. . . . 5 |- ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> ( k e. ( z H z ) -> ( g ( <. y , a >. .x. z ) r ) e. ( y H z ) ) )
188	187	exlimdv 1861	. . . 4 |- ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> ( E. k k e. ( z H z ) -> ( g ( <. y , a >. .x. z ) r ) e. ( y H z ) ) )
189	132, 188	mpd 15	. . 3 |- ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> ( g ( <. y , a >. .x. z ) r ) e. ( y H z ) )
190	133	anbi1d 741	. . . . . . 7 |- ( x = y -> ( ( x e. B /\ a e. B ) <-> ( y e. B /\ a e. B ) ) )
191	190	anbi1d 741	. . . . . 6 |- ( x = y -> ( ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) <-> ( ( y e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) ) )
192	136	3anbi1d 1403	. . . . . 6 |- ( x = y -> ( ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) <-> ( r e. ( y H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) )
193	191, 192	3anbi23d 1402	. . . . 5 |- ( x = y -> ( ( ph /\ ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) <-> ( ph /\ ( ( y e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) ) )
194	141	oveq1d 6665	. . . . . . 7 |- ( x = y -> ( <. x , a >. .x. w ) = ( <. y , a >. .x. w ) )
195	194	oveqd 6667	. . . . . 6 |- ( x = y -> ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) = ( ( k ( <. a , z >. .x. w ) g ) ( <. y , a >. .x. w ) r ) )
196		opeq1 4402	. . . . . . . 8 |- ( x = y -> <. x , z >. = <. y , z >. )
197	196	oveq1d 6665	. . . . . . 7 |- ( x = y -> ( <. x , z >. .x. w ) = ( <. y , z >. .x. w ) )
198		eqidd 2623	. . . . . . 7 |- ( x = y -> k = k )
199	197, 198, 143	oveq123d 6671	. . . . . 6 |- ( x = y -> ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) = ( k ( <. y , z >. .x. w ) ( g ( <. y , a >. .x. z ) r ) ) )
200	195, 199	eqeq12d 2637	. . . . 5 |- ( x = y -> ( ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) <-> ( ( k ( <. a , z >. .x. w ) g ) ( <. y , a >. .x. w ) r ) = ( k ( <. y , z >. .x. w ) ( g ( <. y , a >. .x. z ) r ) ) ) )
201	193, 200	imbi12d 334	. . . 4 |- ( x = y -> ( ( ( ph /\ ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) -> ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) ) <-> ( ( ph /\ ( ( y e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) -> ( ( k ( <. a , z >. .x. w ) g ) ( <. y , a >. .x. w ) r ) = ( k ( <. y , z >. .x. w ) ( g ( <. y , a >. .x. z ) r ) ) ) ) )
202		simpl 473	. . . . . . . . . . . . . 14 |- ( ( y = a /\ f = r ) -> y = a )
203	202	eleq1d 2686	. . . . . . . . . . . . 13 |- ( ( y = a /\ f = r ) -> ( y e. B <-> a e. B ) )
204	203	anbi2d 740	. . . . . . . . . . . 12 |- ( ( y = a /\ f = r ) -> ( ( x e. B /\ y e. B ) <-> ( x e. B /\ a e. B ) ) )
205		simpr 477	. . . . . . . . . . . . . 14 |- ( ( y = a /\ f = r ) -> f = r )
206	202	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ( y = a /\ f = r ) -> ( x H y ) = ( x H a ) )
207	205, 206	eleq12d 2695	. . . . . . . . . . . . 13 |- ( ( y = a /\ f = r ) -> ( f e. ( x H y ) <-> r e. ( x H a ) ) )
208	202	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( ( y = a /\ f = r ) -> ( y H z ) = ( a H z ) )
209	208	eleq2d 2687	. . . . . . . . . . . . 13 |- ( ( y = a /\ f = r ) -> ( g e. ( y H z ) <-> g e. ( a H z ) ) )
210	207, 209	3anbi12d 1400	. . . . . . . . . . . 12 |- ( ( y = a /\ f = r ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) <-> ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) )
211	204, 210	3anbi13d 1401	. . . . . . . . . . 11 |- ( ( y = a /\ f = r ) -> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) ) )
212	22, 211	syl5bb 272	. . . . . . . . . 10 |- ( ( y = a /\ f = r ) -> ( ps <-> ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) ) )
213		df-3an 1039	. . . . . . . . . 10 |- ( ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) <-> ( ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) )
214	212, 213	syl6bb 276	. . . . . . . . 9 |- ( ( y = a /\ f = r ) -> ( ps <-> ( ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) ) )
215	214	anbi2d 740	. . . . . . . 8 |- ( ( y = a /\ f = r ) -> ( ( ph /\ ps ) <-> ( ph /\ ( ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) ) ) )
216		3anass 1042	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) <-> ( ph /\ ( ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) ) )
217	215, 216	syl6bbr 278	. . . . . . 7 |- ( ( y = a /\ f = r ) -> ( ( ph /\ ps ) <-> ( ph /\ ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) ) )
218	202	opeq2d 4409	. . . . . . . . . 10 |- ( ( y = a /\ f = r ) -> <. x , y >. = <. x , a >. )
219	218	oveq1d 6665	. . . . . . . . 9 |- ( ( y = a /\ f = r ) -> ( <. x , y >. .x. w ) = ( <. x , a >. .x. w ) )
220	202	opeq1d 4408	. . . . . . . . . . 11 |- ( ( y = a /\ f = r ) -> <. y , z >. = <. a , z >. )
221	220	oveq1d 6665	. . . . . . . . . 10 |- ( ( y = a /\ f = r ) -> ( <. y , z >. .x. w ) = ( <. a , z >. .x. w ) )
222	221	oveqd 6667	. . . . . . . . 9 |- ( ( y = a /\ f = r ) -> ( k ( <. y , z >. .x. w ) g ) = ( k ( <. a , z >. .x. w ) g ) )
223	219, 222, 205	oveq123d 6671	. . . . . . . 8 |- ( ( y = a /\ f = r ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) )
224	218	oveq1d 6665	. . . . . . . . . 10 |- ( ( y = a /\ f = r ) -> ( <. x , y >. .x. z ) = ( <. x , a >. .x. z ) )
225		eqidd 2623	. . . . . . . . . 10 |- ( ( y = a /\ f = r ) -> g = g )
226	224, 225, 205	oveq123d 6671	. . . . . . . . 9 |- ( ( y = a /\ f = r ) -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , a >. .x. z ) r ) )
227	226	oveq2d 6666	. . . . . . . 8 |- ( ( y = a /\ f = r ) -> ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) )
228	223, 227	eqeq12d 2637	. . . . . . 7 |- ( ( y = a /\ f = r ) -> ( ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) <-> ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) ) )
229	217, 228	imbi12d 334	. . . . . 6 |- ( ( y = a /\ f = r ) -> ( ( ( ph /\ ps ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) <-> ( ( ph /\ ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) -> ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) ) ) )
230	229	sbiedv 2410	. . . . 5 |- ( y = a -> ( [ r / f ] ( ( ph /\ ps ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) <-> ( ( ph /\ ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) -> ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) ) ) )
231		iscatd2.5	. . . . . 6 |- ( ( ph /\ ps ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )
232	231	sbt 2419	. . . . 5 |- [ r / f ] ( ( ph /\ ps ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )
233	230, 232	chvarv 2263	. . . 4 |- ( ( ph /\ ( ( x e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( x H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) -> ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) )
234	201, 233	chvarv 2263	. . 3 |- ( ( ph /\ ( ( y e. B /\ a e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) /\ k e. ( z H w ) ) ) -> ( ( k ( <. a , z >. .x. w ) g ) ( <. y , a >. .x. w ) r ) = ( k ( <. y , z >. .x. w ) ( g ( <. y , a >. .x. z ) r ) ) )
235	1, 2, 3, 4, 5, 62, 123, 189, 234	iscatd 16334	. 2 |- ( ph -> C e. Cat )
236	1, 2, 3, 235, 5, 62, 123	catidd 16341	. 2 |- ( ph -> ( Id ` C ) = ( y e. B |-> .1. ) )
237	235, 236	jca 554	1 |- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> .1. ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   [wsb 1880   e. wcel 1990   =/= wne 2794   A.wral 2912   (/)c0 3915   <.cop 4183   |-> cmpt 4729   ` cfv 5888  (class class class)co 6650   Basecbs 15857   Hom chom 15952  compcco 15953   Catccat 16325   Idccid 16326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-cat 16329  df-cid 16330

This theorem is referenced by:  oppccatid  16379  subccatid  16506  fuccatid  16629  setccatid  16734  catccatid  16752  estrccatid  16772  xpccatid  16828  rngccatidALTV  41989  ringccatidALTV  42052