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

Theorem iscatd2 16323
Description: Version of iscatd 16315 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 3913 . . . . . . 7 ( 1 ∈ (𝑦𝐻𝑦) → (𝑦𝐻𝑦) ≠ ∅)
75, 6syl 17 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝐻𝑦) ≠ ∅)
873ad2antr1 1224 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅)
9 n0 3923 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
108, 9sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
11 n0 3923 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
128, 11sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
13 eeanv 2180 . . . . 5 (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)))
14 simpll 789 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑)
15 simplr2 1102 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎𝐵)
16 simplr1 1101 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦𝐵)
1715, 16jca 554 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎𝐵𝑦𝐵))
18 simplr3 1103 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦))
19 simprl 793 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦))
20 simprr 795 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦))
2118, 19, 203jca 1240 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))
22 iscatd2.ps . . . . . . . . . . . . . . 15 (𝜓 ↔ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
23 simplll 797 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎)
2423eleq1d 2684 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐵𝑎𝐵))
2524anbi1d 740 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑎𝐵𝑦𝐵)))
26 simpllr 798 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦)
2726eleq1d 2684 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐵𝑦𝐵))
28 simplr 791 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦)
2928eleq1d 2684 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑦𝐵))
3027, 29anbi12d 746 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑦𝐵𝑦𝐵)))
31 anidm 675 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝐵) ↔ 𝑦𝐵)
3230, 31syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑦𝐵))
33 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
3423oveq1d 6650 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦))
3533, 34eleq12d 2693 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦)))
3626oveq2d 6651 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦))
3736eleq2d 2685 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦)))
3826, 28oveq12d 6653 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦))
3938eleq2d 2685 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦)))
4035, 37, 393anbi123d 1397 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))
4125, 32, 403anbi123d 1397 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4222, 41syl5bb 272 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4342anbi2d 739 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))))
4423opeq1d 4399 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑦⟩)
4544oveq1d 6650 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑦) = (⟨𝑎, 𝑦· 𝑦))
46 eqidd 2621 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 )
4745, 46, 33oveq123d 6656 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟))
4847, 33eqeq12d 2635 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓 ↔ ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
4943, 48imbi12d 334 . . . . . . . . . . . 12 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5049sbiedv 2408 . . . . . . . . . . 11 (((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5150sbiedv 2408 . . . . . . . . . 10 ((𝑥 = 𝑎𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5251sbiedv 2408 . . . . . . . . 9 (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
53 iscatd2.2 . . . . . . . . . . . 12 ((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5453sbt 2417 . . . . . . . . . . 11 [𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5554sbt 2417 . . . . . . . . . 10 [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5655sbt 2417 . . . . . . . . 9 [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5752, 56chvarv 2261 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5814, 17, 16, 21, 57syl13anc 1326 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5958ex 450 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6059exlimdvv 1860 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6113, 60syl5bir 233 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6210, 12, 61mp2and 714 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
6373ad2antr1 1224 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅)
64 n0 3923 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
6563, 64sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
66 simpr2 1066 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎𝐵)
677ralrimiva 2963 . . . . . . 7 (𝜑 → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
6867adantr 481 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
69 id 22 . . . . . . . . 9 (𝑦 = 𝑎𝑦 = 𝑎)
7069, 69oveq12d 6653 . . . . . . . 8 (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎))
7170neeq1d 2850 . . . . . . 7 (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅))
7271rspcv 3300 . . . . . 6 (𝑎𝐵 → (∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅ → (𝑎𝐻𝑎) ≠ ∅))
7366, 68, 72sylc 65 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅)
74 n0 3923 . . . . 5 ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
7573, 74sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
76 eeanv 2180 . . . . 5 (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)))
77 simpll 789 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑)
78 simplr1 1101 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦𝐵)
79 simplr2 1102 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎𝐵)
80 simprl 793 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦))
81 simplr3 1103 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎))
82 simprr 795 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎))
8380, 81, 823jca 1240 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))
84 simplll 797 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦)
8584eleq1d 2684 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐵𝑦𝐵))
8685anbi1d 740 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑦𝐵𝑦𝐵)))
8786, 31syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ 𝑦𝐵))
88 simpllr 798 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎)
8988eleq1d 2684 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐵𝑎𝐵))
90 simplr 791 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎)
9190eleq1d 2684 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤𝐵𝑎𝐵))
9289, 91anbi12d 746 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑎𝐵𝑎𝐵)))
93 anidm 675 . . . . . . . . . . . . . . . . 17 ((𝑎𝐵𝑎𝐵) ↔ 𝑎𝐵)
9492, 93syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑎𝐵))
9584oveq1d 6650 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦))
9695eleq2d 2685 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦)))
97 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟)
9888oveq2d 6651 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎))
9997, 98eleq12d 2693 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
10088, 90oveq12d 6653 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎))
101100eleq2d 2685 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎)))
10296, 99, 1013anbi123d 1397 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))
10387, 94, 1023anbi123d 1397 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
10422, 103syl5bb 272 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
105104anbi2d 739 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))))
10688oveq2d 6651 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (⟨𝑦, 𝑦· 𝑧) = (⟨𝑦, 𝑦· 𝑎))
107 eqidd 2621 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 )
108106, 97, 107oveq123d 6656 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ))
109108, 97eqeq12d 2635 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔 ↔ (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
110105, 109imbi12d 334 . . . . . . . . . . . 12 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
111110sbiedv 2408 . . . . . . . . . . 11 (((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
112111sbiedv 2408 . . . . . . . . . 10 ((𝑥 = 𝑦𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
113112sbiedv 2408 . . . . . . . . 9 (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
114 iscatd2.3 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
115114sbt 2417 . . . . . . . . . . 11 [𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
116115sbt 2417 . . . . . . . . . 10 [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
117116sbt 2417 . . . . . . . . 9 [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
118113, 117chvarv 2261 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
11977, 78, 79, 83, 118syl13anc 1326 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
120119ex 450 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
121120exlimdvv 1860 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12276, 121syl5bir 233 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12365, 75, 122mp2and 714 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
124673ad2ant1 1080 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
125 simp23 1094 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧𝐵)
126 id 22 . . . . . . . . 9 (𝑦 = 𝑧𝑦 = 𝑧)
127126, 126oveq12d 6653 . . . . . . . 8 (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧))
128127neeq1d 2850 . . . . . . 7 (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅))
129128rspccva 3303 . . . . . 6 ((∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅ ∧ 𝑧𝐵) → (𝑧𝐻𝑧) ≠ ∅)
130124, 125, 129syl2anc 692 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅)
131 n0 3923 . . . . 5 ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
132130, 131sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
133 eleq1 2687 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
1341333anbi1d 1401 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ (𝑦𝐵𝑎𝐵𝑧𝐵)))
135 oveq1 6642 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎))
136135eleq2d 2685 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
137136anbi1d 740 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))))
138137anbi1d 740 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
139134, 138anbi12d 746 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
140139anbi2d 739 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
141 opeq1 4393 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ⟨𝑥, 𝑎⟩ = ⟨𝑦, 𝑎⟩)
142141oveq1d 6650 . . . . . . . . . . 11 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑧) = (⟨𝑦, 𝑎· 𝑧))
143142oveqd 6652 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) = (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))
144 oveq1 6642 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧))
145143, 144eleq12d 2693 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
146140, 145imbi12d 334 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))
147 df-3an 1038 . . . . . . . . . . . . . . 15 (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
14822, 147bitri 264 . . . . . . . . . . . . . 14 (𝜓 ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
149 simpll 789 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
150149eleq1d 2684 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
151150anbi2d 739 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
152 simplr 791 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧)
153152eleq1d 2684 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑧𝐵))
154153anbi2d 739 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑧𝐵𝑧𝐵)))
155 anidm 675 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑧𝐵) ↔ 𝑧𝐵)
156154, 155syl6bb 276 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑧𝐵))
157151, 156anbi12d 746 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵)))
158 df-3an 1038 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵))
159157, 158syl6bbr 278 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ (𝑥𝐵𝑎𝐵𝑧𝐵)))
160 simpr 477 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
161149oveq2d 6651 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
162160, 161eleq12d 2693 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
163149oveq1d 6650 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
164163eleq2d 2685 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
165152oveq2d 6651 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧))
166165eleq2d 2685 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧)))
167162, 164, 1663anbi123d 1397 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
168 df-3an 1038 . . . . . . . . . . . . . . . 16 ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))
169167, 168syl6bb 276 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
170159, 169anbi12d 746 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
171148, 170syl5bb 272 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
172171anbi2d 739 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
173149opeq2d 4400 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
174173oveq1d 6650 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
175 eqidd 2621 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
176174, 175, 160oveq123d 6656 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
177176eleq1d 2684 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))
178172, 177imbi12d 334 . . . . . . . . . . 11 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
179178sbiedv 2408 . . . . . . . . . 10 ((𝑦 = 𝑎𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
180179sbiedv 2408 . . . . . . . . 9 (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
181 iscatd2.4 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
182181sbt 2417 . . . . . . . . . 10 [𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
183182sbt 2417 . . . . . . . . 9 [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
184180, 183chvarv 2261 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))
185146, 184chvarv 2261 . . . . . . 7 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
186185exp45 641 . . . . . 6 (𝜑 → ((𝑦𝐵𝑎𝐵𝑧𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))))
1871863imp 1254 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
188187exlimdv 1859 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
189132, 188mpd 15 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
190133anbi1d 740 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵) ↔ (𝑦𝐵𝑎𝐵)))
191190anbi1d 740 . . . . . 6 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵))))
1921363anbi1d 1401 . . . . . 6 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
193191, 1923anbi23d 1400 . . . . 5 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
194141oveq1d 6650 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑤) = (⟨𝑦, 𝑎· 𝑤))
195194oveqd 6652 . . . . . 6 (𝑥 = 𝑦 → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟))
196 opeq1 4393 . . . . . . . 8 (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
197196oveq1d 6650 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑧· 𝑤) = (⟨𝑦, 𝑧· 𝑤))
198 eqidd 2621 . . . . . . 7 (𝑥 = 𝑦𝑘 = 𝑘)
199197, 198, 143oveq123d 6656 . . . . . 6 (𝑥 = 𝑦 → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
200195, 199eqeq12d 2635 . . . . 5 (𝑥 = 𝑦 → (((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))))
201193, 200imbi12d 334 . . . 4 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))))
202 simpl 473 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑦 = 𝑎)
203202eleq1d 2684 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
204203anbi2d 739 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
205 simpr 477 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑓 = 𝑟)
206202oveq2d 6651 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
207205, 206eleq12d 2693 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
208202oveq1d 6650 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
209208eleq2d 2685 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
210207, 2093anbi12d 1398 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
211204, 2103anbi13d 1399 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
21222, 211syl5bb 272 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
213 df-3an 1038 . . . . . . . . . 10 (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
214212, 213syl6bb 276 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
215214anbi2d 739 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))))
216 3anass 1040 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
217215, 216syl6bbr 278 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
218202opeq2d 4400 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
219218oveq1d 6650 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑤) = (⟨𝑥, 𝑎· 𝑤))
220202opeq1d 4399 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑦, 𝑧⟩ = ⟨𝑎, 𝑧⟩)
221220oveq1d 6650 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑦, 𝑧· 𝑤) = (⟨𝑎, 𝑧· 𝑤))
222221oveqd 6652 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔) = (𝑘(⟨𝑎, 𝑧· 𝑤)𝑔))
223219, 222, 205oveq123d 6656 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟))
224218oveq1d 6650 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
225 eqidd 2621 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑔 = 𝑔)
226224, 225, 205oveq123d 6656 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
227226oveq2d 6651 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
228223, 227eqeq12d 2635 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))))
229217, 228imbi12d 334 . . . . . 6 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
230229sbiedv 2408 . . . . 5 (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
231 iscatd2.5 . . . . . 6 ((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
232231sbt 2417 . . . . 5 [𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
233230, 232chvarv 2261 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
234201, 233chvarv 2261 . . 3 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
2351, 2, 3, 4, 5, 62, 123, 189, 234iscatd 16315 . 2 (𝜑𝐶 ∈ Cat)
2361, 2, 3, 235, 5, 62, 123catidd 16322 . 2 (𝜑 → (Id‘𝐶) = (𝑦𝐵1 ))
237235, 236jca 554 1 (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦𝐵1 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wex 1702  [wsb 1878  wcel 1988  wne 2791  wral 2909  c0 3907  cop 4174  cmpt 4720  cfv 5876  (class class class)co 6635  Basecbs 15838  Hom chom 15933  compcco 15934  Catccat 16306  Idccid 16307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-cat 16310  df-cid 16311
This theorem is referenced by:  oppccatid  16360  subccatid  16487  fuccatid  16610  setccatid  16715  catccatid  16733  estrccatid  16753  xpccatid  16809  rngccatidALTV  41754  ringccatidALTV  41817
  Copyright terms: Public domain W3C validator