Metamath Proof Explorer

Theorem iscatd2

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

Ref Expression
Hypotheses 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 iscatd2 
|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> .1. ) ) )

Proof

Step Hyp Ref Expression
1 iscatd2.b 
 |-  ( ph -> B = ( Base ` C ) )
2 iscatd2.h 
 |-  ( ph -> H = ( Hom ` C ) )
3 iscatd2.o 
 |-  ( ph -> .x. = ( comp ` C ) )
4 iscatd2.c 
 |-  ( ph -> C e. V )
5 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 ) ) ) )
6 iscatd2.1 
 |-  ( ( ph /\ y e. B ) -> .1. e. ( y H y ) )
7 iscatd2.2 
 |-  ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
8 iscatd2.3 
 |-  ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
9 iscatd2.4 
 |-  ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
10 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 ) ) )
11 6 ne0d 
 |-  ( ( ph /\ y e. B ) -> ( y H y ) =/= (/) )
12 11 3ad2antr1 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> ( y H y ) =/= (/) )
13 n0 
 |-  ( ( y H y ) =/= (/) <-> E. g g e. ( y H y ) )
14 12 13 sylib 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> E. g g e. ( y H y ) )
15 n0 
 |-  ( ( y H y ) =/= (/) <-> E. k k e. ( y H y ) )
16 12 15 sylib 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> E. k k e. ( y H y ) )
17 exdistrv 
 |-  ( 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 ) ) )
18 simpll 
 |-  ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) /\ ( g e. ( y H y ) /\ k e. ( y H y ) ) ) -> ph )
19 simplr2 
 |-  ( ( ( 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 )
20 simplr1 
 |-  ( ( ( 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 )
21 19 20 jca 
 |-  ( ( ( 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 ) )
22 simplr3 
 |-  ( ( ( 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 ) )
23 simprl 
 |-  ( ( ( 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 ) )
24 simprr 
 |-  ( ( ( 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 ) )
25 22 23 24 3jca 
 |-  ( ( ( 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 ) ) )
26 simplll 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> x = a )
27 26 eleq1d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( x e. B <-> a e. B ) )
28 27 anbi1d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( x e. B /\ y e. B ) <-> ( a e. B /\ y e. B ) ) )
29 simpllr 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> z = y )
30 29 eleq1d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( z e. B <-> y e. B ) )
31 simplr 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> w = y )
32 31 eleq1d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( w e. B <-> y e. B ) )
33 30 32 anbi12d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( z e. B /\ w e. B ) <-> ( y e. B /\ y e. B ) ) )
34 anidm 
 |-  ( ( y e. B /\ y e. B ) <-> y e. B )
35 33 34 bitrdi 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( z e. B /\ w e. B ) <-> y e. B ) )
36 simpr 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> f = r )
37 26 oveq1d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( x H y ) = ( a H y ) )
38 36 37 eleq12d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( f e. ( x H y ) <-> r e. ( a H y ) ) )
39 29 oveq2d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( y H z ) = ( y H y ) )
40 39 eleq2d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( g e. ( y H z ) <-> g e. ( y H y ) ) )
41 29 31 oveq12d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( z H w ) = ( y H y ) )
42 41 eleq2d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( k e. ( z H w ) <-> k e. ( y H y ) ) )
43 38 40 42 3anbi123d 
 |-  ( ( ( ( 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 ) ) ) )
44 28 35 43 3anbi123d 
 |-  ( ( ( ( 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 ) ) ) ) )
45 5 44 syl5bb 
 |-  ( ( ( ( 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 ) ) ) ) )
46 45 anbi2d 
 |-  ( ( ( ( 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 ) ) ) ) ) )
47 26 opeq1d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> <. x , y >. = <. a , y >. )
48 47 oveq1d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( <. x , y >. .x. y ) = ( <. a , y >. .x. y ) )
49 eqidd 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> .1. = .1. )
50 48 49 36 oveq123d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( .1. ( <. x , y >. .x. y ) f ) = ( .1. ( <. a , y >. .x. y ) r ) )
51 50 36 eqeq12d 
 |-  ( ( ( ( x = a /\ z = y ) /\ w = y ) /\ f = r ) -> ( ( .1. ( <. x , y >. .x. y ) f ) = f <-> ( .1. ( <. a , y >. .x. y ) r ) = r ) )
52 46 51 imbi12d 
 |-  ( ( ( ( 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 ) ) )
53 52 sbiedvw 
 |-  ( ( ( 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 ) ) )
54 53 sbiedvw 
 |-  ( ( 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 ) ) )
55 54 sbiedvw 
 |-  ( 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 ) ) )
56 7 sbt 
 |-  [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
57 56 sbt 
 |-  [ y / w ] [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
58 57 sbt 
 |-  [ y / z ] [ y / w ] [ r / f ] ( ( ph /\ ps ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
59 55 58 chvarvv 
 |-  ( ( 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 )
60 18 21 20 25 59 syl13anc 
 |-  ( ( ( 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 )
61 60 ex 
 |-  ( ( 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 ) )
62 61 exlimdvv 
 |-  ( ( 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 ) )
63 17 62 syl5bir 
 |-  ( ( 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 ) )
64 14 16 63 mp2and 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( a H y ) ) ) -> ( .1. ( <. a , y >. .x. y ) r ) = r )
65 11 3ad2antr1 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( y H y ) =/= (/) )
66 n0 
 |-  ( ( y H y ) =/= (/) <-> E. f f e. ( y H y ) )
67 65 66 sylib 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> E. f f e. ( y H y ) )
68 id 
 |-  ( y = a -> y = a )
69 68 68 oveq12d 
 |-  ( y = a -> ( y H y ) = ( a H a ) )
70 69 neeq1d 
 |-  ( y = a -> ( ( y H y ) =/= (/) <-> ( a H a ) =/= (/) ) )
71 11 ralrimiva 
 |-  ( ph -> A. y e. B ( y H y ) =/= (/) )
72 71 adantr 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> A. y e. B ( y H y ) =/= (/) )
73 simpr2 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> a e. B )
74 70 72 73 rspcdva 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( a H a ) =/= (/) )
75 n0 
 |-  ( ( a H a ) =/= (/) <-> E. k k e. ( a H a ) )
76 74 75 sylib 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> E. k k e. ( a H a ) )
77 exdistrv 
 |-  ( 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 ) ) )
78 simpll 
 |-  ( ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) /\ ( f e. ( y H y ) /\ k e. ( a H a ) ) ) -> ph )
79 simplr1 
 |-  ( ( ( 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 )
80 simplr2 
 |-  ( ( ( 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 )
81 simprl 
 |-  ( ( ( 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 ) )
82 simplr3 
 |-  ( ( ( 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 ) )
83 simprr 
 |-  ( ( ( 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 ) )
84 81 82 83 3jca 
 |-  ( ( ( 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 ) ) )
85 simplll 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> x = y )
86 85 eleq1d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( x e. B <-> y e. B ) )
87 86 anbi1d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( x e. B /\ y e. B ) <-> ( y e. B /\ y e. B ) ) )
88 87 34 bitrdi 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( x e. B /\ y e. B ) <-> y e. B ) )
89 simpllr 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> z = a )
90 89 eleq1d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( z e. B <-> a e. B ) )
91 simplr 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> w = a )
92 91 eleq1d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( w e. B <-> a e. B ) )
93 90 92 anbi12d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( z e. B /\ w e. B ) <-> ( a e. B /\ a e. B ) ) )
94 anidm 
 |-  ( ( a e. B /\ a e. B ) <-> a e. B )
95 93 94 bitrdi 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( z e. B /\ w e. B ) <-> a e. B ) )
96 85 oveq1d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( x H y ) = ( y H y ) )
97 96 eleq2d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( f e. ( x H y ) <-> f e. ( y H y ) ) )
98 simpr 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> g = r )
99 89 oveq2d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( y H z ) = ( y H a ) )
100 98 99 eleq12d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( g e. ( y H z ) <-> r e. ( y H a ) ) )
101 89 91 oveq12d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( z H w ) = ( a H a ) )
102 101 eleq2d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( k e. ( z H w ) <-> k e. ( a H a ) ) )
103 97 100 102 3anbi123d 
 |-  ( ( ( ( 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 ) ) ) )
104 88 95 103 3anbi123d 
 |-  ( ( ( ( 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 ) ) ) ) )
105 5 104 syl5bb 
 |-  ( ( ( ( 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 ) ) ) ) )
106 105 anbi2d 
 |-  ( ( ( ( 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 ) ) ) ) ) )
107 89 oveq2d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( <. y , y >. .x. z ) = ( <. y , y >. .x. a ) )
108 eqidd 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> .1. = .1. )
109 107 98 108 oveq123d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( g ( <. y , y >. .x. z ) .1. ) = ( r ( <. y , y >. .x. a ) .1. ) )
110 109 98 eqeq12d 
 |-  ( ( ( ( x = y /\ z = a ) /\ w = a ) /\ g = r ) -> ( ( g ( <. y , y >. .x. z ) .1. ) = g <-> ( r ( <. y , y >. .x. a ) .1. ) = r ) )
111 106 110 imbi12d 
 |-  ( ( ( ( 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 ) ) )
112 111 sbiedvw 
 |-  ( ( ( 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 ) ) )
113 112 sbiedvw 
 |-  ( ( 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 ) ) )
114 113 sbiedvw 
 |-  ( 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 ) ) )
115 8 sbt 
 |-  [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
116 115 sbt 
 |-  [ a / w ] [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
117 116 sbt 
 |-  [ a / z ] [ a / w ] [ r / g ] ( ( ph /\ ps ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
118 114 117 chvarvv 
 |-  ( ( 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 78 79 80 84 118 syl13anc 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 77 121 syl5bir 
 |-  ( ( 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 67 76 122 mp2and 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ r e. ( y H a ) ) ) -> ( r ( <. y , y >. .x. a ) .1. ) = r )
124 id 
 |-  ( y = z -> y = z )
125 124 124 oveq12d 
 |-  ( y = z -> ( y H y ) = ( z H z ) )
126 125 neeq1d 
 |-  ( y = z -> ( ( y H y ) =/= (/) <-> ( z H z ) =/= (/) ) )
127 71 3ad2ant1 
 |-  ( ( 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 ) =/= (/) )
128 simp23 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> z e. B )
129 126 127 128 rspcdva 
 |-  ( ( ph /\ ( y e. B /\ a e. B /\ z e. B ) /\ ( r e. ( y H a ) /\ g e. ( a H z ) ) ) -> ( z H z ) =/= (/) )
130 n0 
 |-  ( ( z H z ) =/= (/) <-> E. k k e. ( z H z ) )
131 129 130 sylib 
 |-  ( ( 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 ) )
132 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
133 132 3anbi1d 
 |-  ( x = y -> ( ( x e. B /\ a e. B /\ z e. B ) <-> ( y e. B /\ a e. B /\ z e. B ) ) )
134 oveq1 
 |-  ( x = y -> ( x H a ) = ( y H a ) )
135 134 eleq2d 
 |-  ( x = y -> ( r e. ( x H a ) <-> r e. ( y H a ) ) )
136 135 anbi1d 
 |-  ( x = y -> ( ( r e. ( x H a ) /\ g e. ( a H z ) ) <-> ( r e. ( y H a ) /\ g e. ( a H z ) ) ) )
137 136 anbi1d 
 |-  ( 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 ) ) ) )
138 133 137 anbi12d 
 |-  ( 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 ) ) ) ) )
139 138 anbi2d 
 |-  ( 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 ) ) ) ) ) )
140 opeq1 
 |-  ( x = y -> <. x , a >. = <. y , a >. )
141 140 oveq1d 
 |-  ( x = y -> ( <. x , a >. .x. z ) = ( <. y , a >. .x. z ) )
142 141 oveqd 
 |-  ( x = y -> ( g ( <. x , a >. .x. z ) r ) = ( g ( <. y , a >. .x. z ) r ) )
143 oveq1 
 |-  ( x = y -> ( x H z ) = ( y H z ) )
144 142 143 eleq12d 
 |-  ( x = y -> ( ( g ( <. x , a >. .x. z ) r ) e. ( x H z ) <-> ( g ( <. y , a >. .x. z ) r ) e. ( y H z ) ) )
145 139 144 imbi12d 
 |-  ( 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 ) ) ) )
146 df-3an 
 |-  ( ( ( 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 ) ) ) )
147 5 146 bitri 
 |-  ( 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 ) ) ) )
148 simpll 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> y = a )
149 148 eleq1d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( y e. B <-> a e. B ) )
150 149 anbi2d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( x e. B /\ y e. B ) <-> ( x e. B /\ a e. B ) ) )
151 simplr 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> w = z )
152 151 eleq1d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( w e. B <-> z e. B ) )
153 152 anbi2d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( z e. B /\ w e. B ) <-> ( z e. B /\ z e. B ) ) )
154 anidm 
 |-  ( ( z e. B /\ z e. B ) <-> z e. B )
155 153 154 bitrdi 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( ( z e. B /\ w e. B ) <-> z e. B ) )
156 150 155 anbi12d 
 |-  ( ( ( 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 ) ) )
157 df-3an 
 |-  ( ( x e. B /\ a e. B /\ z e. B ) <-> ( ( x e. B /\ a e. B ) /\ z e. B ) )
158 156 157 bitr4di 
 |-  ( ( ( 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 ) ) )
159 simpr 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> f = r )
160 148 oveq2d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( x H y ) = ( x H a ) )
161 159 160 eleq12d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( f e. ( x H y ) <-> r e. ( x H a ) ) )
162 148 oveq1d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( y H z ) = ( a H z ) )
163 162 eleq2d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( g e. ( y H z ) <-> g e. ( a H z ) ) )
164 151 oveq2d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( z H w ) = ( z H z ) )
165 164 eleq2d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( k e. ( z H w ) <-> k e. ( z H z ) ) )
166 161 163 165 3anbi123d 
 |-  ( ( ( 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 ) ) ) )
167 df-3an 
 |-  ( ( 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 ) ) )
168 166 167 bitrdi 
 |-  ( ( ( 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 ) ) ) )
169 158 168 anbi12d 
 |-  ( ( ( 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 ) ) ) ) )
170 147 169 syl5bb 
 |-  ( ( ( 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 ) ) ) ) )
171 170 anbi2d 
 |-  ( ( ( 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 ) ) ) ) ) )
172 148 opeq2d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> <. x , y >. = <. x , a >. )
173 172 oveq1d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( <. x , y >. .x. z ) = ( <. x , a >. .x. z ) )
174 eqidd 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> g = g )
175 173 174 159 oveq123d 
 |-  ( ( ( y = a /\ w = z ) /\ f = r ) -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , a >. .x. z ) r ) )
176 175 eleq1d 
 |-  ( ( ( 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 ) ) )
177 171 176 imbi12d 
 |-  ( ( ( 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 ) ) ) )
178 177 sbiedvw 
 |-  ( ( 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 ) ) ) )
179 178 sbiedvw 
 |-  ( 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 ) ) ) )
180 9 sbt 
 |-  [ r / f ] ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
181 180 sbt 
 |-  [ z / w ] [ r / f ] ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
182 179 181 chvarvv 
 |-  ( ( 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 ) )
183 145 182 chvarvv 
 |-  ( ( 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 ) )
184 183 exp45 
 |-  ( 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 ) ) ) ) )
185 184 3imp 
 |-  ( ( 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 exlimdv 
 |-  ( ( 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 ) ) )
187 131 186 mpd 
 |-  ( ( 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 ) )
188 132 anbi1d 
 |-  ( x = y -> ( ( x e. B /\ a e. B ) <-> ( y e. B /\ a e. B ) ) )
189 188 anbi1d 
 |-  ( 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 ) ) ) )
190 135 3anbi1d 
 |-  ( 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 ) ) ) )
191 189 190 3anbi23d 
 |-  ( 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 ) ) ) ) )
192 140 oveq1d 
 |-  ( x = y -> ( <. x , a >. .x. w ) = ( <. y , a >. .x. w ) )
193 192 oveqd 
 |-  ( x = y -> ( ( k ( <. a , z >. .x. w ) g ) ( <. x , a >. .x. w ) r ) = ( ( k ( <. a , z >. .x. w ) g ) ( <. y , a >. .x. w ) r ) )
194 opeq1 
 |-  ( x = y -> <. x , z >. = <. y , z >. )
195 194 oveq1d 
 |-  ( x = y -> ( <. x , z >. .x. w ) = ( <. y , z >. .x. w ) )
196 eqidd 
 |-  ( x = y -> k = k )
197 195 196 142 oveq123d 
 |-  ( x = y -> ( k ( <. x , z >. .x. w ) ( g ( <. x , a >. .x. z ) r ) ) = ( k ( <. y , z >. .x. w ) ( g ( <. y , a >. .x. z ) r ) ) )
198 193 197 eqeq12d 
 |-  ( 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 ) ) ) )
199 191 198 imbi12d 
 |-  ( 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 ) ) ) ) )
200 simpl 
 |-  ( ( y = a /\ f = r ) -> y = a )
201 200 eleq1d 
 |-  ( ( y = a /\ f = r ) -> ( y e. B <-> a e. B ) )
202 201 anbi2d 
 |-  ( ( y = a /\ f = r ) -> ( ( x e. B /\ y e. B ) <-> ( x e. B /\ a e. B ) ) )
203 simpr 
 |-  ( ( y = a /\ f = r ) -> f = r )
204 200 oveq2d 
 |-  ( ( y = a /\ f = r ) -> ( x H y ) = ( x H a ) )
205 203 204 eleq12d 
 |-  ( ( y = a /\ f = r ) -> ( f e. ( x H y ) <-> r e. ( x H a ) ) )
206 200 oveq1d 
 |-  ( ( y = a /\ f = r ) -> ( y H z ) = ( a H z ) )
207 206 eleq2d 
 |-  ( ( y = a /\ f = r ) -> ( g e. ( y H z ) <-> g e. ( a H z ) ) )
208 205 207 3anbi12d 
 |-  ( ( 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 ) ) ) )
209 202 208 3anbi13d 
 |-  ( ( 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 ) ) ) ) )
210 5 209 syl5bb 
 |-  ( ( 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 ) ) ) ) )
211 df-3an 
 |-  ( ( ( 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 ) ) ) )
212 210 211 bitrdi 
 |-  ( ( 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 212 anbi2d 
 |-  ( ( 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 ) ) ) ) ) )
214 3anass 
 |-  ( ( 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 ) ) ) ) )
215 213 214 bitr4di 
 |-  ( ( 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 200 opeq2d 
 |-  ( ( y = a /\ f = r ) -> <. x , y >. = <. x , a >. )
217 216 oveq1d 
 |-  ( ( y = a /\ f = r ) -> ( <. x , y >. .x. w ) = ( <. x , a >. .x. w ) )
218 200 opeq1d 
 |-  ( ( y = a /\ f = r ) -> <. y , z >. = <. a , z >. )
219 218 oveq1d 
 |-  ( ( y = a /\ f = r ) -> ( <. y , z >. .x. w ) = ( <. a , z >. .x. w ) )
220 219 oveqd 
 |-  ( ( y = a /\ f = r ) -> ( k ( <. y , z >. .x. w ) g ) = ( k ( <. a , z >. .x. w ) g ) )
221 217 220 203 oveq123d 
 |-  ( ( 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 ) )
222 216 oveq1d 
 |-  ( ( y = a /\ f = r ) -> ( <. x , y >. .x. z ) = ( <. x , a >. .x. z ) )
223 eqidd 
 |-  ( ( y = a /\ f = r ) -> g = g )
224 222 223 203 oveq123d 
 |-  ( ( y = a /\ f = r ) -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , a >. .x. z ) r ) )
225 224 oveq2d 
 |-  ( ( 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 ) ) )
226 221 225 eqeq12d 
 |-  ( ( 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 ) ) ) )
227 215 226 imbi12d 
 |-  ( ( 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 ) ) ) ) )
228 227 sbiedvw 
 |-  ( 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 ) ) ) ) )
229 10 sbt 
 |-  [ 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 ) ) )
230 228 229 chvarvv 
 |-  ( ( 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 199 230 chvarvv 
 |-  ( ( 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 ) ) )
232 1 2 3 4 6 64 123 187 231 iscatd 
 |-  ( ph -> C e. Cat )
233 1 2 3 232 6 64 123 catidd 
 |-  ( ph -> ( Id ` C ) = ( y e. B |-> .1. ) )
234 232 233 jca 
 |-  ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> .1. ) ) )