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

Metamath Proof Explorer

Theorem ssceq

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

Ref Expression
Assertion ssceq 
|- ( ( A C_cat B /\ B C_cat A ) -> A = B )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A C_cat B /\ B C_cat A ) -> A C_cat B )
2 eqidd 
 |-  ( ( A C_cat B /\ B C_cat A ) -> dom dom A = dom dom A )
3 1 2 sscfn1 
 |-  ( ( A C_cat B /\ B C_cat A ) -> A Fn ( dom dom A X. dom dom A ) )
4 simpr 
 |-  ( ( A C_cat B /\ B C_cat A ) -> B C_cat A )
5 eqidd 
 |-  ( ( A C_cat B /\ B C_cat A ) -> dom dom B = dom dom B )
6 4 5 sscfn1 
 |-  ( ( A C_cat B /\ B C_cat A ) -> B Fn ( dom dom B X. dom dom B ) )
7 3 6 1 ssc1 
 |-  ( ( A C_cat B /\ B C_cat A ) -> dom dom A C_ dom dom B )
8 6 3 4 ssc1 
 |-  ( ( A C_cat B /\ B C_cat A ) -> dom dom B C_ dom dom A )
9 7 8 eqssd 
 |-  ( ( A C_cat B /\ B C_cat A ) -> dom dom A = dom dom B )
10 9 sqxpeqd 
 |-  ( ( A C_cat B /\ B C_cat A ) -> ( dom dom A X. dom dom A ) = ( dom dom B X. dom dom B ) )
11 3 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> A Fn ( dom dom A X. dom dom A ) )
12 1 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> A C_cat B )
13 simprl 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> x e. dom dom A )
14 simprr 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> y e. dom dom A )
15 11 12 13 14 ssc2 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> ( x A y ) C_ ( x B y ) )
16 6 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> B Fn ( dom dom B X. dom dom B ) )
17 4 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> B C_cat A )
18 7 adantr 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> dom dom A C_ dom dom B )
19 18 13 sseldd 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> x e. dom dom B )
20 18 14 sseldd 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> y e. dom dom B )
21 16 17 19 20 ssc2 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> ( x B y ) C_ ( x A y ) )
22 15 21 eqssd 
 |-  ( ( ( A C_cat B /\ B C_cat A ) /\ ( x e. dom dom A /\ y e. dom dom A ) ) -> ( x A y ) = ( x B y ) )
23 22 ralrimivva 
 |-  ( ( A C_cat B /\ B C_cat A ) -> A. x e. dom dom A A. y e. dom dom A ( x A y ) = ( x B y ) )
24 eqfnov 
 |-  ( ( A Fn ( dom dom A X. dom dom A ) /\ B Fn ( dom dom B X. dom dom B ) ) -> ( A = B <-> ( ( dom dom A X. dom dom A ) = ( dom dom B X. dom dom B ) /\ A. x e. dom dom A A. y e. dom dom A ( x A y ) = ( x B y ) ) ) )
25 3 6 24 syl2anc 
 |-  ( ( A C_cat B /\ B C_cat A ) -> ( A = B <-> ( ( dom dom A X. dom dom A ) = ( dom dom B X. dom dom B ) /\ A. x e. dom dom A A. y e. dom dom A ( x A y ) = ( x B y ) ) ) )
26 10 23 25 mpbir2and 
 |-  ( ( A C_cat B /\ B C_cat A ) -> A = B )