Metamath Proof Explorer

Theorem iscat

Description: The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses iscat.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
iscat.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
iscat.o ⊢ · = ( comp ‘ 𝐶 )
Assertion iscat ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ Cat ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iscat.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 iscat.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 iscat.o ⊢ · = ( comp ‘ 𝐶 )
4 fvexd ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) ∈ V )
5 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
6 5 1 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
7 fvexd ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) ∈ V )
8 simpl ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → 𝑐 = 𝐶 )
9 8 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
10 9 2 eqtr4di ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = 𝐻 )
11 fvexd ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( comp ‘ 𝑐 ) ∈ V )
12 simpll ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑐 = 𝐶 )
13 12 fveq2d ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
14 13 3 eqtr4di ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( comp ‘ 𝑐 ) = · )
15 simpllr ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → 𝑏 = 𝐵 )
16 simplr ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ℎ = 𝐻 )
17 16 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑥 ℎ 𝑥 ) = ( 𝑥 𝐻 𝑥 ) )
18 16 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑦 ℎ 𝑥 ) = ( 𝑦 𝐻 𝑥 ) )
19 simpr ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → 𝑜 = · )
20 19 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) = ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) )
21 20 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) )
22 21 eqeq1d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ↔ ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ) )
23 18 22 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ) )
24 16 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
25 19 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) = ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) )
26 25 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) )
27 26 eqeq1d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
28 24 27 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) )
29 23 28 anbi12d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ) )
30 15 29 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ) )
31 17 30 rexeqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∃ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ↔ ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ) )
32 16 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑦 ℎ 𝑧 ) = ( 𝑦 𝐻 𝑧 ) )
33 19 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) )
34 33 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) )
35 16 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑥 ℎ 𝑧 ) = ( 𝑥 𝐻 𝑧 ) )
36 34 35 eleq12d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ) )
37 16 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑧 ℎ 𝑤 ) = ( 𝑧 𝐻 𝑤 ) )
38 19 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) = ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) )
39 19 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) = ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) )
40 39 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) = ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) )
41 eqidd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → 𝑓 = 𝑓 )
42 38 40 41 oveq123d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) )
43 19 oveqd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) = ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) )
44 eqidd ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → 𝑘 = 𝑘 )
45 43 44 34 oveq123d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
46 42 45 eqeq12d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ↔ ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
47 37 46 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
48 15 47 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ↔ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) )
49 36 48 anbi12d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ↔ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
50 32 49 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
51 24 50 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
52 15 51 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑧 ∈ 𝑏 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
53 15 52 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) )
54 31 53 anbi12d ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ( ∃ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ) ↔ ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
55 15 54 raleqbidv ⊢ ( ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) ∧ 𝑜 = · ) → ( ∀ 𝑥 ∈ 𝑏 ( ∃ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
56 11 14 55 sbcied2 ⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( [ ( comp ‘ 𝑐 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ( ∃ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
57 7 10 56 sbcied2 ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑏 = 𝐵 ) → ( [ ( Hom ‘ 𝑐 ) / ℎ ] [ ( comp ‘ 𝑐 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ( ∃ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
58 4 6 57 sbcied2 ⊢ ( 𝑐 = 𝐶 → ( [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] [ ( comp ‘ 𝑐 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ( ∃ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )
59 df-cat ⊢ Cat = { 𝑐 ∣ [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] [ ( comp ‘ 𝑐 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ( ∃ 𝑔 ∈ ( 𝑥 ℎ 𝑥 ) ∀ 𝑦 ∈ 𝑏 ( ∀ 𝑓 ∈ ( 𝑦 ℎ 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ 𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ 𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑏 ∀ 𝑘 ∈ ( 𝑧 ℎ 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ 𝑜 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ 𝑜 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ 𝑜 𝑧 ) 𝑓 ) ) ) ) }
60 58 59 elab2g ⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ Cat ↔ ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑔 ∈ ( 𝑥 𝐻 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ · 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ · 𝑦 ) 𝑔 ) = 𝑓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ∀ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) ) ) ) )