Metamath Proof Explorer

Theorem thincpropd

Description: Two structures with the same base, hom-sets and composition operation are either both thin categories or neither. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses thincpropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
thincpropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
thincpropd.3 ⊢ φ → C ∈ V
thincpropd.4 ⊢ φ → D ∈ W
Assertion thincpropd ⊢ φ → C ∈ ThinCat ↔ D ∈ ThinCat

Proof

Step Hyp Ref Expression
1 thincpropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
2 thincpropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
3 thincpropd.3 ⊢ φ → C ∈ V
4 thincpropd.4 ⊢ φ → D ∈ W
5 1 2 3 4 catpropd ⊢ φ → C ∈ Cat ↔ D ∈ Cat
6 eqid ⊢ Base C = Base C
7 eqid ⊢ Hom ⁡ C = Hom ⁡ C
8 eqid ⊢ Hom ⁡ D = Hom ⁡ D
9 1 adantr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
10 simprl ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → x ∈ Base C
11 simprr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → y ∈ Base C
12 6 7 8 9 10 11 homfeqval ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → x Hom ⁡ C y = x Hom ⁡ D y
13 12 eleq2d ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → f ∈ x Hom ⁡ C y ↔ f ∈ x Hom ⁡ D y
14 13 mobidv ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → ∃* f f ∈ x Hom ⁡ C y ↔ ∃* f f ∈ x Hom ⁡ D y
15 14 2ralbidva ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y ↔ ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ D y
16 1 homfeqbas ⊢ φ → Base C = Base D
17 16 raleqdv ⊢ φ → ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ D y ↔ ∀ y ∈ Base D ∃* f f ∈ x Hom ⁡ D y
18 16 17 raleqbidv ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ D y ↔ ∀ x ∈ Base D ∀ y ∈ Base D ∃* f f ∈ x Hom ⁡ D y
19 15 18 bitrd ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y ↔ ∀ x ∈ Base D ∀ y ∈ Base D ∃* f f ∈ x Hom ⁡ D y
20 5 19 anbi12d ⊢ φ → C ∈ Cat ∧ ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y ↔ D ∈ Cat ∧ ∀ x ∈ Base D ∀ y ∈ Base D ∃* f f ∈ x Hom ⁡ D y
21 6 7 isthinc ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
22 eqid ⊢ Base D = Base D
23 22 8 isthinc ⊢ D ∈ ThinCat ↔ D ∈ Cat ∧ ∀ x ∈ Base D ∀ y ∈ Base D ∃* f f ∈ x Hom ⁡ D y
24 20 21 23 3bitr4g ⊢ φ → C ∈ ThinCat ↔ D ∈ ThinCat