Theorem isthinc

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

	Ref	Expression
Hypotheses	isthinc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	isthinc.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	isthinc	⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isthinc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isthinc.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		fvexd	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) ∈ V )
4		fveq2	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
5	4 1	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
6		fvexd	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) ∈ V )
7		fveq2	⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
8	7 2	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = 𝐻 )
9	8	adantr	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = 𝐻 )
10		raleq	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ) )
11	10	raleqbi1dv	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ) )
12	11	ad2antlr	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ) )
13		oveq	⊢ ( ℎ = 𝐻 → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
14	13	eleq2d	⊢ ( ℎ = 𝐻 → ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
15	14	mobidv	⊢ ( ℎ = 𝐻 → ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
16	15	2ralbidv	⊢ ( ℎ = 𝐻 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
17	16	adantl	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
18	12 17	bitrd	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
19	6 9 18	sbcied2	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( [ ( Hom ‘ 𝑐 ) / ℎ ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
20	3 5 19	sbcied2	⊢ ( 𝑐 = 𝐶 → ( [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
21		df-thinc	⊢ ThinCat = { 𝑐 ∈ Cat ∣ [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) }
22	20 21	elrab2	⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )