Metamath Proof Explorer


Theorem ssceq

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

Ref Expression
Assertion ssceq A cat B B cat A A = B

Proof

Step Hyp Ref Expression
1 simpl A cat B B cat A A cat B
2 eqidd A cat B B cat A dom dom A = dom dom A
3 1 2 sscfn1 A cat B B cat A A Fn dom dom A × dom dom A
4 simpr A cat B B cat A B cat A
5 eqidd A cat B B cat A dom dom B = dom dom B
6 4 5 sscfn1 A cat B B cat A B Fn dom dom B × dom dom B
7 3 6 1 ssc1 A cat B B cat A dom dom A dom dom B
8 6 3 4 ssc1 A cat B B cat A dom dom B dom dom A
9 7 8 eqssd A cat B B cat A dom dom A = dom dom B
10 9 sqxpeqd A cat B B cat A dom dom A × dom dom A = dom dom B × dom dom B
11 3 adantr A cat B B cat A x dom dom A y dom dom A A Fn dom dom A × dom dom A
12 1 adantr A cat B B cat A x dom dom A y dom dom A A cat B
13 simprl A cat B B cat A x dom dom A y dom dom A x dom dom A
14 simprr A cat B B cat A x dom dom A y dom dom A y dom dom A
15 11 12 13 14 ssc2 A cat B B cat A x dom dom A y dom dom A x A y x B y
16 6 adantr A cat B B cat A x dom dom A y dom dom A B Fn dom dom B × dom dom B
17 4 adantr A cat B B cat A x dom dom A y dom dom A B cat A
18 7 adantr A cat B B cat A x dom dom A y dom dom A dom dom A dom dom B
19 18 13 sseldd A cat B B cat A x dom dom A y dom dom A x dom dom B
20 18 14 sseldd A cat B B cat A x dom dom A y dom dom A y dom dom B
21 16 17 19 20 ssc2 A cat B B cat A x dom dom A y dom dom A x B y x A y
22 15 21 eqssd A cat B B cat A x dom dom A y dom dom A x A y = x B y
23 22 ralrimivva A cat B B cat A x dom dom A y dom dom A x A y = x B y
24 eqfnov A Fn dom dom A × dom dom A B Fn dom dom B × dom dom B A = B dom dom A × dom dom A = dom dom B × dom dom B x dom dom A y dom dom A x A y = x B y
25 3 6 24 syl2anc A cat B B cat A A = B dom dom A × dom dom A = dom dom B × dom dom B x dom dom A y dom dom A x A y = x B y
26 10 23 25 mpbir2and A cat B B cat A A = B