This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isthinc

Description: The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthinc.b 
|- B = ( Base ` C )
isthinc.h 
|- H = ( Hom ` C )
Assertion isthinc 
|- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) )

Proof

Step Hyp Ref Expression
1 isthinc.b 
 |-  B = ( Base ` C )
2 isthinc.h 
 |-  H = ( Hom ` C )
3 fvexd 
 |-  ( c = C -> ( Base ` c ) e. _V )
4 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
5 4 1 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
6 fvexd 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) e. _V )
7 fveq2 
 |-  ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
8 7 2 eqtr4di 
 |-  ( c = C -> ( Hom ` c ) = H )
9 8 adantr 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = H )
10 raleq 
 |-  ( b = B -> ( A. y e. b E* f f e. ( x h y ) <-> A. y e. B E* f f e. ( x h y ) ) )
11 10 raleqbi1dv 
 |-  ( b = B -> ( A. x e. b A. y e. b E* f f e. ( x h y ) <-> A. x e. B A. y e. B E* f f e. ( x h y ) ) )
12 11 ad2antlr 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( A. x e. b A. y e. b E* f f e. ( x h y ) <-> A. x e. B A. y e. B E* f f e. ( x h y ) ) )
13 oveq 
 |-  ( h = H -> ( x h y ) = ( x H y ) )
14 13 eleq2d 
 |-  ( h = H -> ( f e. ( x h y ) <-> f e. ( x H y ) ) )
15 14 mobidv 
 |-  ( h = H -> ( E* f f e. ( x h y ) <-> E* f f e. ( x H y ) ) )
16 15 2ralbidv 
 |-  ( h = H -> ( A. x e. B A. y e. B E* f f e. ( x h y ) <-> A. x e. B A. y e. B E* f f e. ( x H y ) ) )
17 16 adantl 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( A. x e. B A. y e. B E* f f e. ( x h y ) <-> A. x e. B A. y e. B E* f f e. ( x H y ) ) )
18 12 17 bitrd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( A. x e. b A. y e. b E* f f e. ( x h y ) <-> A. x e. B A. y e. B E* f f e. ( x H y ) ) )
19 6 9 18 sbcied2 
 |-  ( ( c = C /\ b = B ) -> ( [. ( Hom ` c ) / h ]. A. x e. b A. y e. b E* f f e. ( x h y ) <-> A. x e. B A. y e. B E* f f e. ( x H y ) ) )
20 3 5 19 sbcied2 
 |-  ( c = C -> ( [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. A. x e. b A. y e. b E* f f e. ( x h y ) <-> A. x e. B A. y e. B E* f f e. ( x H y ) ) )
21 df-thinc 
 |-  ThinCat = { c e. Cat | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. A. x e. b A. y e. b E* f f e. ( x h y ) }
22 20 21 elrab2 
 |-  ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) )