Metamath Proof Explorer

Theorem ssceq

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

Ref Expression
Assertion ssceq ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → 𝐴 ⊆cat 𝐵 )
2 eqidd ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → dom dom 𝐴 = dom dom 𝐴 )
3 1 2 sscfn1 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → 𝐴 Fn ( dom dom 𝐴 × dom dom 𝐴 ) )
4 simpr ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → 𝐵 ⊆cat 𝐴 )
5 eqidd ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → dom dom 𝐵 = dom dom 𝐵 )
6 4 5 sscfn1 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → 𝐵 Fn ( dom dom 𝐵 × dom dom 𝐵 ) )
7 3 6 1 ssc1 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → dom dom 𝐴 ⊆ dom dom 𝐵 )
8 6 3 4 ssc1 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → dom dom 𝐵 ⊆ dom dom 𝐴 )
9 7 8 eqssd ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → dom dom 𝐴 = dom dom 𝐵 )
10 9 sqxpeqd ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → ( dom dom 𝐴 × dom dom 𝐴 ) = ( dom dom 𝐵 × dom dom 𝐵 ) )
11 3 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝐴 Fn ( dom dom 𝐴 × dom dom 𝐴 ) )
12 1 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝐴 ⊆cat 𝐵 )
13 simprl ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝑥 ∈ dom dom 𝐴 )
14 simprr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝑦 ∈ dom dom 𝐴 )
15 11 12 13 14 ssc2 ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → ( 𝑥 𝐴 𝑦 ) ⊆ ( 𝑥 𝐵 𝑦 ) )
16 6 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝐵 Fn ( dom dom 𝐵 × dom dom 𝐵 ) )
17 4 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝐵 ⊆cat 𝐴 )
18 7 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → dom dom 𝐴 ⊆ dom dom 𝐵 )
19 18 13 sseldd ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝑥 ∈ dom dom 𝐵 )
20 18 14 sseldd ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝑦 ∈ dom dom 𝐵 )
21 16 17 19 20 ssc2 ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → ( 𝑥 𝐵 𝑦 ) ⊆ ( 𝑥 𝐴 𝑦 ) )
22 15 21 eqssd ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → ( 𝑥 𝐴 𝑦 ) = ( 𝑥 𝐵 𝑦 ) )
23 22 ralrimivva ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → ∀ 𝑥 ∈ dom dom 𝐴 ∀ 𝑦 ∈ dom dom 𝐴 ( 𝑥 𝐴 𝑦 ) = ( 𝑥 𝐵 𝑦 ) )
24 eqfnov ⊢ ( ( 𝐴 Fn ( dom dom 𝐴 × dom dom 𝐴 ) ∧ 𝐵 Fn ( dom dom 𝐵 × dom dom 𝐵 ) ) → ( 𝐴 = 𝐵 ↔ ( ( dom dom 𝐴 × dom dom 𝐴 ) = ( dom dom 𝐵 × dom dom 𝐵 ) ∧ ∀ 𝑥 ∈ dom dom 𝐴 ∀ 𝑦 ∈ dom dom 𝐴 ( 𝑥 𝐴 𝑦 ) = ( 𝑥 𝐵 𝑦 ) ) ) )
25 3 6 24 syl2anc ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → ( 𝐴 = 𝐵 ↔ ( ( dom dom 𝐴 × dom dom 𝐴 ) = ( dom dom 𝐵 × dom dom 𝐵 ) ∧ ∀ 𝑥 ∈ dom dom 𝐴 ∀ 𝑦 ∈ dom dom 𝐴 ( 𝑥 𝐴 𝑦 ) = ( 𝑥 𝐵 𝑦 ) ) ) )
26 10 23 25 mpbir2and ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐴 ) → 𝐴 = 𝐵 )