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 )