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

Theorem iscatd 16381
 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 1307 . . . . . . . . . 10 (𝜑 → (𝑥𝐵 → (𝑦𝐵 → (𝑓 ∈ (𝑦𝐻𝑥) → ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))))
43imp31 447 . . . . . . . . 9 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → (𝑓 ∈ (𝑦𝐻𝑥) → ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
54ralrimiv 2994 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓)
6 iscatd.3 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)
763exp2 1307 . . . . . . . . . 10 (𝜑 → (𝑥𝐵 → (𝑦𝐵 → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))))
87imp31 447 . . . . . . . . 9 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
98ralrimiv 2994 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)
105, 9jca 553 . . . . . . 7 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
1110ralrimiva 2995 . . . . . 6 ((𝜑𝑥𝐵) → ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
12 oveq1 6697 . . . . . . . . . . 11 (𝑔 = 1 → (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓))
1312eqeq1d 2653 . . . . . . . . . 10 (𝑔 = 1 → ((𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ ( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
1413ralbidv 3015 . . . . . . . . 9 (𝑔 = 1 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
15 oveq2 6698 . . . . . . . . . . 11 (𝑔 = 1 → (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ))
1615eqeq1d 2653 . . . . . . . . . 10 (𝑔 = 1 → ((𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
1716ralbidv 3015 . . . . . . . . 9 (𝑔 = 1 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓))
1814, 17anbi12d 747 . . . . . . . 8 (𝑔 = 1 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)))
1918ralbidv 3015 . . . . . . 7 (𝑔 = 1 → (∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)))
2019rspcev 3340 . . . . . 6 (( 1 ∈ (𝑥𝐻𝑥) ∧ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)( 1 (⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦) 1 ) = 𝑓)) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
211, 11, 20syl2anc 694 . . . . 5 ((𝜑𝑥𝐵) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
22 iscatd.4 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
23223expia 1286 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))
24233exp2 1307 . . . . . . . . 9 (𝜑 → (𝑥𝐵 → (𝑦𝐵 → (𝑧𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))))))
2524imp43 620 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))
26 iscatd.5 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
27263expa 1284 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
28273exp2 1307 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) → (𝑓 ∈ (𝑥𝐻𝑦) → (𝑔 ∈ (𝑦𝐻𝑧) → (𝑘 ∈ (𝑧𝐻𝑤) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
2928imp32 448 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑤) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3029ralrimiv 2994 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
3130ex 449 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵))) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3231expr 642 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑧𝐵𝑤𝐵) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
3332expd 451 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑧𝐵 → (𝑤𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
3433expr 642 . . . . . . . . . 10 ((𝜑𝑥𝐵) → (𝑦𝐵 → (𝑧𝐵 → (𝑤𝐵 → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))))
3534imp42 619 . . . . . . . . 9 ((((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑤𝐵) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3635ralrimdva 2998 . . . . . . . 8 (((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3725, 36jcad 554 . . . . . . 7 (((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
3837ralrimivv 2999 . . . . . 6 (((𝜑𝑥𝐵) ∧ (𝑦𝐵𝑧𝐵)) → ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
3938ralrimivva 3000 . . . . 5 ((𝜑𝑥𝐵) → ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
4021, 39jca 553 . . . 4 ((𝜑𝑥𝐵) → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
4140ralrimiva 2995 . . 3 (𝜑 → ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
42 iscatd.b . . . 4 (𝜑𝐵 = (Base‘𝐶))
43 iscatd.h . . . . . . 7 (𝜑𝐻 = (Hom ‘𝐶))
4443oveqd 6707 . . . . . 6 (𝜑 → (𝑥𝐻𝑥) = (𝑥(Hom ‘𝐶)𝑥))
4543oveqd 6707 . . . . . . . . 9 (𝜑 → (𝑦𝐻𝑥) = (𝑦(Hom ‘𝐶)𝑥))
46 iscatd.o . . . . . . . . . . . 12 (𝜑· = (comp‘𝐶))
4746oveqd 6707 . . . . . . . . . . 11 (𝜑 → (⟨𝑦, 𝑥· 𝑥) = (⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥))
4847oveqd 6707 . . . . . . . . . 10 (𝜑 → (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓))
4948eqeq1d 2653 . . . . . . . . 9 (𝜑 → ((𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓))
5045, 49raleqbidv 3182 . . . . . . . 8 (𝜑 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓))
5143oveqd 6707 . . . . . . . . 9 (𝜑 → (𝑥𝐻𝑦) = (𝑥(Hom ‘𝐶)𝑦))
5246oveqd 6707 . . . . . . . . . . 11 (𝜑 → (⟨𝑥, 𝑥· 𝑦) = (⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦))
5352oveqd 6707 . . . . . . . . . 10 (𝜑 → (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔))
5453eqeq1d 2653 . . . . . . . . 9 (𝜑 → ((𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓))
5551, 54raleqbidv 3182 . . . . . . . 8 (𝜑 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓))
5650, 55anbi12d 747 . . . . . . 7 (𝜑 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓)))
5742, 56raleqbidv 3182 . . . . . 6 (𝜑 → (∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓)))
5844, 57rexeqbidv 3183 . . . . 5 (𝜑 → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓)))
5943oveqd 6707 . . . . . . . . 9 (𝜑 → (𝑦𝐻𝑧) = (𝑦(Hom ‘𝐶)𝑧))
6046oveqd 6707 . . . . . . . . . . . 12 (𝜑 → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧))
6160oveqd 6707 . . . . . . . . . . 11 (𝜑 → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
6243oveqd 6707 . . . . . . . . . . 11 (𝜑 → (𝑥𝐻𝑧) = (𝑥(Hom ‘𝐶)𝑧))
6361, 62eleq12d 2724 . . . . . . . . . 10 (𝜑 → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
6443oveqd 6707 . . . . . . . . . . . 12 (𝜑 → (𝑧𝐻𝑤) = (𝑧(Hom ‘𝐶)𝑤))
6546oveqd 6707 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑥, 𝑦· 𝑤) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤))
6646oveqd 6707 . . . . . . . . . . . . . . 15 (𝜑 → (⟨𝑦, 𝑧· 𝑤) = (⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤))
6766oveqd 6707 . . . . . . . . . . . . . 14 (𝜑 → (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔) = (𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
68 eqidd 2652 . . . . . . . . . . . . . 14 (𝜑𝑓 = 𝑓)
6965, 67, 68oveq123d 6711 . . . . . . . . . . . . 13 (𝜑 → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = ((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓))
7046oveqd 6707 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑥, 𝑧· 𝑤) = (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤))
71 eqidd 2652 . . . . . . . . . . . . . 14 (𝜑𝑘 = 𝑘)
7270, 71, 61oveq123d 6711 . . . . . . . . . . . . 13 (𝜑 → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
7369, 72eqeq12d 2666 . . . . . . . . . . . 12 (𝜑 → (((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
7464, 73raleqbidv 3182 . . . . . . . . . . 11 (𝜑 → (∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
7542, 74raleqbidv 3182 . . . . . . . . . 10 (𝜑 → (∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
7663, 75anbi12d 747 . . . . . . . . 9 (𝜑 → (((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
7759, 76raleqbidv 3182 . . . . . . . 8 (𝜑 → (∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
7851, 77raleqbidv 3182 . . . . . . 7 (𝜑 → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
7942, 78raleqbidv 3182 . . . . . 6 (𝜑 → (∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
8042, 79raleqbidv 3182 . . . . 5 (𝜑 → (∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
8158, 80anbi12d 747 . . . 4 (𝜑 → ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
8242, 81raleqbidv 3182 . . 3 (𝜑 → (∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)((𝑘(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
8341, 82mpbid 222 . 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 2651 . . . 4 (Base‘𝐶) = (Base‘𝐶)
86 eqid 2651 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
87 eqid 2651 . . . 4 (comp‘𝐶) = (comp‘𝐶)
8885, 86, 87iscat 16380 . . 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 247 1 (𝜑𝐶 ∈ Cat)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  ⟨cop 4216  ‘cfv 5926  (class class class)co 6690  Basecbs 15904  Hom chom 15999  compcco 16000  Catccat 16372 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-cat 16376 This theorem is referenced by:  iscatd2  16389  0catg  16395
 Copyright terms: Public domain W3C validator