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 ) ) )