Metamath Proof Explorer

Theorem islmd

Description: The universal property of limits of a diagram. (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses islmd.l 
|- L = ( C DiagFunc D )
islmd.a 
|- A = ( Base ` C )
islmd.n 
|- N = ( D Nat C )
islmd.b 
|- B = ( Base ` D )
islmd.h 
|- H = ( Hom ` C )
islmd.x 
|- .x. = ( comp ` C )
Assertion islmd 
|- ( X ( ( C Limit D ) ` F ) R <-> ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) )

Proof

Step Hyp Ref Expression
1 islmd.l 
 |-  L = ( C DiagFunc D )
2 islmd.a 
 |-  A = ( Base ` C )
3 islmd.n 
 |-  N = ( D Nat C )
4 islmd.b 
 |-  B = ( Base ` D )
5 islmd.h 
 |-  H = ( Hom ` C )
6 islmd.x 
 |-  .x. = ( comp ` C )
7 lmdfval2 
 |-  ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )
8 1 fveq2i 
 |-  ( oppFunc ` L ) = ( oppFunc ` ( C DiagFunc D ) )
9 8 oveq1i 
 |-  ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )
10 7 9 eqtr4i 
 |-  ( ( C Limit D ) ` F ) = ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )
11 10 breqi 
 |-  ( X ( ( C Limit D ) ` F ) R <-> X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R )
12 id 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R )
13 12 up1st2nd 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( <. ( 1st ` ( oppFunc ` L ) ) , ( 2nd ` ( oppFunc ` L ) ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R )
14 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
15 13 14 2 oppcuprcl4 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X e. A )
16 eqid 
 |-  ( oppCat ` ( D FuncCat C ) ) = ( oppCat ` ( D FuncCat C ) )
17 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
18 17 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
19 13 16 18 oppcuprcl3 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> F e. ( D Func C ) )
20 simpr 
 |-  ( ( X e. A /\ F e. ( D Func C ) ) -> F e. ( D Func C ) )
21 20 func1st2nd 
 |-  ( ( X e. A /\ F e. ( D Func C ) ) -> ( 1st ` F ) ( D Func C ) ( 2nd ` F ) )
22 21 funcrcl3 
 |-  ( ( X e. A /\ F e. ( D Func C ) ) -> C e. Cat )
23 21 funcrcl2 
 |-  ( ( X e. A /\ F e. ( D Func C ) ) -> D e. Cat )
24 1 22 23 17 diagcl 
 |-  ( ( X e. A /\ F e. ( D Func C ) ) -> L e. ( C Func ( D FuncCat C ) ) )
25 oppfval2 
 |-  ( L e. ( C Func ( D FuncCat C ) ) -> ( oppFunc ` L ) = <. ( 1st ` L ) , tpos ( 2nd ` L ) >. )
26 24 25 syl 
 |-  ( ( X e. A /\ F e. ( D Func C ) ) -> ( oppFunc ` L ) = <. ( 1st ` L ) , tpos ( 2nd ` L ) >. )
27 26 oveq1d 
 |-  ( ( X e. A /\ F e. ( D Func C ) ) -> ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) )
28 27 breqd 
 |-  ( ( X e. A /\ F e. ( D Func C ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) )
29 15 19 28 syl2anc 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) )
30 29 ibi 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R )
31 17 3 fuchom 
 |-  N = ( Hom ` ( D FuncCat C ) )
32 30 16 31 oppcuprcl5 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> R e. ( ( ( 1st ` L ) ` X ) N F ) )
33 15 32 jca 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) )
34 3 natrcl 
 |-  ( R e. ( ( ( 1st ` L ) ` X ) N F ) -> ( ( ( 1st ` L ) ` X ) e. ( D Func C ) /\ F e. ( D Func C ) ) )
35 34 simprd 
 |-  ( R e. ( ( ( 1st ` L ) ` X ) N F ) -> F e. ( D Func C ) )
36 35 28 sylan2 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) )
37 eqid 
 |-  ( comp ` ( D FuncCat C ) ) = ( comp ` ( D FuncCat C ) )
38 35 adantl 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> F e. ( D Func C ) )
39 35 24 sylan2 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> L e. ( C Func ( D FuncCat C ) ) )
40 39 func1st2nd 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
41 simpl 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> X e. A )
42 simpr 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> R e. ( ( ( 1st ` L ) ` X ) N F ) )
43 2 18 5 31 37 38 40 41 42 14 16 oppcup 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( ( x ( 2nd ` L ) X ) ` m ) ) ) )
44 35 22 sylan2 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> C e. Cat )
45 44 ad2antrr 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> C e. Cat )
46 35 23 sylan2 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> D e. Cat )
47 46 ad2antrr 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> D e. Cat )
48 simplrl 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> x e. A )
49 41 ad2antrr 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> X e. A )
50 simpr 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> m e. ( x H X ) )
51 1 2 4 5 45 47 48 49 50 diag2 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> ( ( x ( 2nd ` L ) X ) ` m ) = ( B X. { m } ) )
52 51 oveq2d 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( ( x ( 2nd ` L ) X ) ` m ) ) = ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( B X. { m } ) ) )
53 1 2 4 5 45 47 48 49 50 3 diag2cl 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> ( B X. { m } ) e. ( ( ( 1st ` L ) ` x ) N ( ( 1st ` L ) ` X ) ) )
54 42 ad2antrr 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> R e. ( ( ( 1st ` L ) ` X ) N F ) )
55 17 3 4 6 37 53 54 fucco 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( B X. { m } ) ) = ( j e. B |-> ( ( R ` j ) ( <. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. .x. ( ( 1st ` F ) ` j ) ) ( ( B X. { m } ) ` j ) ) ) )
56 45 adantr 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> C e. Cat )
57 47 adantr 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> D e. Cat )
58 48 adantr 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> x e. A )
59 eqid 
 |-  ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` x )
60 simpr 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> j e. B )
61 1 56 57 2 58 59 4 60 diag11 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) = x )
62 49 adantr 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> X e. A )
63 eqid 
 |-  ( ( 1st ` L ) ` X ) = ( ( 1st ` L ) ` X )
64 1 56 57 2 62 63 4 60 diag11 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) = X )
65 61 64 opeq12d 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> <. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. = <. x , X >. )
66 65 oveq1d 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> ( <. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. .x. ( ( 1st ` F ) ` j ) ) = ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) )
67 eqidd 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> ( R ` j ) = ( R ` j ) )
68 vex 
 |-  m e. _V
69 68 fvconst2 
 |-  ( j e. B -> ( ( B X. { m } ) ` j ) = m )
70 69 adantl 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> ( ( B X. { m } ) ` j ) = m )
71 66 67 70 oveq123d 
 |-  ( ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) /\ j e. B ) -> ( ( R ` j ) ( <. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. .x. ( ( 1st ` F ) ` j ) ) ( ( B X. { m } ) ` j ) ) = ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) )
72 71 mpteq2dva 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> ( j e. B |-> ( ( R ` j ) ( <. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. .x. ( ( 1st ` F ) ` j ) ) ( ( B X. { m } ) ` j ) ) ) = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) )
73 52 55 72 3eqtrd 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( ( x ( 2nd ` L ) X ) ` m ) ) = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) )
74 73 eqeq2d 
 |-  ( ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) /\ m e. ( x H X ) ) -> ( a = ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( ( x ( 2nd ` L ) X ) ` m ) ) <-> a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) )
75 74 reubidva 
 |-  ( ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ ( x e. A /\ a e. ( ( ( 1st ` L ) ` x ) N F ) ) ) -> ( E! m e. ( x H X ) a = ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( ( x ( 2nd ` L ) X ) ` m ) ) <-> E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) )
76 75 2ralbidva 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( ( x ( 2nd ` L ) X ) ` m ) ) <-> A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) )
77 36 43 76 3bitrd 
 |-  ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) )
78 33 77 biadanii 
 |-  ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) )
79 11 78 bitri 
 |-  ( X ( ( C Limit D ) ` F ) R <-> ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) )