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

Metamath Proof Explorer

Theorem isthincd2

Description: The predicate " C is a thin category" without knowing C is a category (deduction form). The identity arrow operator is also provided as a byproduct. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
isthincd.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
isthincd.t ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
isthincd2.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
isthincd2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
isthincd2.ps ⊢ ( 𝜓 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) )
isthincd2.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 1 ∈ ( 𝑦 𝐻 𝑦 ) )
isthincd2.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
Assertion isthincd2 ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 1 ) ) )

Proof

Step Hyp Ref Expression
1 isthincd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2 isthincd.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3 isthincd.t ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
4 isthincd2.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
5 isthincd2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
6 isthincd2.ps ⊢ ( 𝜓 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) )
7 isthincd2.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 1 ∈ ( 𝑦 𝐻 𝑦 ) )
8 isthincd2.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
9 3an4anass ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) )
10 9 anbi1i ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
11 6 3anbi1i ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) )
12 3anass ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
13 an4 ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
14 11 12 13 3bitri ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
15 df-3an ⊢ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) )
16 15 anbi2i ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
17 10 14 16 3bitr4i ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
18 df-3an ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
19 17 18 bitr4i ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
20 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑥 ∈ 𝐵 )
21 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑦 ∈ 𝐵 )
22 simpr31 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
23 21 7 syldan ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 1 ∈ ( 𝑦 𝐻 𝑦 ) )
24 6 bianass ⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) )
25 24 8 sylbir ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
26 25 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
27 26 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
29 20 21 21 22 23 28 isthincd2lem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑦 ) )
30 3 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
32 20 21 29 22 31 isthincd2lem1 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
33 19 32 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
34 simpr2l ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑧 ∈ 𝐵 )
35 simpr32 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) )
36 21 21 34 23 35 28 isthincd2lem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) ∈ ( 𝑦 𝐻 𝑧 ) )
37 21 34 36 35 31 isthincd2lem1 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
38 19 37 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
39 8 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
40 simpr2r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑤 ∈ 𝐵 )
41 simpr33 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) )
42 21 34 40 35 41 28 isthincd2lem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ∈ ( 𝑦 𝐻 𝑤 ) )
43 20 21 40 22 42 28 isthincd2lem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑤 ) )
44 19 39 sylan2br ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
45 20 34 40 44 41 28 isthincd2lem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ∈ ( 𝑥 𝐻 𝑤 ) )
46 20 40 43 45 31 isthincd2lem1 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
47 19 46 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑤 ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
48 1 2 4 5 19 7 33 38 39 47 iscatd2 ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 1 ) ) )
49 48 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
50 1 2 3 49 isthincd ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
51 48 simprd ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 1 ) )
52 50 51 jca ⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 1 ) ) )