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

Theorem iscatd2 16548
Description: Version of iscatd 16540 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 ∈ (𝑦𝐻𝑦))
6 ne0i 4067 . . . . . . 7 ( 1 ∈ (𝑦𝐻𝑦) → (𝑦𝐻𝑦) ≠ ∅)
75, 6syl 17 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝐻𝑦) ≠ ∅)
873ad2antr1 1202 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅)
9 n0 4076 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
108, 9sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
11 n0 4076 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
128, 11sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
13 eeanv 2343 . . . . 5 (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)))
14 simpll 742 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑)
15 simplr2 1261 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎𝐵)
16 simplr1 1259 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦𝐵)
1715, 16jca 495 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎𝐵𝑦𝐵))
18 simplr3 1263 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦))
19 simprl 746 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦))
20 simprr 748 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦))
2118, 19, 203jca 1121 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))
22 iscatd2.ps . . . . . . . . . . . . . . 15 (𝜓 ↔ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
23 simplll 750 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎)
2423eleq1d 2834 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐵𝑎𝐵))
2524anbi1d 607 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑎𝐵𝑦𝐵)))
26 simpllr 752 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦)
2726eleq1d 2834 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐵𝑦𝐵))
28 simplr 744 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦)
2928eleq1d 2834 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑦𝐵))
3027, 29anbi12d 608 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑦𝐵𝑦𝐵)))
31 anidm 546 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝐵) ↔ 𝑦𝐵)
3230, 31syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑦𝐵))
33 simpr 471 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
3423oveq1d 6807 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦))
3533, 34eleq12d 2843 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦)))
3626oveq2d 6808 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦))
3736eleq2d 2835 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦)))
3826, 28oveq12d 6810 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦))
3938eleq2d 2835 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦)))
4035, 37, 393anbi123d 1546 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))
4125, 32, 403anbi123d 1546 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4222, 41syl5bb 272 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4342anbi2d 606 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))))
4423opeq1d 4543 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑦⟩)
4544oveq1d 6807 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑦) = (⟨𝑎, 𝑦· 𝑦))
46 eqidd 2771 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 )
4745, 46, 33oveq123d 6813 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟))
4847, 33eqeq12d 2785 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓 ↔ ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
4943, 48imbi12d 333 . . . . . . . . . . . 12 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5049sbiedv 2556 . . . . . . . . . . 11 (((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5150sbiedv 2556 . . . . . . . . . 10 ((𝑥 = 𝑎𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5251sbiedv 2556 . . . . . . . . 9 (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
53 iscatd2.2 . . . . . . . . . . . 12 ((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5453sbt 2565 . . . . . . . . . . 11 [𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5554sbt 2565 . . . . . . . . . 10 [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5655sbt 2565 . . . . . . . . 9 [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5752, 56chvarv 2424 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5814, 17, 16, 21, 57syl13anc 1477 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5958ex 397 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6059exlimdvv 2013 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6113, 60syl5bir 233 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6210, 12, 61mp2and 671 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
6373ad2antr1 1202 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅)
64 n0 4076 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
6563, 64sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
66 id 22 . . . . . . . 8 (𝑦 = 𝑎𝑦 = 𝑎)
6766, 66oveq12d 6810 . . . . . . 7 (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎))
6867neeq1d 3001 . . . . . 6 (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅))
697ralrimiva 3114 . . . . . . 7 (𝜑 → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
7069adantr 466 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
71 simpr2 1234 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎𝐵)
7268, 70, 71rspcdva 3464 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅)
73 n0 4076 . . . . 5 ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
7472, 73sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
75 eeanv 2343 . . . . 5 (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)))
76 simpll 742 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑)
77 simplr1 1259 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦𝐵)
78 simplr2 1261 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎𝐵)
79 simprl 746 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦))
80 simplr3 1263 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎))
81 simprr 748 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎))
8279, 80, 813jca 1121 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))
83 simplll 750 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦)
8483eleq1d 2834 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐵𝑦𝐵))
8584anbi1d 607 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑦𝐵𝑦𝐵)))
8685, 31syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ 𝑦𝐵))
87 simpllr 752 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎)
8887eleq1d 2834 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐵𝑎𝐵))
89 simplr 744 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎)
9089eleq1d 2834 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤𝐵𝑎𝐵))
9188, 90anbi12d 608 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑎𝐵𝑎𝐵)))
92 anidm 546 . . . . . . . . . . . . . . . . 17 ((𝑎𝐵𝑎𝐵) ↔ 𝑎𝐵)
9391, 92syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑎𝐵))
9483oveq1d 6807 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦))
9594eleq2d 2835 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦)))
96 simpr 471 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟)
9787oveq2d 6808 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎))
9896, 97eleq12d 2843 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
9987, 89oveq12d 6810 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎))
10099eleq2d 2835 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎)))
10195, 98, 1003anbi123d 1546 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))
10286, 93, 1013anbi123d 1546 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
10322, 102syl5bb 272 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
104103anbi2d 606 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))))
10587oveq2d 6808 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (⟨𝑦, 𝑦· 𝑧) = (⟨𝑦, 𝑦· 𝑎))
106 eqidd 2771 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 )
107105, 96, 106oveq123d 6813 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ))
108107, 96eqeq12d 2785 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔 ↔ (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
109104, 108imbi12d 333 . . . . . . . . . . . 12 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
110109sbiedv 2556 . . . . . . . . . . 11 (((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
111110sbiedv 2556 . . . . . . . . . 10 ((𝑥 = 𝑦𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
112111sbiedv 2556 . . . . . . . . 9 (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
113 iscatd2.3 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
114113sbt 2565 . . . . . . . . . . 11 [𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
115114sbt 2565 . . . . . . . . . 10 [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
116115sbt 2565 . . . . . . . . 9 [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
117112, 116chvarv 2424 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
11876, 77, 78, 82, 117syl13anc 1477 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
119118ex 397 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
120119exlimdvv 2013 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12175, 120syl5bir 233 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12265, 74, 121mp2and 671 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
123 id 22 . . . . . . . 8 (𝑦 = 𝑧𝑦 = 𝑧)
124123, 123oveq12d 6810 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧))
125124neeq1d 3001 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅))
126693ad2ant1 1126 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
127 simp23 1249 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧𝐵)
128125, 126, 127rspcdva 3464 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅)
129 n0 4076 . . . . 5 ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
130128, 129sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
131 eleq1w 2832 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
1321313anbi1d 1550 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ (𝑦𝐵𝑎𝐵𝑧𝐵)))
133 oveq1 6799 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎))
134133eleq2d 2835 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
135134anbi1d 607 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))))
136135anbi1d 607 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
137132, 136anbi12d 608 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
138137anbi2d 606 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
139 opeq1 4537 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ⟨𝑥, 𝑎⟩ = ⟨𝑦, 𝑎⟩)
140139oveq1d 6807 . . . . . . . . . . 11 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑧) = (⟨𝑦, 𝑎· 𝑧))
141140oveqd 6809 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) = (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))
142 oveq1 6799 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧))
143141, 142eleq12d 2843 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
144138, 143imbi12d 333 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))
145 df-3an 1072 . . . . . . . . . . . . . . 15 (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
14622, 145bitri 264 . . . . . . . . . . . . . 14 (𝜓 ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
147 simpll 742 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
148147eleq1d 2834 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
149148anbi2d 606 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
150 simplr 744 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧)
151150eleq1d 2834 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑧𝐵))
152151anbi2d 606 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑧𝐵𝑧𝐵)))
153 anidm 546 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑧𝐵) ↔ 𝑧𝐵)
154152, 153syl6bb 276 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑧𝐵))
155149, 154anbi12d 608 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵)))
156 df-3an 1072 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵))
157155, 156syl6bbr 278 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ (𝑥𝐵𝑎𝐵𝑧𝐵)))
158 simpr 471 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
159147oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
160158, 159eleq12d 2843 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
161147oveq1d 6807 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
162161eleq2d 2835 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
163150oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧))
164163eleq2d 2835 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧)))
165160, 162, 1643anbi123d 1546 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
166 df-3an 1072 . . . . . . . . . . . . . . . 16 ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))
167165, 166syl6bb 276 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
168157, 167anbi12d 608 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
169146, 168syl5bb 272 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
170169anbi2d 606 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
171147opeq2d 4544 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
172171oveq1d 6807 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
173 eqidd 2771 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
174172, 173, 158oveq123d 6813 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
175174eleq1d 2834 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))
176170, 175imbi12d 333 . . . . . . . . . . 11 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
177176sbiedv 2556 . . . . . . . . . 10 ((𝑦 = 𝑎𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
178177sbiedv 2556 . . . . . . . . 9 (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
179 iscatd2.4 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
180179sbt 2565 . . . . . . . . . 10 [𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
181180sbt 2565 . . . . . . . . 9 [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
182178, 181chvarv 2424 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))
183144, 182chvarv 2424 . . . . . . 7 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
184183exp45 425 . . . . . 6 (𝜑 → ((𝑦𝐵𝑎𝐵𝑧𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))))
1851843imp 1100 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
186185exlimdv 2012 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
187130, 186mpd 15 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
188131anbi1d 607 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵) ↔ (𝑦𝐵𝑎𝐵)))
189188anbi1d 607 . . . . . 6 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵))))
1901343anbi1d 1550 . . . . . 6 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
191189, 1903anbi23d 1549 . . . . 5 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
192139oveq1d 6807 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑤) = (⟨𝑦, 𝑎· 𝑤))
193192oveqd 6809 . . . . . 6 (𝑥 = 𝑦 → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟))
194 opeq1 4537 . . . . . . . 8 (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
195194oveq1d 6807 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑧· 𝑤) = (⟨𝑦, 𝑧· 𝑤))
196 eqidd 2771 . . . . . . 7 (𝑥 = 𝑦𝑘 = 𝑘)
197195, 196, 141oveq123d 6813 . . . . . 6 (𝑥 = 𝑦 → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
198193, 197eqeq12d 2785 . . . . 5 (𝑥 = 𝑦 → (((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))))
199191, 198imbi12d 333 . . . 4 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))))
200 simpl 468 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑦 = 𝑎)
201200eleq1d 2834 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
202201anbi2d 606 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
203 simpr 471 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑓 = 𝑟)
204200oveq2d 6808 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
205203, 204eleq12d 2843 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
206200oveq1d 6807 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
207206eleq2d 2835 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
208205, 2073anbi12d 1547 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
209202, 2083anbi13d 1548 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
21022, 209syl5bb 272 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
211 df-3an 1072 . . . . . . . . . 10 (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
212210, 211syl6bb 276 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
213212anbi2d 606 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))))
214 3anass 1079 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
215213, 214syl6bbr 278 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
216200opeq2d 4544 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
217216oveq1d 6807 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑤) = (⟨𝑥, 𝑎· 𝑤))
218200opeq1d 4543 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑦, 𝑧⟩ = ⟨𝑎, 𝑧⟩)
219218oveq1d 6807 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑦, 𝑧· 𝑤) = (⟨𝑎, 𝑧· 𝑤))
220219oveqd 6809 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔) = (𝑘(⟨𝑎, 𝑧· 𝑤)𝑔))
221217, 220, 203oveq123d 6813 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟))
222216oveq1d 6807 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
223 eqidd 2771 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑔 = 𝑔)
224222, 223, 203oveq123d 6813 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
225224oveq2d 6808 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
226221, 225eqeq12d 2785 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))))
227215, 226imbi12d 333 . . . . . 6 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
228227sbiedv 2556 . . . . 5 (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
229 iscatd2.5 . . . . . 6 ((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
230229sbt 2565 . . . . 5 [𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
231228, 230chvarv 2424 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
232199, 231chvarv 2424 . . 3 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
2331, 2, 3, 4, 5, 62, 122, 187, 232iscatd 16540 . 2 (𝜑𝐶 ∈ Cat)
2341, 2, 3, 233, 5, 62, 122catidd 16547 . 2 (𝜑 → (Id‘𝐶) = (𝑦𝐵1 ))
235233, 234jca 495 1 (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦𝐵1 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1070   = wceq 1630  wex 1851  [wsb 2048  wcel 2144  wne 2942  wral 3060  c0 4061  cop 4320  cmpt 4861  cfv 6031  (class class class)co 6792  Basecbs 16063  Hom chom 16159  compcco 16160  Catccat 16531  Idccid 16532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-cat 16535  df-cid 16536
This theorem is referenced by:  oppccatid  16585  subccatid  16712  fuccatid  16835  setccatid  16940  catccatid  16958  estrccatid  16978  xpccatid  17035  rngccatidALTV  42507  ringccatidALTV  42570
  Copyright terms: Public domain W3C validator