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

Theorem iscatd2 16804
Description: Version of iscatd 16796 with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
iscatd2.b (𝜑𝐵 = (Base‘𝐶))
iscatd2.h (𝜑𝐻 = (Hom ‘𝐶))
iscatd2.o (𝜑· = (comp‘𝐶))
iscatd2.c (𝜑𝐶𝑉)
iscatd2.ps (𝜓 ↔ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
iscatd2.1 ((𝜑𝑦𝐵) → 1 ∈ (𝑦𝐻𝑦))
iscatd2.2 ((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
iscatd2.3 ((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
iscatd2.4 ((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
iscatd2.5 ((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
Assertion
Ref Expression
iscatd2 (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦𝐵1 )))
Distinct variable groups:   𝑓,𝑔,𝑘,𝑤,𝑥,𝑧, 1   𝑦,𝑓,𝐵,𝑔,𝑘,𝑤,𝑥,𝑧   𝐶,𝑔,𝑘,𝑤,𝑦,𝑧   𝑓,𝐻,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧   𝜑,𝑓,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧   · ,𝑓,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜓(𝑥,𝑦,𝑧,𝑤,𝑓,𝑔,𝑘)   𝐶(𝑥,𝑓)   1 (𝑦)   𝑉(𝑥,𝑦,𝑧,𝑤,𝑓,𝑔,𝑘)

Proof of Theorem iscatd2
Dummy variables 𝑎 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iscatd2.b . . 3 (𝜑𝐵 = (Base‘𝐶))
2 iscatd2.h . . 3 (𝜑𝐻 = (Hom ‘𝐶))
3 iscatd2.o . . 3 (𝜑· = (comp‘𝐶))
4 iscatd2.c . . 3 (𝜑𝐶𝑉)
5 iscatd2.1 . . 3 ((𝜑𝑦𝐵) → 1 ∈ (𝑦𝐻𝑦))
65ne0d 4181 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝐻𝑦) ≠ ∅)
763ad2antr1 1168 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅)
8 n0 4190 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
97, 8sylib 210 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
10 n0 4190 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
117, 10sylib 210 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
12 exdistrv 1914 . . . . 5 (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)))
13 simpll 754 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑)
14 simplr2 1196 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎𝐵)
15 simplr1 1195 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦𝐵)
1614, 15jca 504 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎𝐵𝑦𝐵))
17 simplr3 1197 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦))
18 simprl 758 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦))
19 simprr 760 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦))
2017, 18, 193jca 1108 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))
21 iscatd2.ps . . . . . . . . . . . . . . 15 (𝜓 ↔ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
22 simplll 762 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎)
2322eleq1d 2844 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐵𝑎𝐵))
2423anbi1d 620 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑎𝐵𝑦𝐵)))
25 simpllr 763 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦)
2625eleq1d 2844 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐵𝑦𝐵))
27 simplr 756 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦)
2827eleq1d 2844 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑦𝐵))
2926, 28anbi12d 621 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑦𝐵𝑦𝐵)))
30 anidm 557 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝐵) ↔ 𝑦𝐵)
3129, 30syl6bb 279 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑦𝐵))
32 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
3322oveq1d 6985 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦))
3432, 33eleq12d 2854 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦)))
3525oveq2d 6986 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦))
3635eleq2d 2845 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦)))
3725, 27oveq12d 6988 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦))
3837eleq2d 2845 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦)))
3934, 36, 383anbi123d 1415 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))
4024, 31, 393anbi123d 1415 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4121, 40syl5bb 275 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4241anbi2d 619 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))))
4322opeq1d 4677 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑦⟩)
4443oveq1d 6985 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑦) = (⟨𝑎, 𝑦· 𝑦))
45 eqidd 2773 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 )
4644, 45, 32oveq123d 6991 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟))
4746, 32eqeq12d 2787 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓 ↔ ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
4842, 47imbi12d 337 . . . . . . . . . . . 12 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
4948sbiedv 2470 . . . . . . . . . . 11 (((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5049sbiedv 2470 . . . . . . . . . 10 ((𝑥 = 𝑎𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5150sbiedv 2470 . . . . . . . . 9 (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
52 iscatd2.2 . . . . . . . . . . . 12 ((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5352sbt 2017 . . . . . . . . . . 11 [𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5453sbt 2017 . . . . . . . . . 10 [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5554sbt 2017 . . . . . . . . 9 [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5651, 55chvarv 2327 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5713, 16, 15, 20, 56syl13anc 1352 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5857ex 405 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
5958exlimdvv 1893 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6012, 59syl5bir 235 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
619, 11, 60mp2and 686 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
6263ad2antr1 1168 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅)
63 n0 4190 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
6462, 63sylib 210 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
65 id 22 . . . . . . . 8 (𝑦 = 𝑎𝑦 = 𝑎)
6665, 65oveq12d 6988 . . . . . . 7 (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎))
6766neeq1d 3020 . . . . . 6 (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅))
686ralrimiva 3126 . . . . . . 7 (𝜑 → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
6968adantr 473 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
70 simpr2 1175 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎𝐵)
7167, 69, 70rspcdva 3535 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅)
72 n0 4190 . . . . 5 ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
7371, 72sylib 210 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
74 exdistrv 1914 . . . . 5 (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)))
75 simpll 754 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑)
76 simplr1 1195 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦𝐵)
77 simplr2 1196 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎𝐵)
78 simprl 758 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦))
79 simplr3 1197 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎))
80 simprr 760 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎))
8178, 79, 803jca 1108 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))
82 simplll 762 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦)
8382eleq1d 2844 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐵𝑦𝐵))
8483anbi1d 620 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑦𝐵𝑦𝐵)))
8584, 30syl6bb 279 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ 𝑦𝐵))
86 simpllr 763 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎)
8786eleq1d 2844 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐵𝑎𝐵))
88 simplr 756 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎)
8988eleq1d 2844 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤𝐵𝑎𝐵))
9087, 89anbi12d 621 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑎𝐵𝑎𝐵)))
91 anidm 557 . . . . . . . . . . . . . . . . 17 ((𝑎𝐵𝑎𝐵) ↔ 𝑎𝐵)
9290, 91syl6bb 279 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑎𝐵))
9382oveq1d 6985 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦))
9493eleq2d 2845 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦)))
95 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟)
9686oveq2d 6986 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎))
9795, 96eleq12d 2854 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
9886, 88oveq12d 6988 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎))
9998eleq2d 2845 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎)))
10094, 97, 993anbi123d 1415 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))
10185, 92, 1003anbi123d 1415 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
10221, 101syl5bb 275 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
103102anbi2d 619 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))))
10486oveq2d 6986 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (⟨𝑦, 𝑦· 𝑧) = (⟨𝑦, 𝑦· 𝑎))
105 eqidd 2773 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 )
106104, 95, 105oveq123d 6991 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ))
107106, 95eqeq12d 2787 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔 ↔ (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
108103, 107imbi12d 337 . . . . . . . . . . . 12 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
109108sbiedv 2470 . . . . . . . . . . 11 (((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
110109sbiedv 2470 . . . . . . . . . 10 ((𝑥 = 𝑦𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
111110sbiedv 2470 . . . . . . . . 9 (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
112 iscatd2.3 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
113112sbt 2017 . . . . . . . . . . 11 [𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
114113sbt 2017 . . . . . . . . . 10 [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
115114sbt 2017 . . . . . . . . 9 [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
116111, 115chvarv 2327 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
11775, 76, 77, 81, 116syl13anc 1352 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
118117ex 405 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
119118exlimdvv 1893 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12074, 119syl5bir 235 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12164, 73, 120mp2and 686 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
122 id 22 . . . . . . . 8 (𝑦 = 𝑧𝑦 = 𝑧)
123122, 122oveq12d 6988 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧))
124123neeq1d 3020 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅))
125683ad2ant1 1113 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
126 simp23 1188 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧𝐵)
127124, 125, 126rspcdva 3535 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅)
128 n0 4190 . . . . 5 ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
129127, 128sylib 210 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
130 eleq1w 2842 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
1311303anbi1d 1419 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ (𝑦𝐵𝑎𝐵𝑧𝐵)))
132 oveq1 6977 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎))
133132eleq2d 2845 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
134133anbi1d 620 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))))
135134anbi1d 620 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
136131, 135anbi12d 621 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
137136anbi2d 619 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
138 opeq1 4671 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ⟨𝑥, 𝑎⟩ = ⟨𝑦, 𝑎⟩)
139138oveq1d 6985 . . . . . . . . . . 11 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑧) = (⟨𝑦, 𝑎· 𝑧))
140139oveqd 6987 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) = (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))
141 oveq1 6977 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧))
142140, 141eleq12d 2854 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
143137, 142imbi12d 337 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))
144 df-3an 1070 . . . . . . . . . . . . . . 15 (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
14521, 144bitri 267 . . . . . . . . . . . . . 14 (𝜓 ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
146 simpll 754 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
147146eleq1d 2844 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
148147anbi2d 619 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
149 simplr 756 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧)
150149eleq1d 2844 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑧𝐵))
151150anbi2d 619 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑧𝐵𝑧𝐵)))
152 anidm 557 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑧𝐵) ↔ 𝑧𝐵)
153151, 152syl6bb 279 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑧𝐵))
154148, 153anbi12d 621 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵)))
155 df-3an 1070 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵))
156154, 155syl6bbr 281 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ (𝑥𝐵𝑎𝐵𝑧𝐵)))
157 simpr 477 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
158146oveq2d 6986 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
159157, 158eleq12d 2854 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
160146oveq1d 6985 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
161160eleq2d 2845 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
162149oveq2d 6986 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧))
163162eleq2d 2845 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧)))
164159, 161, 1633anbi123d 1415 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
165 df-3an 1070 . . . . . . . . . . . . . . . 16 ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))
166164, 165syl6bb 279 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
167156, 166anbi12d 621 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
168145, 167syl5bb 275 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
169168anbi2d 619 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
170146opeq2d 4678 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
171170oveq1d 6985 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
172 eqidd 2773 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
173171, 172, 157oveq123d 6991 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
174173eleq1d 2844 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))
175169, 174imbi12d 337 . . . . . . . . . . 11 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
176175sbiedv 2470 . . . . . . . . . 10 ((𝑦 = 𝑎𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
177176sbiedv 2470 . . . . . . . . 9 (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
178 iscatd2.4 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
179178sbt 2017 . . . . . . . . . 10 [𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
180179sbt 2017 . . . . . . . . 9 [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
181177, 180chvarv 2327 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))
182143, 181chvarv 2327 . . . . . . 7 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
183182exp45 431 . . . . . 6 (𝜑 → ((𝑦𝐵𝑎𝐵𝑧𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))))
1841833imp 1091 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
185184exlimdv 1892 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
186129, 185mpd 15 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
187130anbi1d 620 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵) ↔ (𝑦𝐵𝑎𝐵)))
188187anbi1d 620 . . . . . 6 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵))))
1891333anbi1d 1419 . . . . . 6 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
190188, 1893anbi23d 1418 . . . . 5 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
191138oveq1d 6985 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑤) = (⟨𝑦, 𝑎· 𝑤))
192191oveqd 6987 . . . . . 6 (𝑥 = 𝑦 → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟))
193 opeq1 4671 . . . . . . . 8 (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
194193oveq1d 6985 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑧· 𝑤) = (⟨𝑦, 𝑧· 𝑤))
195 eqidd 2773 . . . . . . 7 (𝑥 = 𝑦𝑘 = 𝑘)
196194, 195, 140oveq123d 6991 . . . . . 6 (𝑥 = 𝑦 → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
197192, 196eqeq12d 2787 . . . . 5 (𝑥 = 𝑦 → (((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))))
198190, 197imbi12d 337 . . . 4 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))))
199 simpl 475 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑦 = 𝑎)
200199eleq1d 2844 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
201200anbi2d 619 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
202 simpr 477 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑓 = 𝑟)
203199oveq2d 6986 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
204202, 203eleq12d 2854 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
205199oveq1d 6985 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
206205eleq2d 2845 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
207204, 2063anbi12d 1416 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
208201, 2073anbi13d 1417 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
20921, 208syl5bb 275 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
210 df-3an 1070 . . . . . . . . . 10 (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
211209, 210syl6bb 279 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
212211anbi2d 619 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))))
213 3anass 1076 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
214212, 213syl6bbr 281 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
215199opeq2d 4678 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
216215oveq1d 6985 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑤) = (⟨𝑥, 𝑎· 𝑤))
217199opeq1d 4677 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑦, 𝑧⟩ = ⟨𝑎, 𝑧⟩)
218217oveq1d 6985 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑦, 𝑧· 𝑤) = (⟨𝑎, 𝑧· 𝑤))
219218oveqd 6987 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔) = (𝑘(⟨𝑎, 𝑧· 𝑤)𝑔))
220216, 219, 202oveq123d 6991 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟))
221215oveq1d 6985 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
222 eqidd 2773 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑔 = 𝑔)
223221, 222, 202oveq123d 6991 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
224223oveq2d 6986 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
225220, 224eqeq12d 2787 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))))
226214, 225imbi12d 337 . . . . . 6 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
227226sbiedv 2470 . . . . 5 (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
228 iscatd2.5 . . . . . 6 ((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
229228sbt 2017 . . . . 5 [𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
230227, 229chvarv 2327 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
231198, 230chvarv 2327 . . 3 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
2321, 2, 3, 4, 5, 61, 121, 186, 231iscatd 16796 . 2 (𝜑𝐶 ∈ Cat)
2331, 2, 3, 232, 5, 61, 121catidd 16803 . 2 (𝜑 → (Id‘𝐶) = (𝑦𝐵1 ))
234232, 233jca 504 1 (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦𝐵1 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wex 1742  [wsb 2015  wcel 2050  wne 2961  wral 3082  c0 4172  cop 4441  cmpt 5002  cfv 6182  (class class class)co 6970  Basecbs 16333  Hom chom 16426  compcco 16427  Catccat 16787  Idccid 16788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pr 5180
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-cat 16791  df-cid 16792
This theorem is referenced by:  oppccatid  16841  subccatid  16968  fuccatid  17091  setccatid  17196  catccatid  17214  estrccatid  17234  xpccatid  17290  rngccatidALTV  43624  ringccatidALTV  43687
  Copyright terms: Public domain W3C validator