Metamath Proof Explorer

Theorem ssctr

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

Ref Expression
Assertion ssctr 
|- ( ( A C_cat B /\ B C_cat C ) -> A C_cat C )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A C_cat B /\ B C_cat C ) -> A C_cat B )
2 eqidd 
 |-  ( ( A C_cat B /\ B C_cat C ) -> dom dom A = dom dom A )
3 1 2 sscfn1 
 |-  ( ( A C_cat B /\ B C_cat C ) -> A Fn ( dom dom A X. dom dom A ) )
4 eqidd 
 |-  ( ( A C_cat B /\ B C_cat C ) -> dom dom B = dom dom B )
5 1 4 sscfn2 
 |-  ( ( A C_cat B /\ B C_cat C ) -> B Fn ( dom dom B X. dom dom B ) )
6 3 5 1 ssc1 
 |-  ( ( A C_cat B /\ B C_cat C ) -> dom dom A C_ dom dom B )
7 simpr 
 |-  ( ( A C_cat B /\ B C_cat C ) -> B C_cat C )
8 eqidd 
 |-  ( ( A C_cat B /\ B C_cat C ) -> dom dom C = dom dom C )
9 7 8 sscfn2 
 |-  ( ( A C_cat B /\ B C_cat C ) -> C Fn ( dom dom C X. dom dom C ) )
10 5 9 7 ssc1 
 |-  ( ( A C_cat B /\ B C_cat C ) -> dom dom B C_ dom dom C )
11 6 10 sstrd 
 |-  ( ( A C_cat B /\ B C_cat C ) -> dom dom A C_ dom dom C )
12 3 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> A Fn ( dom dom A X. dom dom A ) )
13 1 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> A C_cat B )
14 simprl 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> x e. dom dom A )
15 simprr 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> y e. dom dom A )
16 12 13 14 15 ssc2 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> ( x A y ) C_ ( x B y ) )
17 5 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> B Fn ( dom dom B X. dom dom B ) )
18 7 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> B C_cat C )
19 6 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> dom dom A C_ dom dom B )
20 19 14 sseldd 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> x e. dom dom B )
21 19 15 sseldd 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> y e. dom dom B )
22 17 18 20 21 ssc2 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> ( x B y ) C_ ( x C y ) )
23 16 22 sstrd 
 |-  ( ( ( A C_cat B /\ B C_cat C ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> ( x A y ) C_ ( x C y ) )
24 23 ralrimivva 
 |-  ( ( A C_cat B /\ B C_cat C ) -> A. x e. dom dom A A. y e. dom dom A ( x A y ) C_ ( x C y ) )
25 sscrel 
 |-  Rel C_cat
26 25 brrelex2i 
 |-  ( B C_cat C -> C e. _V )
27 26 adantl 
 |-  ( ( A C_cat B /\ B C_cat C ) -> C e. _V )
28 dmexg 
 |-  ( C e. _V -> dom C e. _V )
29 dmexg 
 |-  ( dom C e. _V -> dom dom C e. _V )
30 27 28 29 3syl 
 |-  ( ( A C_cat B /\ B C_cat C ) -> dom dom C e. _V )
31 3 9 30 isssc 
 |-  ( ( A C_cat B /\ B C_cat C ) -> ( A C_cat C <-> ( dom dom A C_ dom dom C /\ A. x e. dom dom A A. y e. dom dom A ( x A y ) C_ ( x C y ) ) ) )
32 11 24 31 mpbir2and 
 |-  ( ( A C_cat B /\ B C_cat C ) -> A C_cat C )