# Metamath Proof Explorer

## Theorem 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 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
iscatd2.h ${⊢}{\phi }\to {H}=\mathrm{Hom}\left({C}\right)$
iscatd2.o
iscatd2.c ${⊢}{\phi }\to {C}\in {V}$
iscatd2.ps ${⊢}{\psi }↔\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\wedge \left({f}\in \left({x}{H}{y}\right)\wedge {g}\in \left({y}{H}{z}\right)\wedge {k}\in \left({z}{H}{w}\right)\right)\right)$
iscatd2.1
iscatd2.2
iscatd2.3
iscatd2.4
iscatd2.5
Assertion iscatd2

### Proof

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