2arwcat

Description: The condition for a structure with at most one object and at most two morphisms being a category. "2arwcat.2" to "2arwcat.5" are also necessary conditions if X , .0. , and .1. are all sets, due to catlid , catrid , and catcocl . (Contributed by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypotheses	2arwcat.b	$⊢ φ \to \{X\} = {Base}_{C}$
	2arwcat.h	$⊢ φ \to H = Hom (C)$
	2arwcat.x	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
	2arwcat.1	$⊢ X H X = \{\underset{˙}{0}, \underset{˙}{1}\}$
	2arwcat.2	$⊢ φ \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = \underset{˙}{1}$
	2arwcat.3	$⊢ φ \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0} = \underset{˙}{0}$
	2arwcat.4	$⊢ φ \to \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = \underset{˙}{0}$
	2arwcat.5	$⊢ φ \to \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0} \in \{\underset{˙}{0}, \underset{˙}{1}\}$
Assertion	2arwcat	$⊢ φ \to (C \in Cat \land Id (C) = (y \in \{X\} ⟼ \underset{˙}{1}))$

Proof

Step	Hyp	Ref	Expression
1		2arwcat.b	$⊢ φ \to \{X\} = {Base}_{C}$
2		2arwcat.h	$⊢ φ \to H = Hom (C)$
3		2arwcat.x	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
4		2arwcat.1	$⊢ X H X = \{\underset{˙}{0}, \underset{˙}{1}\}$
5		2arwcat.2	$⊢ φ \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = \underset{˙}{1}$
6		2arwcat.3	$⊢ φ \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0} = \underset{˙}{0}$
7		2arwcat.4	$⊢ φ \to \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = \underset{˙}{0}$
8		2arwcat.5	$⊢ φ \to \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0} \in \{\underset{˙}{0}, \underset{˙}{1}\}$
9		ovex	$⊢ \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} \in V$
10	5 9	eqeltrrdi	$⊢ φ \to \underset{˙}{1} \in V$
11		prid2g	$⊢ \underset{˙}{1} \in V \to \underset{˙}{1} \in \{\underset{˙}{0}, \underset{˙}{1}\}$
12	10 11	syl	$⊢ φ \to \underset{˙}{1} \in \{\underset{˙}{0}, \underset{˙}{1}\}$
13	12 4	eleqtrrdi	$⊢ φ \to \underset{˙}{1} \in (X H X)$
14		df-ov	$⊢ X H X = H (⟨X, X⟩)$
15	2	fveq1d	$⊢ φ \to H (⟨X, X⟩) = Hom (C) (⟨X, X⟩)$
16	14 15	eqtrid	$⊢ φ \to X H X = Hom (C) (⟨X, X⟩)$
17	13 16	eleqtrd	$⊢ φ \to \underset{˙}{1} \in Hom (C) (⟨X, X⟩)$
18		elfv2ex	$⊢ \underset{˙}{1} \in Hom (C) (⟨X, X⟩) \to C \in V$
19	17 18	syl	$⊢ φ \to C \in V$
20	4	2arwcatlem1	$⊢ (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1}))) \leftrightarrow ((x \in \{X\} \land y \in \{X\}) \land (z \in \{X\} \land w \in \{X\}) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$
21	12	adantr	$⊢ (φ \land y \in \{X\}) \to \underset{˙}{1} \in \{\underset{˙}{0}, \underset{˙}{1}\}$
22		velsn	$⊢ y \in \{X\} \leftrightarrow y = X$
23		id	$⊢ y = X \to y = X$
24	23 23	oveq12d	$⊢ y = X \to y H y = X H X$
25	24 4	eqtrdi	$⊢ y = X \to y H y = \{\underset{˙}{0}, \underset{˙}{1}\}$
26	22 25	sylbi	$⊢ y \in \{X\} \to y H y = \{\underset{˙}{0}, \underset{˙}{1}\}$
27	26	adantl	$⊢ (φ \land y \in \{X\}) \to y H y = \{\underset{˙}{0}, \underset{˙}{1}\}$
28	21 27	eleqtrrd	$⊢ (φ \land y \in \{X\}) \to \underset{˙}{1} \in (y H y)$
29		simprll	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (x = X \land y = X)$
30	29	simpld	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to x = X$
31	29	simprd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to y = X$
32		simprr1	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (f = \underset{˙}{0} \lor f = \underset{˙}{1})$
33	5	adantr	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = \underset{˙}{1}$
34	6	adantr	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0} = \underset{˙}{0}$
35	30 31 31 32 33 34	2arwcatlem2	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f$
36		simprlr	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (z = X \land w = X)$
37	36	simpld	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to z = X$
38		simprr2	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (g = \underset{˙}{0} \lor g = \underset{˙}{1})$
39	7	adantr	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = \underset{˙}{0}$
40	31 31 37 38 33 39	2arwcatlem3	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g$
41	8	adantr	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0} \in \{\underset{˙}{0}, \underset{˙}{1}\}$
42	30 31 37 32 33 39 34 41 38	2arwcatlem4	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in \{\underset{˙}{0}, \underset{˙}{1}\}$
43	30 37	oveq12d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to x H z = X H X$
44	43 4	eqtrdi	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to x H z = \{\underset{˙}{0}, \underset{˙}{1}\}$
45	42 44	eleqtrrd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
46	6 7 8	2arwcatlem5	$⊢ φ \to (\underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0}) (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0} = \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) (\underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0})$
47	46	ad4antr	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to (\underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0}) (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0} = \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) (\underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0})$
48		simpr	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to k = \underset{˙}{0}$
49		simplr	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to g = \underset{˙}{0}$
50	48 49	oveq12d	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) g = \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0}$
51		simpr	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \to f = \underset{˙}{0}$
52	51	ad2antrr	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to f = \underset{˙}{0}$
53	50 52	oveq12d	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = (\underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0}) (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0}$
54	49 52	oveq12d	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to g (⟨X, X⟩ \underset{˙}{\cdot} X) f = \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0}$
55	48 54	oveq12d	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f) = \underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) (\underset{˙}{0} (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{0})$
56	47 53 55	3eqtr4d	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{0}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
57		eqidd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to X = X$
58	30 31	opeq12d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to ⟨x, y⟩ = ⟨X, X⟩$
59	58 37	oveq12d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to ⟨x, y⟩ \underset{˙}{\cdot} z = ⟨X, X⟩ \underset{˙}{\cdot} X$
60	59	oveqd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨X, X⟩ \underset{˙}{\cdot} X) f$
61	60 42	eqeltrrd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to g (⟨X, X⟩ \underset{˙}{\cdot} X) f \in \{\underset{˙}{0}, \underset{˙}{1}\}$
62		ovex	$⊢ g (⟨X, X⟩ \underset{˙}{\cdot} X) f \in V$
63	62	elpr	$⊢ g (⟨X, X⟩ \underset{˙}{\cdot} X) f \in \{\underset{˙}{0}, \underset{˙}{1}\} \leftrightarrow (g (⟨X, X⟩ \underset{˙}{\cdot} X) f = \underset{˙}{0} \lor g (⟨X, X⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1})$
64	61 63	sylib	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (g (⟨X, X⟩ \underset{˙}{\cdot} X) f = \underset{˙}{0} \lor g (⟨X, X⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1})$
65	57 57 57 64 33 34	2arwcatlem2	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f) = g (⟨X, X⟩ \underset{˙}{\cdot} X) f$
66	65	ad3antrrr	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{1}) \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f) = g (⟨X, X⟩ \underset{˙}{\cdot} X) f$
67		simpr	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{1}) \to k = \underset{˙}{1}$
68	67	oveq1d	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{1}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f) = \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
69	67	oveq1d	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{1}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) g = \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) g$
70	57 57 57 38 33 34	2arwcatlem2	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) g = g$
71	70	ad3antrrr	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{1}) \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) g = g$
72	69 71	eqtrd	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{1}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) g = g$
73	72	oveq1d	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{1}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = g (⟨X, X⟩ \underset{˙}{\cdot} X) f$
74	66 68 73	3eqtr4rd	$⊢ ((((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \land k = \underset{˙}{1}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
75		simprr3	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (k = \underset{˙}{0} \lor k = \underset{˙}{1})$
76	75	ad2antrr	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \to (k = \underset{˙}{0} \lor k = \underset{˙}{1})$
77	56 74 76	mpjaodan	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{0}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
78		simpr	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to g = \underset{˙}{1}$
79	78	oveq2d	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) g = k (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1}$
80	57 57 57 75 33 39	2arwcatlem3	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = k$
81	80	ad2antrr	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = k$
82	79 81	eqtrd	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) g = k$
83	82	oveq1d	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = k (⟨X, X⟩ \underset{˙}{\cdot} X) f$
84	78	oveq1d	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to g (⟨X, X⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) f$
85	57 57 57 32 33 34	2arwcatlem2	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) f = f$
86	85	ad2antrr	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to \underset{˙}{1} (⟨X, X⟩ \underset{˙}{\cdot} X) f = f$
87	84 86	eqtrd	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f$
88	87	oveq2d	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f) = k (⟨X, X⟩ \underset{˙}{\cdot} X) f$
89	83 88	eqtr4d	$⊢ (((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \land g = \underset{˙}{1}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
90	38	adantr	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \to (g = \underset{˙}{0} \lor g = \underset{˙}{1})$
91	77 89 90	mpjaodan	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{0}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
92	57 57 57 38 33 39 34 41 75	2arwcatlem4	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) g \in \{\underset{˙}{0}, \underset{˙}{1}\}$
93		ovex	$⊢ k (⟨X, X⟩ \underset{˙}{\cdot} X) g \in V$
94	93	elpr	$⊢ k (⟨X, X⟩ \underset{˙}{\cdot} X) g \in \{\underset{˙}{0}, \underset{˙}{1}\} \leftrightarrow (k (⟨X, X⟩ \underset{˙}{\cdot} X) g = \underset{˙}{0} \lor k (⟨X, X⟩ \underset{˙}{\cdot} X) g = \underset{˙}{1})$
95	92 94	sylib	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g = \underset{˙}{0} \lor k (⟨X, X⟩ \underset{˙}{\cdot} X) g = \underset{˙}{1})$
96	57 57 57 95 33 39	2arwcatlem3	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = k (⟨X, X⟩ \underset{˙}{\cdot} X) g$
97	96	adantr	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{1}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = k (⟨X, X⟩ \underset{˙}{\cdot} X) g$
98		simpr	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{1}) \to f = \underset{˙}{1}$
99	98	oveq2d	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{1}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1}$
100	98	oveq2d	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{1}) \to g (⟨X, X⟩ \underset{˙}{\cdot} X) f = g (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1}$
101	57 57 57 38 33 39	2arwcatlem3	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to g (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = g$
102	101	adantr	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{1}) \to g (⟨X, X⟩ \underset{˙}{\cdot} X) \underset{˙}{1} = g$
103	100 102	eqtrd	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{1}) \to g (⟨X, X⟩ \underset{˙}{\cdot} X) f = g$
104	103	oveq2d	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{1}) \to k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f) = k (⟨X, X⟩ \underset{˙}{\cdot} X) g$
105	97 99 104	3eqtr4d	$⊢ ((φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \land f = \underset{˙}{1}) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
106	91 105 32	mpjaodan	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f = k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
107	36	simprd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to w = X$
108	58 107	oveq12d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to ⟨x, y⟩ \underset{˙}{\cdot} w = ⟨X, X⟩ \underset{˙}{\cdot} X$
109	31 37	opeq12d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to ⟨y, z⟩ = ⟨X, X⟩$
110	109 107	oveq12d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to ⟨y, z⟩ \underset{˙}{\cdot} w = ⟨X, X⟩ \underset{˙}{\cdot} X$
111	110	oveqd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to k (⟨y, z⟩ \underset{˙}{\cdot} w) g = k (⟨X, X⟩ \underset{˙}{\cdot} X) g$
112		eqidd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to f = f$
113	108 111 112	oveq123d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = (k (⟨X, X⟩ \underset{˙}{\cdot} X) g) (⟨X, X⟩ \underset{˙}{\cdot} X) f$
114	30 37	opeq12d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to ⟨x, z⟩ = ⟨X, X⟩$
115	114 107	oveq12d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to ⟨x, z⟩ \underset{˙}{\cdot} w = ⟨X, X⟩ \underset{˙}{\cdot} X$
116		eqidd	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to k = k$
117	115 116 60	oveq123d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) = k (⟨X, X⟩ \underset{˙}{\cdot} X) (g (⟨X, X⟩ \underset{˙}{\cdot} X) f)$
118	106 113 117	3eqtr4d	$⊢ (φ \land (((x = X \land y = X) \land (z = X \land w = X)) \land ((f = \underset{˙}{0} \lor f = \underset{˙}{1}) \land (g = \underset{˙}{0} \lor g = \underset{˙}{1}) \land (k = \underset{˙}{0} \lor k = \underset{˙}{1})))) \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)$
119	1 2 3 19 20 28 35 40 45 118	iscatd2	$⊢ φ \to (C \in Cat \land Id (C) = (y \in \{X\} ⟼ \underset{˙}{1}))$

Metamath Proof Explorer

Theorem 2arwcat

Proof