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 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
thincpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
thincpropd.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
thincpropd.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion thincpropd ( 𝜑 → ( 𝐶 ∈ ThinCat ↔ 𝐷 ∈ ThinCat ) )

Proof

Step Hyp Ref Expression
1 thincpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2 thincpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3 thincpropd.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 thincpropd.4 ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5 1 2 3 4 catpropd ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
10 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
12 6 7 8 9 10 11 homfeqval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
13 12 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
14 13 mobidv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
15 14 2ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
16 1 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
17 16 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
18 16 17 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
19 15 18 bitrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
20 5 19 anbi12d ⊢ ( 𝜑 → ( ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ↔ ( 𝐷 ∈ Cat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) ) )
21 6 7 isthinc ⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
22 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
23 22 8 isthinc ⊢ ( 𝐷 ∈ ThinCat ↔ ( 𝐷 ∈ Cat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
24 20 21 23 3bitr4g ⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ↔ 𝐷 ∈ ThinCat ) )