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

Metamath Proof Explorer

Theorem isthincd

Description: The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
isthincd.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
isthincd.t ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
isthincd.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion isthincd ( 𝜑 → 𝐶 ∈ ThinCat )

Proof

Step Hyp Ref Expression
1 isthincd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2 isthincd.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3 isthincd.t ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
4 isthincd.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 3 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
6 2 oveqd ⊢ ( 𝜑 → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
7 6 eleq2d ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
8 7 mobidv ⊢ ( 𝜑 → ( ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
9 1 8 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
10 1 9 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
11 5 10 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
14 12 13 isthinc ⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
15 4 11 14 sylanbrc ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )