Metamath Proof Explorer

Theorem funcf2lem2

Description: A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 25-Sep-2025)

Ref Expression
Hypothesis funcf2lem2.b 
|- B = ( E ` C )
Assertion funcf2lem2 
|- ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 funcf2lem2.b 
 |-  B = ( E ` C )
2 funcf2lem 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G e. _V /\ G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )
3 3simpc 
 |-  ( ( G e. _V /\ G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) -> ( G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )
4 2 3 sylbi 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) -> ( G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )
5 fnov 
 |-  ( G Fn ( B X. B ) <-> G = ( x e. B , y e. B |-> ( x G y ) ) )
6 5 biimpi 
 |-  ( G Fn ( B X. B ) -> G = ( x e. B , y e. B |-> ( x G y ) ) )
7 1 fvexi 
 |-  B e. _V
8 7 7 mpoex 
 |-  ( x e. B , y e. B |-> ( x G y ) ) e. _V
9 6 8 eqeltrdi 
 |-  ( G Fn ( B X. B ) -> G e. _V )
10 9 adantr 
 |-  ( ( G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) -> G e. _V )
11 simpl 
 |-  ( ( G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) -> G Fn ( B X. B ) )
12 simpr 
 |-  ( ( G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) -> A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
13 10 11 12 2 syl3anbrc 
 |-  ( ( G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) -> G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
14 4 13 impbii 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )