iscatd2

Description: Version of iscatd with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	iscatd2.b	$⊢ φ \to B = {Base}_{C}$
	iscatd2.h	$⊢ φ \to H = Hom (C)$
	iscatd2.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
	iscatd2.c	$⊢ φ \to C \in V$
	iscatd2.ps	$⊢ ψ \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)))$
	iscatd2.1	$⊢ (φ \land y \in B) \to \underset{˙}{1} \in (y H y)$
	iscatd2.2	$⊢ (φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f$
	iscatd2.3	$⊢ (φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g$
	iscatd2.4	$⊢ (φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
	iscatd2.5	$⊢ (φ \land ψ) \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)$
Assertion	iscatd2	$⊢ φ \to (C \in Cat \land Id (C) = (y \in B ⟼ \underset{˙}{1}))$

Proof

Step	Hyp	Ref	Expression
1		iscatd2.b	$⊢ φ \to B = {Base}_{C}$
2		iscatd2.h	$⊢ φ \to H = Hom (C)$
3		iscatd2.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
4		iscatd2.c	$⊢ φ \to C \in V$
5		iscatd2.ps	$⊢ ψ \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)))$
6		iscatd2.1	$⊢ (φ \land y \in B) \to \underset{˙}{1} \in (y H y)$
7		iscatd2.2	$⊢ (φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f$
8		iscatd2.3	$⊢ (φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g$
9		iscatd2.4	$⊢ (φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
10		iscatd2.5	$⊢ (φ \land ψ) \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)$
11	6	ne0d	$⊢ (φ \land y \in B) \to y H y \neq \emptyset$
12	11	3ad2antr1	$⊢ (φ \land (y \in B \land a \in B \land r \in (a H y))) \to y H y \neq \emptyset$
13		n0	$⊢ y H y \neq \emptyset \leftrightarrow \exists g g \in (y H y)$
14	12 13	sylib	$⊢ (φ \land (y \in B \land a \in B \land r \in (a H y))) \to \exists g g \in (y H y)$
15		n0	$⊢ y H y \neq \emptyset \leftrightarrow \exists k k \in (y H y)$
16	12 15	sylib	$⊢ (φ \land (y \in B \land a \in B \land r \in (a H y))) \to \exists k k \in (y H y)$
17		exdistrv	$⊢ \exists g \exists k (g \in (y H y) \land k \in (y H y)) \leftrightarrow (\exists g g \in (y H y) \land \exists k k \in (y H y))$
18		simpll	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to φ$
19		simplr2	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to a \in B$
20		simplr1	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to y \in B$
21	19 20	jca	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to (a \in B \land y \in B)$
22		simplr3	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to r \in (a H y)$
23		simprl	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to g \in (y H y)$
24		simprr	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to k \in (y H y)$
25	22 23 24	3jca	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to (r \in (a H y) \land g \in (y H y) \land k \in (y H y))$
26		simplll	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to x = a$
27	26	eleq1d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (x \in B \leftrightarrow a \in B)$
28	27	anbi1d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to ((x \in B \land y \in B) \leftrightarrow (a \in B \land y \in B))$
29		simpllr	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to z = y$
30	29	eleq1d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (z \in B \leftrightarrow y \in B)$
31		simplr	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to w = y$
32	31	eleq1d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (w \in B \leftrightarrow y \in B)$
33	30 32	anbi12d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to ((z \in B \land w \in B) \leftrightarrow (y \in B \land y \in B))$
34		anidm	$⊢ (y \in B \land y \in B) \leftrightarrow y \in B$
35	33 34	bitrdi	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to ((z \in B \land w \in B) \leftrightarrow y \in B)$
36		simpr	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to f = r$
37	26	oveq1d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to x H y = a H y$
38	36 37	eleq12d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (f \in (x H y) \leftrightarrow r \in (a H y))$
39	29	oveq2d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to y H z = y H y$
40	39	eleq2d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (g \in (y H z) \leftrightarrow g \in (y H y))$
41	29 31	oveq12d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to z H w = y H y$
42	41	eleq2d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (k \in (z H w) \leftrightarrow k \in (y H y))$
43	38 40 42	3anbi123d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to ((f \in (x H y) \land g \in (y H z) \land k \in (z H w)) \leftrightarrow (r \in (a H y) \land g \in (y H y) \land k \in (y H y)))$
44	28 35 43	3anbi123d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (((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 ((a \in B \land y \in B) \land y \in B \land (r \in (a H y) \land g \in (y H y) \land k \in (y H y))))$
45	5 44	syl5bb	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (ψ \leftrightarrow ((a \in B \land y \in B) \land y \in B \land (r \in (a H y) \land g \in (y H y) \land k \in (y H y))))$
46	45	anbi2d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to ((φ \land ψ) \leftrightarrow (φ \land ((a \in B \land y \in B) \land y \in B \land (r \in (a H y) \land g \in (y H y) \land k \in (y H y)))))$
47	26	opeq1d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to ⟨x, y⟩ = ⟨a, y⟩$
48	47	oveq1d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to ⟨x, y⟩ \underset{˙}{\cdot} y = ⟨a, y⟩ \underset{˙}{\cdot} y$
49		eqidd	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to \underset{˙}{1} = \underset{˙}{1}$
50	48 49 36	oveq123d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r$
51	50 36	eqeq12d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (\underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f \leftrightarrow \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r)$
52	46 51	imbi12d	$⊢ (((x = a \land z = y) \land w = y) \land f = r) \to (((φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f) \leftrightarrow ((φ \land ((a \in B \land y \in B) \land y \in B \land (r \in (a H y) \land g \in (y H y) \land k \in (y H y)))) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r))$
53	52	sbiedvw	$⊢ ((x = a \land z = y) \land w = y) \to ([r/ f] ((φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f) \leftrightarrow ((φ \land ((a \in B \land y \in B) \land y \in B \land (r \in (a H y) \land g \in (y H y) \land k \in (y H y)))) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r))$
54	53	sbiedvw	$⊢ (x = a \land z = y) \to ([y/ w] [r/ f] ((φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f) \leftrightarrow ((φ \land ((a \in B \land y \in B) \land y \in B \land (r \in (a H y) \land g \in (y H y) \land k \in (y H y)))) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r))$
55	54	sbiedvw	$⊢ x = a \to ([y/ z] [y/ w] [r/ f] ((φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f) \leftrightarrow ((φ \land ((a \in B \land y \in B) \land y \in B \land (r \in (a H y) \land g \in (y H y) \land k \in (y H y)))) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r))$
56	7	sbt	$⊢ [r/ f] ((φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f)$
57	56	sbt	$⊢ [y/ w] [r/ f] ((φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f)$
58	57	sbt	$⊢ [y/ z] [y/ w] [r/ f] ((φ \land ψ) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f)$
59	55 58	chvarvv	$⊢ (φ \land ((a \in B \land y \in B) \land y \in B \land (r \in (a H y) \land g \in (y H y) \land k \in (y H y)))) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r$
60	18 21 20 25 59	syl13anc	$⊢ ((φ \land (y \in B \land a \in B \land r \in (a H y))) \land (g \in (y H y) \land k \in (y H y))) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r$
61	60	ex	$⊢ (φ \land (y \in B \land a \in B \land r \in (a H y))) \to ((g \in (y H y) \land k \in (y H y)) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r)$
62	61	exlimdvv	$⊢ (φ \land (y \in B \land a \in B \land r \in (a H y))) \to (\exists g \exists k (g \in (y H y) \land k \in (y H y)) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r)$
63	17 62	syl5bir	$⊢ (φ \land (y \in B \land a \in B \land r \in (a H y))) \to ((\exists g g \in (y H y) \land \exists k k \in (y H y)) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r)$
64	14 16 63	mp2and	$⊢ (φ \land (y \in B \land a \in B \land r \in (a H y))) \to \underset{˙}{1} (⟨a, y⟩ \underset{˙}{\cdot} y) r = r$
65	11	3ad2antr1	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to y H y \neq \emptyset$
66		n0	$⊢ y H y \neq \emptyset \leftrightarrow \exists f f \in (y H y)$
67	65 66	sylib	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to \exists f f \in (y H y)$
68		id	$⊢ y = a \to y = a$
69	68 68	oveq12d	$⊢ y = a \to y H y = a H a$
70	69	neeq1d	$⊢ y = a \to (y H y \neq \emptyset \leftrightarrow a H a \neq \emptyset)$
71	11	ralrimiva	$⊢ φ \to \forall y \in B y H y \neq \emptyset$
72	71	adantr	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to \forall y \in B y H y \neq \emptyset$
73		simpr2	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to a \in B$
74	70 72 73	rspcdva	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to a H a \neq \emptyset$
75		n0	$⊢ a H a \neq \emptyset \leftrightarrow \exists k k \in (a H a)$
76	74 75	sylib	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to \exists k k \in (a H a)$
77		exdistrv	$⊢ \exists f \exists k (f \in (y H y) \land k \in (a H a)) \leftrightarrow (\exists f f \in (y H y) \land \exists k k \in (a H a))$
78		simpll	$⊢ ((φ \land (y \in B \land a \in B \land r \in (y H a))) \land (f \in (y H y) \land k \in (a H a))) \to φ$
79		simplr1	$⊢ ((φ \land (y \in B \land a \in B \land r \in (y H a))) \land (f \in (y H y) \land k \in (a H a))) \to y \in B$
80		simplr2	$⊢ ((φ \land (y \in B \land a \in B \land r \in (y H a))) \land (f \in (y H y) \land k \in (a H a))) \to a \in B$
81		simprl	$⊢ ((φ \land (y \in B \land a \in B \land r \in (y H a))) \land (f \in (y H y) \land k \in (a H a))) \to f \in (y H y)$
82		simplr3	$⊢ ((φ \land (y \in B \land a \in B \land r \in (y H a))) \land (f \in (y H y) \land k \in (a H a))) \to r \in (y H a)$
83		simprr	$⊢ ((φ \land (y \in B \land a \in B \land r \in (y H a))) \land (f \in (y H y) \land k \in (a H a))) \to k \in (a H a)$
84	81 82 83	3jca	$⊢ ((φ \land (y \in B \land a \in B \land r \in (y H a))) \land (f \in (y H y) \land k \in (a H a))) \to (f \in (y H y) \land r \in (y H a) \land k \in (a H a))$
85		simplll	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to x = y$
86	85	eleq1d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (x \in B \leftrightarrow y \in B)$
87	86	anbi1d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to ((x \in B \land y \in B) \leftrightarrow (y \in B \land y \in B))$
88	87 34	bitrdi	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to ((x \in B \land y \in B) \leftrightarrow y \in B)$
89		simpllr	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to z = a$
90	89	eleq1d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (z \in B \leftrightarrow a \in B)$
91		simplr	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to w = a$
92	91	eleq1d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (w \in B \leftrightarrow a \in B)$
93	90 92	anbi12d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to ((z \in B \land w \in B) \leftrightarrow (a \in B \land a \in B))$
94		anidm	$⊢ (a \in B \land a \in B) \leftrightarrow a \in B$
95	93 94	bitrdi	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to ((z \in B \land w \in B) \leftrightarrow a \in B)$
96	85	oveq1d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to x H y = y H y$
97	96	eleq2d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (f \in (x H y) \leftrightarrow f \in (y H y))$
98		simpr	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to g = r$
99	89	oveq2d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to y H z = y H a$
100	98 99	eleq12d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (g \in (y H z) \leftrightarrow r \in (y H a))$
101	89 91	oveq12d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to z H w = a H a$
102	101	eleq2d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (k \in (z H w) \leftrightarrow k \in (a H a))$
103	97 100 102	3anbi123d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to ((f \in (x H y) \land g \in (y H z) \land k \in (z H w)) \leftrightarrow (f \in (y H y) \land r \in (y H a) \land k \in (a H a)))$
104	88 95 103	3anbi123d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (((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 (y \in B \land a \in B \land (f \in (y H y) \land r \in (y H a) \land k \in (a H a))))$
105	5 104	syl5bb	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (ψ \leftrightarrow (y \in B \land a \in B \land (f \in (y H y) \land r \in (y H a) \land k \in (a H a))))$
106	105	anbi2d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to ((φ \land ψ) \leftrightarrow (φ \land (y \in B \land a \in B \land (f \in (y H y) \land r \in (y H a) \land k \in (a H a)))))$
107	89	oveq2d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to ⟨y, y⟩ \underset{˙}{\cdot} z = ⟨y, y⟩ \underset{˙}{\cdot} a$
108		eqidd	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to \underset{˙}{1} = \underset{˙}{1}$
109	107 98 108	oveq123d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1}$
110	109 98	eqeq12d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g \leftrightarrow r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r)$
111	106 110	imbi12d	$⊢ (((x = y \land z = a) \land w = a) \land g = r) \to (((φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g) \leftrightarrow ((φ \land (y \in B \land a \in B \land (f \in (y H y) \land r \in (y H a) \land k \in (a H a)))) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r))$
112	111	sbiedvw	$⊢ ((x = y \land z = a) \land w = a) \to ([r/ g] ((φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g) \leftrightarrow ((φ \land (y \in B \land a \in B \land (f \in (y H y) \land r \in (y H a) \land k \in (a H a)))) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r))$
113	112	sbiedvw	$⊢ (x = y \land z = a) \to ([a/ w] [r/ g] ((φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g) \leftrightarrow ((φ \land (y \in B \land a \in B \land (f \in (y H y) \land r \in (y H a) \land k \in (a H a)))) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r))$
114	113	sbiedvw	$⊢ x = y \to ([a/ z] [a/ w] [r/ g] ((φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g) \leftrightarrow ((φ \land (y \in B \land a \in B \land (f \in (y H y) \land r \in (y H a) \land k \in (a H a)))) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r))$
115	8	sbt	$⊢ [r/ g] ((φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g)$
116	115	sbt	$⊢ [a/ w] [r/ g] ((φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g)$
117	116	sbt	$⊢ [a/ z] [a/ w] [r/ g] ((φ \land ψ) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g)$
118	114 117	chvarvv	$⊢ (φ \land (y \in B \land a \in B \land (f \in (y H y) \land r \in (y H a) \land k \in (a H a)))) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r$
119	78 79 80 84 118	syl13anc	$⊢ ((φ \land (y \in B \land a \in B \land r \in (y H a))) \land (f \in (y H y) \land k \in (a H a))) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r$
120	119	ex	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to ((f \in (y H y) \land k \in (a H a)) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r)$
121	120	exlimdvv	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to (\exists f \exists k (f \in (y H y) \land k \in (a H a)) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r)$
122	77 121	syl5bir	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to ((\exists f f \in (y H y) \land \exists k k \in (a H a)) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r)$
123	67 76 122	mp2and	$⊢ (φ \land (y \in B \land a \in B \land r \in (y H a))) \to r (⟨y, y⟩ \underset{˙}{\cdot} a) \underset{˙}{1} = r$
124		id	$⊢ y = z \to y = z$
125	124 124	oveq12d	$⊢ y = z \to y H y = z H z$
126	125	neeq1d	$⊢ y = z \to (y H y \neq \emptyset \leftrightarrow z H z \neq \emptyset)$
127	71	3ad2ant1	$⊢ (φ \land (y \in B \land a \in B \land z \in B) \land (r \in (y H a) \land g \in (a H z))) \to \forall y \in B y H y \neq \emptyset$
128		simp23	$⊢ (φ \land (y \in B \land a \in B \land z \in B) \land (r \in (y H a) \land g \in (a H z))) \to z \in B$
129	126 127 128	rspcdva	$⊢ (φ \land (y \in B \land a \in B \land z \in B) \land (r \in (y H a) \land g \in (a H z))) \to z H z \neq \emptyset$
130		n0	$⊢ z H z \neq \emptyset \leftrightarrow \exists k k \in (z H z)$
131	129 130	sylib	$⊢ (φ \land (y \in B \land a \in B \land z \in B) \land (r \in (y H a) \land g \in (a H z))) \to \exists k k \in (z H z)$
132		eleq1w	$⊢ x = y \to (x \in B \leftrightarrow y \in B)$
133	132	3anbi1d	$⊢ x = y \to ((x \in B \land a \in B \land z \in B) \leftrightarrow (y \in B \land a \in B \land z \in B))$
134		oveq1	$⊢ x = y \to x H a = y H a$
135	134	eleq2d	$⊢ x = y \to (r \in (x H a) \leftrightarrow r \in (y H a))$
136	135	anbi1d	$⊢ x = y \to ((r \in (x H a) \land g \in (a H z)) \leftrightarrow (r \in (y H a) \land g \in (a H z)))$
137	136	anbi1d	$⊢ x = y \to (((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)) \leftrightarrow ((r \in (y H a) \land g \in (a H z)) \land k \in (z H z)))$
138	133 137	anbi12d	$⊢ x = y \to (((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z))) \leftrightarrow ((y \in B \land a \in B \land z \in B) \land ((r \in (y H a) \land g \in (a H z)) \land k \in (z H z))))$
139	138	anbi2d	$⊢ x = y \to ((φ \land ((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)))) \leftrightarrow (φ \land ((y \in B \land a \in B \land z \in B) \land ((r \in (y H a) \land g \in (a H z)) \land k \in (z H z)))))$
140		opeq1	$⊢ x = y \to ⟨x, a⟩ = ⟨y, a⟩$
141	140	oveq1d	$⊢ x = y \to ⟨x, a⟩ \underset{˙}{\cdot} z = ⟨y, a⟩ \underset{˙}{\cdot} z$
142	141	oveqd	$⊢ x = y \to g (⟨x, a⟩ \underset{˙}{\cdot} z) r = g (⟨y, a⟩ \underset{˙}{\cdot} z) r$
143		oveq1	$⊢ x = y \to x H z = y H z$
144	142 143	eleq12d	$⊢ x = y \to (g (⟨x, a⟩ \underset{˙}{\cdot} z) r \in (x H z) \leftrightarrow g (⟨y, a⟩ \underset{˙}{\cdot} z) r \in (y H z))$
145	139 144	imbi12d	$⊢ x = y \to (((φ \land ((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)))) \to g (⟨x, a⟩ \underset{˙}{\cdot} z) r \in (x H z)) \leftrightarrow ((φ \land ((y \in B \land a \in B \land z \in B) \land ((r \in (y H a) \land g \in (a H z)) \land k \in (z H z)))) \to g (⟨y, a⟩ \underset{˙}{\cdot} z) r \in (y H z)))$
146		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)))$
147	5 146	bitri	$⊢ ψ \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)))$
148		simpll	$⊢ ((y = a \land w = z) \land f = r) \to y = a$
149	148	eleq1d	$⊢ ((y = a \land w = z) \land f = r) \to (y \in B \leftrightarrow a \in B)$
150	149	anbi2d	$⊢ ((y = a \land w = z) \land f = r) \to ((x \in B \land y \in B) \leftrightarrow (x \in B \land a \in B))$
151		simplr	$⊢ ((y = a \land w = z) \land f = r) \to w = z$
152	151	eleq1d	$⊢ ((y = a \land w = z) \land f = r) \to (w \in B \leftrightarrow z \in B)$
153	152	anbi2d	$⊢ ((y = a \land w = z) \land f = r) \to ((z \in B \land w \in B) \leftrightarrow (z \in B \land z \in B))$
154		anidm	$⊢ (z \in B \land z \in B) \leftrightarrow z \in B$
155	153 154	bitrdi	$⊢ ((y = a \land w = z) \land f = r) \to ((z \in B \land w \in B) \leftrightarrow z \in B)$
156	150 155	anbi12d	$⊢ ((y = a \land w = z) \land f = r) \to (((x \in B \land y \in B) \land (z \in B \land w \in B)) \leftrightarrow ((x \in B \land a \in B) \land z \in B))$
157		df-3an	$⊢ (x \in B \land a \in B \land z \in B) \leftrightarrow ((x \in B \land a \in B) \land z \in B)$
158	156 157	bitr4di	$⊢ ((y = a \land w = z) \land f = r) \to (((x \in B \land y \in B) \land (z \in B \land w \in B)) \leftrightarrow (x \in B \land a \in B \land z \in B))$
159		simpr	$⊢ ((y = a \land w = z) \land f = r) \to f = r$
160	148	oveq2d	$⊢ ((y = a \land w = z) \land f = r) \to x H y = x H a$
161	159 160	eleq12d	$⊢ ((y = a \land w = z) \land f = r) \to (f \in (x H y) \leftrightarrow r \in (x H a))$
162	148	oveq1d	$⊢ ((y = a \land w = z) \land f = r) \to y H z = a H z$
163	162	eleq2d	$⊢ ((y = a \land w = z) \land f = r) \to (g \in (y H z) \leftrightarrow g \in (a H z))$
164	151	oveq2d	$⊢ ((y = a \land w = z) \land f = r) \to z H w = z H z$
165	164	eleq2d	$⊢ ((y = a \land w = z) \land f = r) \to (k \in (z H w) \leftrightarrow k \in (z H z))$
166	161 163 165	3anbi123d	$⊢ ((y = a \land w = z) \land f = r) \to ((f \in (x H y) \land g \in (y H z) \land k \in (z H w)) \leftrightarrow (r \in (x H a) \land g \in (a H z) \land k \in (z H z)))$
167		df-3an	$⊢ (r \in (x H a) \land g \in (a H z) \land k \in (z H z)) \leftrightarrow ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z))$
168	166 167	bitrdi	$⊢ ((y = a \land w = z) \land f = r) \to ((f \in (x H y) \land g \in (y H z) \land k \in (z H w)) \leftrightarrow ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)))$
169	158 168	anbi12d	$⊢ ((y = a \land w = z) \land f = r) \to ((((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 a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z))))$
170	147 169	syl5bb	$⊢ ((y = a \land w = z) \land f = r) \to (ψ \leftrightarrow ((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z))))$
171	170	anbi2d	$⊢ ((y = a \land w = z) \land f = r) \to ((φ \land ψ) \leftrightarrow (φ \land ((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)))))$
172	148	opeq2d	$⊢ ((y = a \land w = z) \land f = r) \to ⟨x, y⟩ = ⟨x, a⟩$
173	172	oveq1d	$⊢ ((y = a \land w = z) \land f = r) \to ⟨x, y⟩ \underset{˙}{\cdot} z = ⟨x, a⟩ \underset{˙}{\cdot} z$
174		eqidd	$⊢ ((y = a \land w = z) \land f = r) \to g = g$
175	173 174 159	oveq123d	$⊢ ((y = a \land w = z) \land f = r) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, a⟩ \underset{˙}{\cdot} z) r$
176	175	eleq1d	$⊢ ((y = a \land w = z) \land f = r) \to (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \leftrightarrow g (⟨x, a⟩ \underset{˙}{\cdot} z) r \in (x H z))$
177	171 176	imbi12d	$⊢ ((y = a \land w = z) \land f = r) \to (((φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)) \leftrightarrow ((φ \land ((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)))) \to g (⟨x, a⟩ \underset{˙}{\cdot} z) r \in (x H z)))$
178	177	sbiedvw	$⊢ (y = a \land w = z) \to ([r/ f] ((φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)) \leftrightarrow ((φ \land ((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)))) \to g (⟨x, a⟩ \underset{˙}{\cdot} z) r \in (x H z)))$
179	178	sbiedvw	$⊢ y = a \to ([z/ w] [r/ f] ((φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)) \leftrightarrow ((φ \land ((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)))) \to g (⟨x, a⟩ \underset{˙}{\cdot} z) r \in (x H z)))$
180	9	sbt	$⊢ [r/ f] ((φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z))$
181	180	sbt	$⊢ [z/ w] [r/ f] ((φ \land ψ) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z))$
182	179 181	chvarvv	$⊢ (φ \land ((x \in B \land a \in B \land z \in B) \land ((r \in (x H a) \land g \in (a H z)) \land k \in (z H z)))) \to g (⟨x, a⟩ \underset{˙}{\cdot} z) r \in (x H z)$
183	145 182	chvarvv	$⊢ (φ \land ((y \in B \land a \in B \land z \in B) \land ((r \in (y H a) \land g \in (a H z)) \land k \in (z H z)))) \to g (⟨y, a⟩ \underset{˙}{\cdot} z) r \in (y H z)$
184	183	exp45	$⊢ φ \to ((y \in B \land a \in B \land z \in B) \to ((r \in (y H a) \land g \in (a H z)) \to (k \in (z H z) \to g (⟨y, a⟩ \underset{˙}{\cdot} z) r \in (y H z))))$
185	184	3imp	$⊢ (φ \land (y \in B \land a \in B \land z \in B) \land (r \in (y H a) \land g \in (a H z))) \to (k \in (z H z) \to g (⟨y, a⟩ \underset{˙}{\cdot} z) r \in (y H z))$
186	185	exlimdv	$⊢ (φ \land (y \in B \land a \in B \land z \in B) \land (r \in (y H a) \land g \in (a H z))) \to (\exists k k \in (z H z) \to g (⟨y, a⟩ \underset{˙}{\cdot} z) r \in (y H z))$
187	131 186	mpd	$⊢ (φ \land (y \in B \land a \in B \land z \in B) \land (r \in (y H a) \land g \in (a H z))) \to g (⟨y, a⟩ \underset{˙}{\cdot} z) r \in (y H z)$
188	132	anbi1d	$⊢ x = y \to ((x \in B \land a \in B) \leftrightarrow (y \in B \land a \in B))$
189	188	anbi1d	$⊢ x = y \to (((x \in B \land a \in B) \land (z \in B \land w \in B)) \leftrightarrow ((y \in B \land a \in B) \land (z \in B \land w \in B)))$
190	135	3anbi1d	$⊢ x = y \to ((r \in (x H a) \land g \in (a H z) \land k \in (z H w)) \leftrightarrow (r \in (y H a) \land g \in (a H z) \land k \in (z H w)))$
191	189 190	3anbi23d	$⊢ x = y \to ((φ \land ((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))) \leftrightarrow (φ \land ((y \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (y H a) \land g \in (a H z) \land k \in (z H w))))$
192	140	oveq1d	$⊢ x = y \to ⟨x, a⟩ \underset{˙}{\cdot} w = ⟨y, a⟩ \underset{˙}{\cdot} w$
193	192	oveqd	$⊢ x = y \to (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨x, a⟩ \underset{˙}{\cdot} w) r = (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨y, a⟩ \underset{˙}{\cdot} w) r$
194		opeq1	$⊢ x = y \to ⟨x, z⟩ = ⟨y, z⟩$
195	194	oveq1d	$⊢ x = y \to ⟨x, z⟩ \underset{˙}{\cdot} w = ⟨y, z⟩ \underset{˙}{\cdot} w$
196		eqidd	$⊢ x = y \to k = k$
197	195 196 142	oveq123d	$⊢ x = y \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, a⟩ \underset{˙}{\cdot} z) r) = k (⟨y, z⟩ \underset{˙}{\cdot} w) (g (⟨y, a⟩ \underset{˙}{\cdot} z) r)$
198	193 197	eqeq12d	$⊢ x = y \to ((k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨x, a⟩ \underset{˙}{\cdot} w) r = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, a⟩ \underset{˙}{\cdot} z) r) \leftrightarrow (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨y, a⟩ \underset{˙}{\cdot} w) r = k (⟨y, z⟩ \underset{˙}{\cdot} w) (g (⟨y, a⟩ \underset{˙}{\cdot} z) r))$
199	191 198	imbi12d	$⊢ x = y \to (((φ \land ((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))) \to (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨x, a⟩ \underset{˙}{\cdot} w) r = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, a⟩ \underset{˙}{\cdot} z) r)) \leftrightarrow ((φ \land ((y \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (y H a) \land g \in (a H z) \land k \in (z H w))) \to (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨y, a⟩ \underset{˙}{\cdot} w) r = k (⟨y, z⟩ \underset{˙}{\cdot} w) (g (⟨y, a⟩ \underset{˙}{\cdot} z) r)))$
200		simpl	$⊢ (y = a \land f = r) \to y = a$
201	200	eleq1d	$⊢ (y = a \land f = r) \to (y \in B \leftrightarrow a \in B)$
202	201	anbi2d	$⊢ (y = a \land f = r) \to ((x \in B \land y \in B) \leftrightarrow (x \in B \land a \in B))$
203		simpr	$⊢ (y = a \land f = r) \to f = r$
204	200	oveq2d	$⊢ (y = a \land f = r) \to x H y = x H a$
205	203 204	eleq12d	$⊢ (y = a \land f = r) \to (f \in (x H y) \leftrightarrow r \in (x H a))$
206	200	oveq1d	$⊢ (y = a \land f = r) \to y H z = a H z$
207	206	eleq2d	$⊢ (y = a \land f = r) \to (g \in (y H z) \leftrightarrow g \in (a H z))$
208	205 207	3anbi12d	$⊢ (y = a \land f = r) \to ((f \in (x H y) \land g \in (y H z) \land k \in (z H w)) \leftrightarrow (r \in (x H a) \land g \in (a H z) \land k \in (z H w)))$
209	202 208	3anbi13d	$⊢ (y = a \land f = r) \to (((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 a \in B) \land (z \in B \land w \in B) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))))$
210	5 209	syl5bb	$⊢ (y = a \land f = r) \to (ψ \leftrightarrow ((x \in B \land a \in B) \land (z \in B \land w \in B) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))))$
211		df-3an	$⊢ ((x \in B \land a \in B) \land (z \in B \land w \in B) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))) \leftrightarrow (((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w)))$
212	210 211	bitrdi	$⊢ (y = a \land f = r) \to (ψ \leftrightarrow (((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))))$
213	212	anbi2d	$⊢ (y = a \land f = r) \to ((φ \land ψ) \leftrightarrow (φ \land (((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w)))))$
214		3anass	$⊢ (φ \land ((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))) \leftrightarrow (φ \land (((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))))$
215	213 214	bitr4di	$⊢ (y = a \land f = r) \to ((φ \land ψ) \leftrightarrow (φ \land ((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))))$
216	200	opeq2d	$⊢ (y = a \land f = r) \to ⟨x, y⟩ = ⟨x, a⟩$
217	216	oveq1d	$⊢ (y = a \land f = r) \to ⟨x, y⟩ \underset{˙}{\cdot} w = ⟨x, a⟩ \underset{˙}{\cdot} w$
218	200	opeq1d	$⊢ (y = a \land f = r) \to ⟨y, z⟩ = ⟨a, z⟩$
219	218	oveq1d	$⊢ (y = a \land f = r) \to ⟨y, z⟩ \underset{˙}{\cdot} w = ⟨a, z⟩ \underset{˙}{\cdot} w$
220	219	oveqd	$⊢ (y = a \land f = r) \to k (⟨y, z⟩ \underset{˙}{\cdot} w) g = k (⟨a, z⟩ \underset{˙}{\cdot} w) g$
221	217 220 203	oveq123d	$⊢ (y = a \land f = r) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨x, a⟩ \underset{˙}{\cdot} w) r$
222	216	oveq1d	$⊢ (y = a \land f = r) \to ⟨x, y⟩ \underset{˙}{\cdot} z = ⟨x, a⟩ \underset{˙}{\cdot} z$
223		eqidd	$⊢ (y = a \land f = r) \to g = g$
224	222 223 203	oveq123d	$⊢ (y = a \land f = r) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, a⟩ \underset{˙}{\cdot} z) r$
225	224	oveq2d	$⊢ (y = a \land f = r) \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, a⟩ \underset{˙}{\cdot} z) r)$
226	221 225	eqeq12d	$⊢ (y = a \land f = r) \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) \leftrightarrow (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨x, a⟩ \underset{˙}{\cdot} w) r = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, a⟩ \underset{˙}{\cdot} z) r))$
227	215 226	imbi12d	$⊢ (y = a \land f = r) \to (((φ \land ψ) \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)) \leftrightarrow ((φ \land ((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))) \to (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨x, a⟩ \underset{˙}{\cdot} w) r = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, a⟩ \underset{˙}{\cdot} z) r)))$
228	227	sbiedvw	$⊢ y = a \to ([r/ f] ((φ \land ψ) \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)) \leftrightarrow ((φ \land ((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))) \to (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨x, a⟩ \underset{˙}{\cdot} w) r = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, a⟩ \underset{˙}{\cdot} z) r)))$
229	10	sbt	$⊢ [r/ f] ((φ \land ψ) \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))$
230	228 229	chvarvv	$⊢ (φ \land ((x \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (x H a) \land g \in (a H z) \land k \in (z H w))) \to (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨x, a⟩ \underset{˙}{\cdot} w) r = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, a⟩ \underset{˙}{\cdot} z) r)$
231	199 230	chvarvv	$⊢ (φ \land ((y \in B \land a \in B) \land (z \in B \land w \in B)) \land (r \in (y H a) \land g \in (a H z) \land k \in (z H w))) \to (k (⟨a, z⟩ \underset{˙}{\cdot} w) g) (⟨y, a⟩ \underset{˙}{\cdot} w) r = k (⟨y, z⟩ \underset{˙}{\cdot} w) (g (⟨y, a⟩ \underset{˙}{\cdot} z) r)$
232	1 2 3 4 6 64 123 187 231	iscatd	$⊢ φ \to C \in Cat$
233	1 2 3 232 6 64 123	catidd	$⊢ φ \to Id (C) = (y \in B ⟼ \underset{˙}{1})$
234	232 233	jca	$⊢ φ \to (C \in Cat \land Id (C) = (y \in B ⟼ \underset{˙}{1}))$

Metamath Proof Explorer

Theorem iscatd2

Proof