Metamath Proof Explorer

Theorem isnat

Description: Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natfval.1 
|- N = ( C Nat D )
natfval.b 
|- B = ( Base ` C )
natfval.h 
|- H = ( Hom ` C )
natfval.j 
|- J = ( Hom ` D )
natfval.o 
|- .x. = ( comp ` D )
isnat.f 
|- ( ph -> F ( C Func D ) G )
isnat.g 
|- ( ph -> K ( C Func D ) L )
Assertion isnat 
|- ( ph -> ( A e. ( <. F , G >. N <. K , L >. ) <-> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 natfval.1 
 |-  N = ( C Nat D )
2 natfval.b 
 |-  B = ( Base ` C )
3 natfval.h 
 |-  H = ( Hom ` C )
4 natfval.j 
 |-  J = ( Hom ` D )
5 natfval.o 
 |-  .x. = ( comp ` D )
6 isnat.f 
 |-  ( ph -> F ( C Func D ) G )
7 isnat.g 
 |-  ( ph -> K ( C Func D ) L )
8 1 2 3 4 5 natfval 
 |-  N = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } )
9 8 a1i 
 |-  ( ph -> N = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } ) )
10 fvexd 
 |-  ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) -> ( 1st ` f ) e. _V )
11 simprl 
 |-  ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) -> f = <. F , G >. )
12 11 fveq2d 
 |-  ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) -> ( 1st ` f ) = ( 1st ` <. F , G >. ) )
13 relfunc 
 |-  Rel ( C Func D )
14 brrelex12 
 |-  ( ( Rel ( C Func D ) /\ F ( C Func D ) G ) -> ( F e. _V /\ G e. _V ) )
15 13 6 14 sylancr 
 |-  ( ph -> ( F e. _V /\ G e. _V ) )
16 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
17 15 16 syl 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
18 17 adantr 
 |-  ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) -> ( 1st ` <. F , G >. ) = F )
19 12 18 eqtrd 
 |-  ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) -> ( 1st ` f ) = F )
20 fvexd 
 |-  ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) -> ( 1st ` g ) e. _V )
21 simplrr 
 |-  ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) -> g = <. K , L >. )
22 21 fveq2d 
 |-  ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) -> ( 1st ` g ) = ( 1st ` <. K , L >. ) )
23 brrelex12 
 |-  ( ( Rel ( C Func D ) /\ K ( C Func D ) L ) -> ( K e. _V /\ L e. _V ) )
24 13 7 23 sylancr 
 |-  ( ph -> ( K e. _V /\ L e. _V ) )
25 op1stg 
 |-  ( ( K e. _V /\ L e. _V ) -> ( 1st ` <. K , L >. ) = K )
26 24 25 syl 
 |-  ( ph -> ( 1st ` <. K , L >. ) = K )
27 26 ad2antrr 
 |-  ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) -> ( 1st ` <. K , L >. ) = K )
28 22 27 eqtrd 
 |-  ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) -> ( 1st ` g ) = K )
29 simplr 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> r = F )
30 29 fveq1d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( r ` x ) = ( F ` x ) )
31 simpr 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> s = K )
32 31 fveq1d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( s ` x ) = ( K ` x ) )
33 30 32 oveq12d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( ( r ` x ) J ( s ` x ) ) = ( ( F ` x ) J ( K ` x ) ) )
34 33 ixpeq2dv 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> X_ x e. B ( ( r ` x ) J ( s ` x ) ) = X_ x e. B ( ( F ` x ) J ( K ` x ) ) )
35 29 fveq1d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( r ` y ) = ( F ` y ) )
36 30 35 opeq12d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> <. ( r ` x ) , ( r ` y ) >. = <. ( F ` x ) , ( F ` y ) >. )
37 31 fveq1d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( s ` y ) = ( K ` y ) )
38 36 37 oveq12d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) = ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) )
39 eqidd 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( a ` y ) = ( a ` y ) )
40 11 ad2antrr 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> f = <. F , G >. )
41 40 fveq2d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( 2nd ` f ) = ( 2nd ` <. F , G >. ) )
42 op2ndg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 2nd ` <. F , G >. ) = G )
43 15 42 syl 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
44 43 ad3antrrr 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( 2nd ` <. F , G >. ) = G )
45 41 44 eqtrd 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( 2nd ` f ) = G )
46 45 oveqd 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( x ( 2nd ` f ) y ) = ( x G y ) )
47 46 fveq1d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( ( x ( 2nd ` f ) y ) ` h ) = ( ( x G y ) ` h ) )
48 38 39 47 oveq123d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) )
49 30 32 opeq12d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> <. ( r ` x ) , ( s ` x ) >. = <. ( F ` x ) , ( K ` x ) >. )
50 49 37 oveq12d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) = ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) )
51 21 adantr 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> g = <. K , L >. )
52 51 fveq2d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( 2nd ` g ) = ( 2nd ` <. K , L >. ) )
53 op2ndg 
 |-  ( ( K e. _V /\ L e. _V ) -> ( 2nd ` <. K , L >. ) = L )
54 24 53 syl 
 |-  ( ph -> ( 2nd ` <. K , L >. ) = L )
55 54 ad3antrrr 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( 2nd ` <. K , L >. ) = L )
56 52 55 eqtrd 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( 2nd ` g ) = L )
57 56 oveqd 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( x ( 2nd ` g ) y ) = ( x L y ) )
58 57 fveq1d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( ( x ( 2nd ` g ) y ) ` h ) = ( ( x L y ) ` h ) )
59 eqidd 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( a ` x ) = ( a ` x ) )
60 50 58 59 oveq123d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) )
61 48 60 eqeq12d 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) <-> ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) ) )
62 61 ralbidv 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) <-> A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) ) )
63 62 2ralbidv 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> ( A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) <-> A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) ) )
64 34 63 rabeqbidv 
 |-  ( ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) /\ s = K ) -> { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } = { a e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) } )
65 20 28 64 csbied2 
 |-  ( ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) /\ r = F ) -> [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } = { a e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) } )
66 10 19 65 csbied2 
 |-  ( ( ph /\ ( f = <. F , G >. /\ g = <. K , L >. ) ) -> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } = { a e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) } )
67 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
68 6 67 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
69 df-br 
 |-  ( K ( C Func D ) L <-> <. K , L >. e. ( C Func D ) )
70 7 69 sylib 
 |-  ( ph -> <. K , L >. e. ( C Func D ) )
71 ovex 
 |-  ( ( F ` x ) J ( K ` x ) ) e. _V
72 71 rgenw 
 |-  A. x e. B ( ( F ` x ) J ( K ` x ) ) e. _V
73 ixpexg 
 |-  ( A. x e. B ( ( F ` x ) J ( K ` x ) ) e. _V -> X_ x e. B ( ( F ` x ) J ( K ` x ) ) e. _V )
74 72 73 ax-mp 
 |-  X_ x e. B ( ( F ` x ) J ( K ` x ) ) e. _V
75 74 rabex 
 |-  { a e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) } e. _V
76 75 a1i 
 |-  ( ph -> { a e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) } e. _V )
77 9 66 68 70 76 ovmpod 
 |-  ( ph -> ( <. F , G >. N <. K , L >. ) = { a e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) } )
78 77 eleq2d 
 |-  ( ph -> ( A e. ( <. F , G >. N <. K , L >. ) <-> A e. { a e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) } ) )
79 fveq1 
 |-  ( a = A -> ( a ` y ) = ( A ` y ) )
80 79 oveq1d 
 |-  ( a = A -> ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) )
81 fveq1 
 |-  ( a = A -> ( a ` x ) = ( A ` x ) )
82 81 oveq2d 
 |-  ( a = A -> ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) )
83 80 82 eqeq12d 
 |-  ( a = A -> ( ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) <-> ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) )
84 83 ralbidv 
 |-  ( a = A -> ( A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) <-> A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) )
85 84 2ralbidv 
 |-  ( a = A -> ( A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) <-> A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) )
86 85 elrab 
 |-  ( A e. { a e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( a ` x ) ) } <-> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) )
87 78 86 bitrdi 
 |-  ( ph -> ( A e. ( <. F , G >. N <. K , L >. ) <-> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) ) )