Metamath Proof Explorer

Theorem brssc

Description: The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion brssc 
|- ( H C_cat J <-> E. t ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) )

Proof

Step Hyp Ref Expression
1 sscrel 
 |-  Rel C_cat
2 1 brrelex12i 
 |-  ( H C_cat J -> ( H e. _V /\ J e. _V ) )
3 vex 
 |-  t e. _V
4 3 3 xpex 
 |-  ( t X. t ) e. _V
5 fnex 
 |-  ( ( J Fn ( t X. t ) /\ ( t X. t ) e. _V ) -> J e. _V )
6 4 5 mpan2 
 |-  ( J Fn ( t X. t ) -> J e. _V )
7 elex 
 |-  ( H e. X_ x e. ( s X. s ) ~P ( J ` x ) -> H e. _V )
8 7 rexlimivw 
 |-  ( E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) -> H e. _V )
9 6 8 anim12ci 
 |-  ( ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) -> ( H e. _V /\ J e. _V ) )
10 9 exlimiv 
 |-  ( E. t ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) -> ( H e. _V /\ J e. _V ) )
11 simpr 
 |-  ( ( h = H /\ j = J ) -> j = J )
12 11 fneq1d 
 |-  ( ( h = H /\ j = J ) -> ( j Fn ( t X. t ) <-> J Fn ( t X. t ) ) )
13 simpl 
 |-  ( ( h = H /\ j = J ) -> h = H )
14 11 fveq1d 
 |-  ( ( h = H /\ j = J ) -> ( j ` x ) = ( J ` x ) )
15 14 pweqd 
 |-  ( ( h = H /\ j = J ) -> ~P ( j ` x ) = ~P ( J ` x ) )
16 15 ixpeq2dv 
 |-  ( ( h = H /\ j = J ) -> X_ x e. ( s X. s ) ~P ( j ` x ) = X_ x e. ( s X. s ) ~P ( J ` x ) )
17 13 16 eleq12d 
 |-  ( ( h = H /\ j = J ) -> ( h e. X_ x e. ( s X. s ) ~P ( j ` x ) <-> H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) )
18 17 rexbidv 
 |-  ( ( h = H /\ j = J ) -> ( E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) <-> E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) )
19 12 18 anbi12d 
 |-  ( ( h = H /\ j = J ) -> ( ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) ) <-> ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) ) )
20 19 exbidv 
 |-  ( ( h = H /\ j = J ) -> ( E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) ) <-> E. t ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) ) )
21 df-ssc 
 |-  C_cat = { <. h , j >. | E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) ) }
22 20 21 brabga 
 |-  ( ( H e. _V /\ J e. _V ) -> ( H C_cat J <-> E. t ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) ) )
23 2 10 22 pm5.21nii 
 |-  ( H C_cat J <-> E. t ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) )