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

Theorem iscatd2 17725
Description: Version of iscatd 17717 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 4341 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝐻𝑦) ≠ ∅)
763ad2antr1 1188 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅)
8 n0 4352 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
97, 8sylib 218 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
10 n0 4352 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
117, 10sylib 218 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
12 exdistrv 1954 . . . . 5 (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)))
13 simpll 766 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑)
14 simplr2 1216 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎𝐵)
15 simplr1 1215 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦𝐵)
1614, 15jca 511 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎𝐵𝑦𝐵))
17 simplr3 1217 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦))
18 simprl 770 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦))
19 simprr 772 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦))
2017, 18, 193jca 1128 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))
21 iscatd2.ps . . . . . . . . . . . . . . 15 (𝜓 ↔ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
22 simplll 774 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎)
2322eleq1d 2825 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐵𝑎𝐵))
2423anbi1d 631 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑎𝐵𝑦𝐵)))
25 simpllr 775 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦)
2625eleq1d 2825 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐵𝑦𝐵))
27 simplr 768 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦)
2827eleq1d 2825 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑦𝐵))
2926, 28anbi12d 632 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑦𝐵𝑦𝐵)))
30 anidm 564 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝐵) ↔ 𝑦𝐵)
3129, 30bitrdi 287 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑦𝐵))
32 simpr 484 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
3322oveq1d 7447 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦))
3432, 33eleq12d 2834 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦)))
3525oveq2d 7448 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦))
3635eleq2d 2826 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦)))
3725, 27oveq12d 7450 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦))
3837eleq2d 2826 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦)))
3934, 36, 383anbi123d 1437 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))
4024, 31, 393anbi123d 1437 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4121, 40bitrid 283 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
4241anbi2d 630 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))))
4322opeq1d 4878 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑦⟩)
4443oveq1d 7447 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑦) = (⟨𝑎, 𝑦· 𝑦))
45 eqidd 2737 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 )
4644, 45, 32oveq123d 7453 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟))
4746, 32eqeq12d 2752 . . . . . . . . . . . . 13 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓 ↔ ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
4842, 47imbi12d 344 . . . . . . . . . . . 12 ((((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
4948sbiedvw 2094 . . . . . . . . . . 11 (((𝑥 = 𝑎𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5049sbiedvw 2094 . . . . . . . . . 10 ((𝑥 = 𝑎𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
5150sbiedvw 2094 . . . . . . . . 9 (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)))
52 iscatd2.2 . . . . . . . . . . . 12 ((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5352sbt 2065 . . . . . . . . . . 11 [𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5453sbt 2065 . . . . . . . . . 10 [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5554sbt 2065 . . . . . . . . 9 [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → ( 1 (⟨𝑥, 𝑦· 𝑦)𝑓) = 𝑓)
5651, 55chvarvv 1997 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝐵𝑦𝐵) ∧ 𝑦𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5713, 16, 15, 20, 56syl13anc 1373 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
5857ex 412 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
5958exlimdvv 1933 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
6012, 59biimtrrid 243 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟))
619, 11, 60mp2and 699 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦· 𝑦)𝑟) = 𝑟)
6263ad2antr1 1188 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅)
63 n0 4352 . . . . 5 ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
6462, 63sylib 218 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
65 id 22 . . . . . . . 8 (𝑦 = 𝑎𝑦 = 𝑎)
6665, 65oveq12d 7450 . . . . . . 7 (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎))
6766neeq1d 2999 . . . . . 6 (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅))
686ralrimiva 3145 . . . . . . 7 (𝜑 → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
6968adantr 480 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
70 simpr2 1195 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎𝐵)
7167, 69, 70rspcdva 3622 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅)
72 n0 4352 . . . . 5 ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
7371, 72sylib 218 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
74 exdistrv 1954 . . . . 5 (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)))
75 simpll 766 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑)
76 simplr1 1215 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦𝐵)
77 simplr2 1216 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎𝐵)
78 simprl 770 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦))
79 simplr3 1217 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎))
80 simprr 772 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎))
8178, 79, 803jca 1128 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))
82 simplll 774 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦)
8382eleq1d 2825 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐵𝑦𝐵))
8483anbi1d 631 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑦𝐵𝑦𝐵)))
8584, 30bitrdi 287 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ 𝑦𝐵))
86 simpllr 775 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎)
8786eleq1d 2825 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐵𝑎𝐵))
88 simplr 768 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎)
8988eleq1d 2825 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤𝐵𝑎𝐵))
9087, 89anbi12d 632 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑎𝐵𝑎𝐵)))
91 anidm 564 . . . . . . . . . . . . . . . . 17 ((𝑎𝐵𝑎𝐵) ↔ 𝑎𝐵)
9290, 91bitrdi 287 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑎𝐵))
9382oveq1d 7447 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦))
9493eleq2d 2826 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦)))
95 simpr 484 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟)
9686oveq2d 7448 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎))
9795, 96eleq12d 2834 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
9886, 88oveq12d 7450 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎))
9998eleq2d 2826 . . . . . . . . . . . . . . . . 17 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎)))
10094, 97, 993anbi123d 1437 . . . . . . . . . . . . . . . 16 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))
10185, 92, 1003anbi123d 1437 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
10221, 101bitrid 283 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
103102anbi2d 630 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))))
10486oveq2d 7448 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (⟨𝑦, 𝑦· 𝑧) = (⟨𝑦, 𝑦· 𝑎))
105 eqidd 2737 . . . . . . . . . . . . . . 15 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 )
106104, 95, 105oveq123d 7453 . . . . . . . . . . . . . 14 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ))
107106, 95eqeq12d 2752 . . . . . . . . . . . . 13 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔 ↔ (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
108103, 107imbi12d 344 . . . . . . . . . . . 12 ((((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
109108sbiedvw 2094 . . . . . . . . . . 11 (((𝑥 = 𝑦𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
110109sbiedvw 2094 . . . . . . . . . 10 ((𝑥 = 𝑦𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
111110sbiedvw 2094 . . . . . . . . 9 (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)))
112 iscatd2.3 . . . . . . . . . . . 12 ((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
113112sbt 2065 . . . . . . . . . . 11 [𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
114113sbt 2065 . . . . . . . . . 10 [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
115114sbt 2065 . . . . . . . . 9 [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑𝜓) → (𝑔(⟨𝑦, 𝑦· 𝑧) 1 ) = 𝑔)
116111, 115chvarvv 1997 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑎𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
11775, 76, 77, 81, 116syl13anc 1373 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
118117ex 412 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
119118exlimdvv 1933 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12074, 119biimtrrid 243 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟))
12164, 73, 120mp2and 699 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦· 𝑎) 1 ) = 𝑟)
122 id 22 . . . . . . . 8 (𝑦 = 𝑧𝑦 = 𝑧)
123122, 122oveq12d 7450 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧))
124123neeq1d 2999 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅))
125683ad2ant1 1133 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦𝐵 (𝑦𝐻𝑦) ≠ ∅)
126 simp23 1208 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧𝐵)
127124, 125, 126rspcdva 3622 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅)
128 n0 4352 . . . . 5 ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
129127, 128sylib 218 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
130 eleq1w 2823 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
1311303anbi1d 1441 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ (𝑦𝐵𝑎𝐵𝑧𝐵)))
132 oveq1 7439 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎))
133132eleq2d 2826 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
134133anbi1d 631 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))))
135134anbi1d 631 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
136131, 135anbi12d 632 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
137136anbi2d 630 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
138 opeq1 4872 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ⟨𝑥, 𝑎⟩ = ⟨𝑦, 𝑎⟩)
139138oveq1d 7447 . . . . . . . . . . 11 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑧) = (⟨𝑦, 𝑎· 𝑧))
140139oveqd 7449 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) = (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))
141 oveq1 7439 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧))
142140, 141eleq12d 2834 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
143137, 142imbi12d 344 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))
144 df-3an 1088 . . . . . . . . . . . . . . 15 (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
14521, 144bitri 275 . . . . . . . . . . . . . 14 (𝜓 ↔ (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
146 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
147146eleq1d 2825 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
148147anbi2d 630 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
149 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧)
150149eleq1d 2825 . . . . . . . . . . . . . . . . . . 19 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤𝐵𝑧𝐵))
151150anbi2d 630 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ (𝑧𝐵𝑧𝐵)))
152 anidm 564 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵𝑧𝐵) ↔ 𝑧𝐵)
153151, 152bitrdi 287 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧𝐵𝑤𝐵) ↔ 𝑧𝐵))
154148, 153anbi12d 632 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵)))
155 df-3an 1088 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑎𝐵𝑧𝐵) ↔ ((𝑥𝐵𝑎𝐵) ∧ 𝑧𝐵))
156154, 155bitr4di 289 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ (𝑥𝐵𝑎𝐵𝑧𝐵)))
157 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
158146oveq2d 7448 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
159157, 158eleq12d 2834 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
160146oveq1d 7447 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
161160eleq2d 2826 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
162149oveq2d 7448 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧))
163162eleq2d 2826 . . . . . . . . . . . . . . . . 17 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧)))
164159, 161, 1633anbi123d 1437 . . . . . . . . . . . . . . . 16 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
165 df-3an 1088 . . . . . . . . . . . . . . . 16 ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))
166164, 165bitrdi 287 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
167156, 166anbi12d 632 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
168145, 167bitrid 283 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
169168anbi2d 630 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
170146opeq2d 4879 . . . . . . . . . . . . . . 15 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
171170oveq1d 7447 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
172 eqidd 2737 . . . . . . . . . . . . . 14 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
173171, 172, 157oveq123d 7453 . . . . . . . . . . . . 13 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
174173eleq1d 2825 . . . . . . . . . . . 12 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))
175169, 174imbi12d 344 . . . . . . . . . . 11 (((𝑦 = 𝑎𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
176175sbiedvw 2094 . . . . . . . . . 10 ((𝑦 = 𝑎𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
177176sbiedvw 2094 . . . . . . . . 9 (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
178 iscatd2.4 . . . . . . . . . . 11 ((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
179178sbt 2065 . . . . . . . . . 10 [𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
180179sbt 2065 . . . . . . . . 9 [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑𝜓) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
181177, 180chvarvv 1997 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟) ∈ (𝑥𝐻𝑧))
182143, 181chvarvv 1997 . . . . . . 7 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵𝑧𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
183182exp45 438 . . . . . 6 (𝜑 → ((𝑦𝐵𝑎𝐵𝑧𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))))
1841833imp 1110 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
185184exlimdv 1932 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
186129, 185mpd 15 . . 3 ((𝜑 ∧ (𝑦𝐵𝑎𝐵𝑧𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(⟨𝑦, 𝑎· 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
187130anbi1d 631 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐵𝑎𝐵) ↔ (𝑦𝐵𝑎𝐵)))
188187anbi1d 631 . . . . . 6 (𝑥 = 𝑦 → (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ↔ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵))))
1891333anbi1d 1441 . . . . . 6 (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
190188, 1893anbi23d 1440 . . . . 5 (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
191138oveq1d 7447 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑎· 𝑤) = (⟨𝑦, 𝑎· 𝑤))
192191oveqd 7449 . . . . . 6 (𝑥 = 𝑦 → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟))
193 opeq1 4872 . . . . . . . 8 (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
194193oveq1d 7447 . . . . . . 7 (𝑥 = 𝑦 → (⟨𝑥, 𝑧· 𝑤) = (⟨𝑦, 𝑧· 𝑤))
195 eqidd 2737 . . . . . . 7 (𝑥 = 𝑦𝑘 = 𝑘)
196194, 195, 140oveq123d 7453 . . . . . 6 (𝑥 = 𝑦 → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
197192, 196eqeq12d 2752 . . . . 5 (𝑥 = 𝑦 → (((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟))))
198190, 197imbi12d 344 . . . 4 (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))))
199 simpl 482 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑦 = 𝑎)
200199eleq1d 2825 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐵𝑎𝐵))
201200anbi2d 630 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑥𝐵𝑦𝐵) ↔ (𝑥𝐵𝑎𝐵)))
202 simpr 484 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑓 = 𝑟)
203199oveq2d 7448 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
204202, 203eleq12d 2834 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
205199oveq1d 7447 . . . . . . . . . . . . . 14 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
206205eleq2d 2826 . . . . . . . . . . . . 13 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
207204, 2063anbi12d 1438 . . . . . . . . . . . 12 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
208201, 2073anbi13d 1439 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
20921, 208bitrid 283 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
210 df-3an 1088 . . . . . . . . . 10 (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
211209, 210bitrdi 287 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝜓 ↔ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
212211anbi2d 630 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))))
213 3anass 1094 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
214212, 213bitr4di 289 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝜑𝜓) ↔ (𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
215199opeq2d 4879 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
216215oveq1d 7447 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑤) = (⟨𝑥, 𝑎· 𝑤))
217199opeq1d 4878 . . . . . . . . . . 11 ((𝑦 = 𝑎𝑓 = 𝑟) → ⟨𝑦, 𝑧⟩ = ⟨𝑎, 𝑧⟩)
218217oveq1d 7447 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑦, 𝑧· 𝑤) = (⟨𝑎, 𝑧· 𝑤))
219218oveqd 7449 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔) = (𝑘(⟨𝑎, 𝑧· 𝑤)𝑔))
220216, 219, 202oveq123d 7453 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟))
221215oveq1d 7447 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑥, 𝑎· 𝑧))
222 eqidd 2737 . . . . . . . . . 10 ((𝑦 = 𝑎𝑓 = 𝑟) → 𝑔 = 𝑔)
223221, 222, 202oveq123d 7453 . . . . . . . . 9 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))
224223oveq2d 7448 . . . . . . . 8 ((𝑦 = 𝑎𝑓 = 𝑟) → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
225220, 224eqeq12d 2752 . . . . . . 7 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟))))
226214, 225imbi12d 344 . . . . . 6 ((𝑦 = 𝑎𝑓 = 𝑟) → (((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
227226sbiedvw 2094 . . . . 5 (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))))
228 iscatd2.5 . . . . . 6 ((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
229228sbt 2065 . . . . 5 [𝑟 / 𝑓]((𝜑𝜓) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
230227, 229chvarvv 1997 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑎· 𝑧)𝑟)))
231198, 230chvarvv 1997 . . 3 ((𝜑 ∧ ((𝑦𝐵𝑎𝐵) ∧ (𝑧𝐵𝑤𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧· 𝑤)𝑔)(⟨𝑦, 𝑎· 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧· 𝑤)(𝑔(⟨𝑦, 𝑎· 𝑧)𝑟)))
2321, 2, 3, 4, 5, 61, 121, 186, 231iscatd 17717 . 2 (𝜑𝐶 ∈ Cat)
2331, 2, 3, 232, 5, 61, 121catidd 17724 . 2 (𝜑 → (Id‘𝐶) = (𝑦𝐵1 ))
234232, 233jca 511 1 (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦𝐵1 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wex 1778  [wsb 2063  wcel 2107  wne 2939  wral 3060  c0 4332  cop 4631  cmpt 5224  cfv 6560  (class class class)co 7432  Basecbs 17248  Hom chom 17309  compcco 17310  Catccat 17708  Idccid 17709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pr 5431
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-cat 17712  df-cid 17713
This theorem is referenced by:  oppccatid  17763  subccatid  17892  fuccatid  18018  setccatid  18130  catccatid  18152  estrccatid  18177  xpccatid  18234  rngccatidALTV  48193  ringccatidALTV  48227  isthincd2  49111  mndtccatid  49239
  Copyright terms: Public domain W3C validator