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	$⊢ φ \to B = {Base}_{C}$
	isthincd.h	$⊢ φ \to H = Hom (C)$
	isthincd.t	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (x H y)$
	isthincd2.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
	isthincd2.c	$⊢ φ \to C \in V$
	isthincd2.ps	$⊢ ψ \leftrightarrow ((x \in B \land y \in B \land z \in B) \land (f \in (x H y) \land g \in (y H z)))$
	isthincd2.1	$⊢ (φ \land y \in B) \to \underset{˙}{1} \in (y H y)$
	isthincd2.2	$⊢ (φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
Assertion	isthincd2	$⊢ φ \to (C \in ThinCat \land Id (C) = (y \in B ⟼ \underset{˙}{1}))$

Proof

Step	Hyp	Ref	Expression
1		isthincd.b	$⊢ φ \to B = {Base}_{C}$
2		isthincd.h	$⊢ φ \to H = Hom (C)$
3		isthincd.t	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (x H y)$
4		isthincd2.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
5		isthincd2.c	$⊢ φ \to C \in V$
6		isthincd2.ps	$⊢ ψ \leftrightarrow ((x \in B \land y \in B \land z \in B) \land (f \in (x H y) \land g \in (y H z)))$
7		isthincd2.1	$⊢ (φ \land y \in B) \to \underset{˙}{1} \in (y H y)$
8		isthincd2.2	$⊢ (φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
9		3an4anass	$⊢ ((x \in B \land y \in B \land z \in B) \land w \in B) \leftrightarrow ((x \in B \land y \in B) \land (z \in B \land w \in B))$
10	9	anbi1i	$⊢ (((x \in B \land y \in B \land z \in B) \land w \in B) \land ((f \in (x H y) \land g \in (y H z)) \land k \in (z H w))) \leftrightarrow (((x \in B \land y \in B) \land (z \in B \land w \in B)) \land ((f \in (x H y) \land g \in (y H z)) \land k \in (z H w)))$
11	6	3anbi1i	$⊢ (ψ \land w \in B \land k \in (z H w)) \leftrightarrow (((x \in B \land y \in B \land z \in B) \land (f \in (x H y) \land g \in (y H z))) \land w \in B \land k \in (z H w))$
12		3anass	$⊢ (((x \in B \land y \in B \land z \in B) \land (f \in (x H y) \land g \in (y H z))) \land w \in B \land k \in (z H w)) \leftrightarrow (((x \in B \land y \in B \land z \in B) \land (f \in (x H y) \land g \in (y H z))) \land (w \in B \land k \in (z H w)))$
13		an4	$⊢ (((x \in B \land y \in B \land z \in B) \land (f \in (x H y) \land g \in (y H z))) \land (w \in B \land k \in (z H w))) \leftrightarrow (((x \in B \land y \in B \land z \in B) \land w \in B) \land ((f \in (x H y) \land g \in (y H z)) \land k \in (z H w)))$
14	11 12 13	3bitri	$⊢ (ψ \land w \in B \land k \in (z H w)) \leftrightarrow (((x \in B \land y \in B \land z \in B) \land w \in B) \land ((f \in (x H y) \land g \in (y H z)) \land k \in (z H w)))$
15		df-3an	$⊢ (f \in (x H y) \land g \in (y H z) \land k \in (z H w)) \leftrightarrow ((f \in (x H y) \land g \in (y H z)) \land k \in (z H w))$
16	15	anbi2i	$⊢ (((x \in B \land y \in B) \land (z \in B \land w \in B)) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \leftrightarrow (((x \in B \land y \in B) \land (z \in B \land w \in B)) \land ((f \in (x H y) \land g \in (y H z)) \land k \in (z H w)))$
17	10 14 16	3bitr4i	$⊢ (ψ \land w \in B \land k \in (z H w)) \leftrightarrow (((x \in B \land y \in B) \land (z \in B \land w \in B)) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$
18		df-3an	$⊢ ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \leftrightarrow (((x \in B \land y \in B) \land (z \in B \land w \in B)) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$
19	17 18	bitr4i	$⊢ (ψ \land w \in B \land k \in (z H w)) \leftrightarrow ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$
20		simpr1l	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to x \in B$
21		simpr1r	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to y \in B$
22		simpr31	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to f \in (x H y)$
23	21 7	syldan	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to \underset{˙}{1} \in (y H y)$
24	6	bianass	$⊢ (φ \land ψ) \leftrightarrow ((φ \land (x \in B \land y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z)))$
25	24 8	sylbir	$⊢ ((φ \land (x \in B \land y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
26	25	ralrimivva	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
27	26	ralrimivvva	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
28	27	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
29	20 21 21 22 23 28	isthincd2lem2	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f \in (x H y)$
30	3	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B \exists^{*} f f \in (x H y)$
31	30	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to \forall x \in B \forall y \in B \exists^{*} f f \in (x H y)$
32	20 21 29 22 31	isthincd2lem1	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f$
33	19 32	sylan2b	$⊢ (φ \land (ψ \land w \in B \land k \in (z H w))) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f$
34		simpr2l	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to z \in B$
35		simpr32	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g \in (y H z)$
36	21 21 34 23 35 28	isthincd2lem2	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} \in (y H z)$
37	21 34 36 35 31	isthincd2lem1	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g$
38	19 37	sylan2b	$⊢ (φ \land (ψ \land w \in B \land k \in (z H w))) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g$
39	8	3ad2antr1	$⊢ (φ \land (ψ \land w \in B \land k \in (z H w))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
40		simpr2r	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to w \in B$
41		simpr33	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k \in (z H w)$
42	21 34 40 35 41 28	isthincd2lem2	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k (⟨y, z⟩ \underset{˙}{\cdot} w) g \in (y H w)$
43	20 21 40 22 42 28	isthincd2lem2	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f \in (x H w)$
44	19 39	sylan2br	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
45	20 34 40 44 41 28	isthincd2lem2	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) \in (x H w)$
46	20 40 43 45 31	isthincd2lem1	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
47	19 46	sylan2b	$⊢ (φ \land (ψ \land w \in B \land k \in (z H w))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
48	1 2 4 5 19 7 33 38 39 47	iscatd2	$⊢ φ \to (C \in Cat \land Id (C) = (y \in B ⟼ \underset{˙}{1}))$
49	48	simpld	$⊢ φ \to C \in Cat$
50	1 2 3 49	isthincd	$⊢ φ \to C \in ThinCat$
51	48	simprd	$⊢ φ \to Id (C) = (y \in B ⟼ \underset{˙}{1})$
52	50 51	jca	$⊢ φ \to (C \in ThinCat \land Id (C) = (y \in B ⟼ \underset{˙}{1}))$

Metamath Proof Explorer

Theorem isthincd2

Proof