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

Theorem iscatd2 16389
Description: Version of iscatd 16381 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 3954 . . . . . . 7 ( 1 ∈ (𝑦𝐻𝑦) → (𝑦𝐻𝑦) ≠ ∅)
75, 6syl 17 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝐻𝑦) ≠ ∅)
873ad2antr1 1246 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅)
9 n0 3964 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
108, 9sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
11 n0 3964 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
128, 11sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
13 eeanv 2218 . . . . 5 (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)))
14 simpll 805 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑)
15 simplr2 1124 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎𝐵)
16 simplr1 1123 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦𝐵)
1715, 16jca 553 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎𝐵𝑦𝐵))
18 simplr3 1125 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦))
19 simprl 809 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦))
20 simprr 811 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦))
2118, 19, 203jca 1261 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))
22 iscatd2.ps . . . . . . . . . . . . . . 15 (𝜓 ↔ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
23 simplll 813 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎)
2423eleq1d 2715 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐵𝑎𝐵))
2524anbi1d 741 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑎𝐵𝑦𝐵)))
26 simpllr 815 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦)
2726eleq1d 2715 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐵𝑦𝐵))
28 simplr 807 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦)
2928eleq1d 2715 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑦𝐵))
3027, 29anbi12d 747 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑦𝐵𝑦𝐵)))
31 anidm 677 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝐵) ↔ 𝑦𝐵)
3230, 31syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑦𝐵))
33 simpr 476 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
3423oveq1d 6705 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦))
3533, 34eleq12d 2724 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦)))
3626oveq2d 6706 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦))
3736eleq2d 2716 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦)))
3826, 28oveq12d 6708 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦))
3938eleq2d 2716 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦)))
4035, 37, 393anbi123d 1439 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))
4125, 32, 403anbi123d 1439 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4222, 41syl5bb 272 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4342anbi2d 740 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))))
4423opeq1d 4439 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑦⟩)
4544oveq1d 6705 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑦) = (⟨𝑎, 𝑦· 𝑦))
46 eqidd 2652 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 )
4745, 46, 33oveq123d 6711 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟))
4847, 33eqeq12d 2666 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓 ↔ ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
4943, 48imbi12d 333 . . . . . . . . . . . 12 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5049sbiedv 2438 . . . . . . . . . . 11 (((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5150sbiedv 2438 . . . . . . . . . 10 ((𝑥 = 𝑎𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5251sbiedv 2438 . . . . . . . . 9 (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
53 iscatd2.2 . . . . . . . . . . . 12 ((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5453sbt 2447 . . . . . . . . . . 11 [𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5554sbt 2447 . . . . . . . . . 10 [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5655sbt 2447 . . . . . . . . 9 [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5752, 56chvarv 2299 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5814, 17, 16, 21, 57syl13anc 1368 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5958ex 449 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6059exlimdvv 1902 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6113, 60syl5bir 233 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6210, 12, 61mp2and 715 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
6373ad2antr1 1246 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅)
64 n0 3964 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
6563, 64sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
66 simpr2 1088 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎𝐵)
677ralrimiva 2995 . . . . . . 7 (𝜑 → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
6867adantr 480 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
69 id 22 . . . . . . . . 9 (𝑦 = 𝑎𝑦 = 𝑎)
7069, 69oveq12d 6708 . . . . . . . 8 (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎))
7170neeq1d 2882 . . . . . . 7 (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅))
7271rspcv 3336 . . . . . 6 (𝑎𝐵 → (∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅ → (𝑎𝐻𝑎) ≠ ∅))
7366, 68, 72sylc 65 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅)
74 n0 3964 . . . . 5 ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
7573, 74sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
76 eeanv 2218 . . . . 5 (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)))
77 simpll 805 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑)
78 simplr1 1123 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦𝐵)
79 simplr2 1124 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎𝐵)
80 simprl 809 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦))
81 simplr3 1125 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎))
82 simprr 811 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎))
8380, 81, 823jca 1261 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))
84 simplll 813 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦)
8584eleq1d 2715 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐵𝑦𝐵))
8685anbi1d 741 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑦𝐵𝑦𝐵)))
8786, 31syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ 𝑦𝐵))
88 simpllr 815 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎)
8988eleq1d 2715 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐵𝑎𝐵))
90 simplr 807 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎)
9190eleq1d 2715 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤𝐵𝑎𝐵))
9289, 91anbi12d 747 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑎𝐵𝑎𝐵)))
93 anidm 677 . . . . . . . . . . . . . . . . 17 ((𝑎𝐵𝑎𝐵) ↔ 𝑎𝐵)
9492, 93syl6bb 276 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑎𝐵))
9584oveq1d 6705 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦))
9695eleq2d 2716 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦)))
97 simpr 476 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟)
9888oveq2d 6706 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎))
9997, 98eleq12d 2724 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
10088, 90oveq12d 6708 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎))
101100eleq2d 2716 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎)))
10296, 99, 1013anbi123d 1439 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))
10387, 94, 1023anbi123d 1439 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
10422, 103syl5bb 272 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
105104anbi2d 740 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))))
10688oveq2d 6706 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (⟨𝑦, 𝑦· 𝑧) = (⟨𝑦, 𝑦· 𝑎))
107 eqidd 2652 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 )
108106, 97, 107oveq123d 6711 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ))
109108, 97eqeq12d 2666 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔 ↔ (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
110105, 109imbi12d 333 . . . . . . . . . . . 12 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
111110sbiedv 2438 . . . . . . . . . . 11 (((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
112111sbiedv 2438 . . . . . . . . . 10 ((𝑥 = 𝑦𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
113112sbiedv 2438 . . . . . . . . 9 (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
114 iscatd2.3 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
115114sbt 2447 . . . . . . . . . . 11 [𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
116115sbt 2447 . . . . . . . . . 10 [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
117116sbt 2447 . . . . . . . . 9 [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
118113, 117chvarv 2299 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
11977, 78, 79, 83, 118syl13anc 1368 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
120119ex 449 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
121120exlimdvv 1902 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12276, 121syl5bir 233 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12365, 75, 122mp2and 715 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
124673ad2ant1 1102 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
125 simp23 1116 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧𝐵)
126 id 22 . . . . . . . . 9 (𝑦 = 𝑧𝑦 = 𝑧)
127126, 126oveq12d 6708 . . . . . . . 8 (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧))
128127neeq1d 2882 . . . . . . 7 (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅))
129128rspccva 3339 . . . . . 6 ((∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅ ∧ 𝑧𝐵) → (𝑧𝐻𝑧) ≠ ∅)
130124, 125, 129syl2anc 694 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅)
131 n0 3964 . . . . 5 ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
132130, 131sylib 208 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
133 eleq1 2718 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
1341333anbi1d 1443 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ (𝑦𝐵𝑎𝐵𝑧𝐵)))
135 oveq1 6697 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎))
136135eleq2d 2716 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
137136anbi1d 741 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))))
138137anbi1d 741 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
139134, 138anbi12d 747 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
140139anbi2d 740 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
141 opeq1 4433 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ⟨𝑥, 𝑎⟩ = ⟨𝑦, 𝑎⟩)
142141oveq1d 6705 . . . . . . . . . . 11 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑧) = (⟨𝑦, 𝑎· 𝑧))
143142oveqd 6707 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) = (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))
144 oveq1 6697 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧))
145143, 144eleq12d 2724 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
146140, 145imbi12d 333 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))
147 df-3an 1056 . . . . . . . . . . . . . . 15 (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
14822, 147bitri 264 . . . . . . . . . . . . . 14 (𝜓 ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
149 simpll 805 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
150149eleq1d 2715 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
151150anbi2d 740 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
152 simplr 807 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧)
153152eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑧𝐵))
154153anbi2d 740 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑧𝐵𝑧𝐵)))
155 anidm 677 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑧𝐵) ↔ 𝑧𝐵)
156154, 155syl6bb 276 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑧𝐵))
157151, 156anbi12d 747 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵)))
158 df-3an 1056 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵))
159157, 158syl6bbr 278 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ (𝑥𝐵𝑎𝐵𝑧𝐵)))
160 simpr 476 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
161149oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
162160, 161eleq12d 2724 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
163149oveq1d 6705 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
164163eleq2d 2716 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
165152oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧))
166165eleq2d 2716 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧)))
167162, 164, 1663anbi123d 1439 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
168 df-3an 1056 . . . . . . . . . . . . . . . 16 ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))
169167, 168syl6bb 276 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
170159, 169anbi12d 747 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
171148, 170syl5bb 272 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
172171anbi2d 740 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
173149opeq2d 4440 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
174173oveq1d 6705 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
175 eqidd 2652 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
176174, 175, 160oveq123d 6711 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
177176eleq1d 2715 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))
178172, 177imbi12d 333 . . . . . . . . . . 11 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
179178sbiedv 2438 . . . . . . . . . 10 ((𝑦 = 𝑎𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
180179sbiedv 2438 . . . . . . . . 9 (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
181 iscatd2.4 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
182181sbt 2447 . . . . . . . . . 10 [𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
183182sbt 2447 . . . . . . . . 9 [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
184180, 183chvarv 2299 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))
185146, 184chvarv 2299 . . . . . . 7 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
186185exp45 641 . . . . . 6 (𝜑 → ((𝑦𝐵𝑎𝐵𝑧𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))))
1871863imp 1275 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
188187exlimdv 1901 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
189132, 188mpd 15 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
190133anbi1d 741 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵) ↔ (𝑦𝐵𝑎𝐵)))
191190anbi1d 741 . . . . . 6 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵))))
1921363anbi1d 1443 . . . . . 6 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
193191, 1923anbi23d 1442 . . . . 5 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
194141oveq1d 6705 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑤) = (⟨𝑦, 𝑎· 𝑤))
195194oveqd 6707 . . . . . 6 (𝑥 = 𝑦 → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟))
196 opeq1 4433 . . . . . . . 8 (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
197196oveq1d 6705 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑧· 𝑤) = (⟨𝑦, 𝑧· 𝑤))
198 eqidd 2652 . . . . . . 7 (𝑥 = 𝑦𝑘 = 𝑘)
199197, 198, 143oveq123d 6711 . . . . . 6 (𝑥 = 𝑦 → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
200195, 199eqeq12d 2666 . . . . 5 (𝑥 = 𝑦 → (((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))))
201193, 200imbi12d 333 . . . 4 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))))
202 simpl 472 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑦 = 𝑎)
203202eleq1d 2715 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
204203anbi2d 740 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
205 simpr 476 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑓 = 𝑟)
206202oveq2d 6706 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
207205, 206eleq12d 2724 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
208202oveq1d 6705 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
209208eleq2d 2716 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
210207, 2093anbi12d 1440 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
211204, 2103anbi13d 1441 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
21222, 211syl5bb 272 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
213 df-3an 1056 . . . . . . . . . 10 (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
214212, 213syl6bb 276 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
215214anbi2d 740 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))))
216 3anass 1059 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
217215, 216syl6bbr 278 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
218202opeq2d 4440 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
219218oveq1d 6705 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑤) = (⟨𝑥, 𝑎· 𝑤))
220202opeq1d 4439 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑦, 𝑧⟩ = ⟨𝑎, 𝑧⟩)
221220oveq1d 6705 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑦, 𝑧· 𝑤) = (⟨𝑎, 𝑧· 𝑤))
222221oveqd 6707 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔) = (𝑘(⟨𝑎, 𝑧· 𝑤)𝑔))
223219, 222, 205oveq123d 6711 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟))
224218oveq1d 6705 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
225 eqidd 2652 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑔 = 𝑔)
226224, 225, 205oveq123d 6711 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
227226oveq2d 6706 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
228223, 227eqeq12d 2666 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))))
229217, 228imbi12d 333 . . . . . 6 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
230229sbiedv 2438 . . . . 5 (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
231 iscatd2.5 . . . . . 6 ((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
232231sbt 2447 . . . . 5 [𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
233230, 232chvarv 2299 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
234201, 233chvarv 2299 . . 3 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
2351, 2, 3, 4, 5, 62, 123, 189, 234iscatd 16381 . 2 (𝜑𝐶 ∈ Cat)
2361, 2, 3, 235, 5, 62, 123catidd 16388 . 2 (𝜑 → (Id‘𝐶) = (𝑦𝐵1 ))
237235, 236jca 553 1 (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦𝐵1 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  [wsb 1937  wcel 2030  wne 2823  wral 2941  c0 3948  cop 4216  cmpt 4762  cfv 5926  (class class class)co 6690  Basecbs 15904  Hom chom 15999  compcco 16000  Catccat 16372  Idccid 16373
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-rep 4804  ax-sep 4814  ax-nul 4822  ax-pr 4936
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-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  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-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-cat 16376  df-cid 16377
This theorem is referenced by:  oppccatid  16426  subccatid  16553  fuccatid  16676  setccatid  16781  catccatid  16799  estrccatid  16819  xpccatid  16875  rngccatidALTV  42314  ringccatidALTV  42377
  Copyright terms: Public domain W3C validator