MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscatd Structured version   Visualization version   GIF version

Theorem iscatd 17382
Description: Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
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
Ref Expression
iscatd (𝜑𝐶 ∈ Cat)
Distinct variable groups:   𝑓,𝑔,𝑦, 1   𝑓,𝑘,𝑤,𝑥,𝑧,𝐵,𝑔,𝑦   𝜑,𝑓,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧   · ,𝑔   𝐶,𝑓,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧   𝑓,𝐻,𝑔,𝑘,𝑤
Allowed substitution hints:   · (𝑥,𝑦,𝑧,𝑤,𝑓,𝑘)   1 (𝑥,𝑧,𝑤,𝑘)   𝐻(𝑥,𝑦,𝑧)   𝑉(𝑥,𝑦,𝑧,𝑤,𝑓,𝑔,𝑘)

Proof of Theorem iscatd
StepHypRef Expression
1 iscatd.1 . . . . . 6 ((𝜑𝑥𝐵) → 1 ∈ (𝑥𝐻𝑥))
2 iscatd.2 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓)
323exp2 1353 . . . . . . . . . 10 (𝜑 → (𝑥𝐵 → (𝑦𝐵 → (𝑓 ∈ (𝑦𝐻𝑥) → ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))))
43imp31 418 . . . . . . . . 9 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → (𝑓 ∈ (𝑦𝐻𝑥) → ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
54ralrimiv 3102 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓)
6 iscatd.3 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)
763exp2 1353 . . . . . . . . . 10 (𝜑 → (𝑥𝐵 → (𝑦𝐵 → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))))
87imp31 418 . . . . . . . . 9 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
98ralrimiv 3102 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)
105, 9jca 512 . . . . . . 7 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
1110ralrimiva 3103 . . . . . 6 ((𝜑𝑥𝐵) → ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
12 oveq1 7282 . . . . . . . . . . 11 (𝑔 = 1 → (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓))
1312eqeq1d 2740 . . . . . . . . . 10 (𝑔 = 1 → ((𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
1413ralbidv 3112 . . . . . . . . 9 (𝑔 = 1 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
15 oveq2 7283 . . . . . . . . . . 11 (𝑔 = 1 → (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ))
1615eqeq1d 2740 . . . . . . . . . 10 (𝑔 = 1 → ((𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
1716ralbidv 3112 . . . . . . . . 9 (𝑔 = 1 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
1814, 17anbi12d 631 . . . . . . . 8 (𝑔 = 1 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)))
1918ralbidv 3112 . . . . . . 7 (𝑔 = 1 → (∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)))
2019rspcev 3561 . . . . . 6 (( 1 ∈ (𝑥𝐻𝑥) ∧ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
211, 11, 20syl2anc 584 . . . . 5 ((𝜑𝑥𝐵) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
22 iscatd.4 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
23223expia 1120 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))
24233exp2 1353 . . . . . . . . 9 (𝜑 → (𝑥𝐵 → (𝑦𝐵 → (𝑧𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))))))
2524imp43 428 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))
26 iscatd.5 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
27263expa 1117 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
28273exp2 1353 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑔 ∈ (𝑦𝐻𝑧) → (𝑘 ∈ (𝑧𝐻𝑤) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
2928imp32 419 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑤) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3029ralrimiv 3102 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
3130ex 413 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3231expr 457 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑧𝐵𝑤𝐵) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
3332expd 416 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑧𝐵 → (𝑤𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
3433expr 457 . . . . . . . . . 10 ((𝜑𝑥𝐵) → (𝑦𝐵 → (𝑧𝐵 → (𝑤𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))))
3534imp42 427 . . . . . . . . 9 ((((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑤𝐵) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3635ralrimdva 3106 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3725, 36jcad 513 . . . . . . 7 (((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
3837ralrimivv 3122 . . . . . 6 (((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3938ralrimivva 3123 . . . . 5 ((𝜑𝑥𝐵) → ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
4021, 39jca 512 . . . 4 ((𝜑𝑥𝐵) → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
4140ralrimiva 3103 . . 3 (𝜑 → ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
42 iscatd.b . . . 4 (𝜑𝐵 = (Base‘𝐶))
43 iscatd.h . . . . . . 7 (𝜑𝐻 = (Hom ‘𝐶))
4443oveqd 7292 . . . . . 6 (𝜑 → (𝑥𝐻𝑥) = (𝑥(Hom ‘𝐶)𝑥))
4543oveqd 7292 . . . . . . . . 9 (𝜑 → (𝑦𝐻𝑥) = (𝑦(Hom ‘𝐶)𝑥))
46 iscatd.o . . . . . . . . . . . 12 (𝜑· = (comp‘𝐶))
4746oveqd 7292 . . . . . . . . . . 11 (𝜑 → (⟨𝑦, 𝑥· 𝑥) = (⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥))
4847oveqd 7292 . . . . . . . . . 10 (𝜑 → (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓))
4948eqeq1d 2740 . . . . . . . . 9 (𝜑 → ((𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓))
5045, 49raleqbidv 3336 . . . . . . . 8 (𝜑 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓))
5143oveqd 7292 . . . . . . . . 9 (𝜑 → (𝑥𝐻𝑦) = (𝑥(Hom ‘𝐶)𝑦))
5246oveqd 7292 . . . . . . . . . . 11 (𝜑 → (⟨𝑥, 𝑥· 𝑦) = (⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦))
5352oveqd 7292 . . . . . . . . . 10 (𝜑 → (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔))
5453eqeq1d 2740 . . . . . . . . 9 (𝜑 → ((𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓))
5551, 54raleqbidv 3336 . . . . . . . 8 (𝜑 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓))
5650, 55anbi12d 631 . . . . . . 7 (𝜑 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓)))
5742, 56raleqbidv 3336 . . . . . 6 (𝜑 → (∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓)))
5844, 57rexeqbidv 3337 . . . . 5 (𝜑 → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓)))
5943oveqd 7292 . . . . . . . . 9 (𝜑 → (𝑦𝐻𝑧) = (𝑦(Hom ‘𝐶)𝑧))
6046oveqd 7292 . . . . . . . . . . . 12 (𝜑 → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
6160oveqd 7292 . . . . . . . . . . 11 (𝜑 → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
6243oveqd 7292 . . . . . . . . . . 11 (𝜑 → (𝑥𝐻𝑧) = (𝑥(Hom ‘𝐶)𝑧))
6361, 62eleq12d 2833 . . . . . . . . . 10 (𝜑 → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
6443oveqd 7292 . . . . . . . . . . . 12 (𝜑 → (𝑧𝐻𝑤) = (𝑧(Hom ‘𝐶)𝑤))
6546oveqd 7292 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑥, 𝑦· 𝑤) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤))
6646oveqd 7292 . . . . . . . . . . . . . . 15 (𝜑 → (⟨𝑦, 𝑧· 𝑤) = (⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤))
6766oveqd 7292 . . . . . . . . . . . . . 14 (𝜑 → (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔) = (𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
68 eqidd 2739 . . . . . . . . . . . . . 14 (𝜑𝑓 = 𝑓)
6965, 67, 68oveq123d 7296 . . . . . . . . . . . . 13 (𝜑 → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = ((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓))
7046oveqd 7292 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑥, 𝑧· 𝑤) = (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤))
71 eqidd 2739 . . . . . . . . . . . . . 14 (𝜑𝑘 = 𝑘)
7270, 71, 61oveq123d 7296 . . . . . . . . . . . . 13 (𝜑 → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
7369, 72eqeq12d 2754 . . . . . . . . . . . 12 (𝜑 → (((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
7464, 73raleqbidv 3336 . . . . . . . . . . 11 (𝜑 → (∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
7542, 74raleqbidv 3336 . . . . . . . . . 10 (𝜑 → (∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
7663, 75anbi12d 631 . . . . . . . . 9 (𝜑 → (((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
7759, 76raleqbidv 3336 . . . . . . . 8 (𝜑 → (∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
7851, 77raleqbidv 3336 . . . . . . 7 (𝜑 → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
7942, 78raleqbidv 3336 . . . . . 6 (𝜑 → (∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
8042, 79raleqbidv 3336 . . . . 5 (𝜑 → (∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
8158, 80anbi12d 631 . . . 4 (𝜑 → ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
8242, 81raleqbidv 3336 . . 3 (𝜑 → (∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
8341, 82mpbid 231 . 2 (𝜑 → ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
84 iscatd.c . . 3 (𝜑𝐶𝑉)
85 eqid 2738 . . . 4 (Base‘𝐶) = (Base‘𝐶)
86 eqid 2738 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
87 eqid 2738 . . . 4 (comp‘𝐶) = (comp‘𝐶)
8885, 86, 87iscat 17381 . . 3 (𝐶𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
8984, 88syl 17 . 2 (𝜑 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
9083, 89mpbird 256 1 (𝜑𝐶 ∈ Cat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  wral 3064  wrex 3065  cop 4567  cfv 6433  (class class class)co 7275  Basecbs 16912  Hom chom 16973  compcco 16974  Catccat 17373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-cat 17377
This theorem is referenced by:  iscatd2  17390  0catg  17397
  Copyright terms: Public domain W3C validator