This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscatd

Description: Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses iscatd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
iscatd.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
iscatd.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
iscatd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
iscatd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ ( 𝑥 𝐻 𝑥 ) )
iscatd.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ) ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 )
iscatd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 )
iscatd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
iscatd.5 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
Assertion iscatd ( 𝜑 → 𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 iscatd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2 iscatd.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3 iscatd.o ⊢ ( 𝜑 → · = ( comp ‘ 𝐶 ) )
4 iscatd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5 iscatd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ ( 𝑥 𝐻 𝑥 ) )
6 iscatd.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ) ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 )
7 iscatd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 )
8 iscatd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
9 iscatd.5 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
10 6 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 → ( 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ) ) ) )
11 10 imp31 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) → ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ) )
12 11 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 )
13 7 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) ) ) )
14 13 imp31 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) )
15 14 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 )
16 12 15 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) )
17 16 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) )
18 oveq1 ⊢ ( 𝑔 = 1 → ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) )
19 18 eqeq1d ⊢ ( 𝑔 = 1 → ( ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ) )
20 19 ralbidv ⊢ ( 𝑔 = 1 → ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ) )
21 oveq2 ⊢ ( 𝑔 = 1 → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) )
22 21 eqeq1d ⊢ ( 𝑔 = 1 → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) )
23 22 ralbidv ⊢ ( 𝑔 = 1 → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) )
24 20 23 anbi12d ⊢ ( 𝑔 = 1 → ( ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) ) )
25 24 ralbidv ⊢ ( 𝑔 = 1 → ( ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) ) )
26 25 rspcev ⊢ ( ( 1 ∈ ( 𝑥 𝐻 𝑥 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 1 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 1 ) = 𝑓 ) ) → ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
27 5 17 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
28 8 3expia ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
29 28 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝐵 → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) ) ) ) )
30 29 imp43 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
31 9 3expa ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
32 31 3exp2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) → ( 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
33 32 imp32 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
34 33 ralrimiv ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
35 34 ex ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
36 35 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
37 36 expd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑧 ∈ 𝐵 → ( 𝑤 ∈ 𝐵 → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
38 37 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝐵 → ( 𝑤 ∈ 𝐵 → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) ) )
39 38 imp42 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
40 39 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
41 30 40 jcad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
42 41 ralrimivv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
43 42 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
44 27 43 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
45 44 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
46 2 oveqd ⊢ ( 𝜑 → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
47 2 oveqd ⊢ ( 𝜑 → ( 𝑦 𝐻 𝑥 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
48 3 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) = ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) )
49 48 oveqd ⊢ ( 𝜑 → ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) )
50 49 eqeq1d ⊢ ( 𝜑 → ( ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ) )
51 47 50 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ) )
52 2 oveqd ⊢ ( 𝜑 → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
53 3 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) = ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) )
54 53 oveqd ⊢ ( 𝜑 → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) )
55 54 eqeq1d ⊢ ( 𝜑 → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) )
56 52 55 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) )
57 51 56 anbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
58 1 57 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
59 46 58 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∃ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
60 2 oveqd ⊢ ( 𝜑 → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
61 3 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) )
62 61 oveqd ⊢ ( 𝜑 → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
63 2 oveqd ⊢ ( 𝜑 → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
64 62 63 eleq12d ⊢ ( 𝜑 → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ) )
65 2 oveqd ⊢ ( 𝜑 → ( 𝑧 𝐻 𝑤 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) )
66 3 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) )
67 3 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) = ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) )
68 67 oveqd ⊢ ( 𝜑 → ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) = ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) )
69 eqidd ⊢ ( 𝜑 → 𝑓 = 𝑓 )
70 66 68 69 oveq123d ⊢ ( 𝜑 → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) )
71 3 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) = ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) )
72 eqidd ⊢ ( 𝜑 → 𝑘 = 𝑘 )
73 71 72 62 oveq123d ⊢ ( 𝜑 → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) )
74 70 73 eqeq12d ⊢ ( 𝜑 → ( ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ↔ ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) )
75 65 74 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) )
76 1 75 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) )
77 64 76 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ↔ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) )
78 60 77 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) )
79 52 78 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) )
80 1 79 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) )
81 1 80 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) )
82 59 81 anbi12d ⊢ ( 𝜑 → ( ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ↔ ( ∃ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) ) )
83 1 82 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ∃ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) ) )
84 45 83 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ∃ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) )
85 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
86 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
87 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
88 85 86 87 iscat ⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ Cat ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ∃ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) ) )
89 4 88 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ∃ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐶 ) ∀ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) ) ) )
90 84 89 mpbird ⊢ ( 𝜑 → 𝐶 ∈ Cat )