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

Metamath Proof Explorer

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 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )