Theorem iscatd2 17713

Description: Version of iscatd 17705 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.

Step	Hyp	Ref	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	5	ne0d 4294	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝐻𝑦) ≠ ∅)
7	6	3ad2antr1 1202	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅)
8		n0 4305	. . . . 5 ⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
9	7, 8	sylib 220	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
10		n0 4305	. . . . 5 ⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
11	7, 10	sylib 220	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
12		exdistrv 1975	. . . . 5 ⊢ (∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)))
13		simpll 776	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑)
14		simplr2 1230	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎 ∈ 𝐵)
15		simplr1 1229	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦 ∈ 𝐵)
16	14, 15	jca 519	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
17		simplr3 1231	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦))
18		simprl 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦))
19		simprr 782	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦))
20	17, 18, 19	3jca 1141	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))
21		iscatd2.ps	. . . . . . . . . . . . . . 15 ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
22		simplll 784	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎)
23	22	eleq1d 2847	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
24	23	anbi1d 640	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
25		simpllr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦)
26	25	eleq1d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
27		simplr 778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦)
28	27	eleq1d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
29	26, 28	anbi12d 641	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
30		anidm 572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵)
31	29, 30	bitrdi 289	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵))
32		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
33	22	oveq1d 7411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦))
34	32, 33	eleq12d 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦)))
35	25	oveq2d 7412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦))
36	35	eleq2d 2848	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦)))
37	25, 27	oveq12d 7414	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦))
38	37	eleq2d 2848	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦)))
39	34, 36, 38	3anbi123d 1457	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))
40	24, 31, 39	3anbi123d 1457	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
41	21, 40	bitrid 285	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
42	41	anbi2d 639	. . . . . . . . . . . . 13 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))))
43	22	opeq1d 4837	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑦⟩)
44	43	oveq1d 7411	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦⟩ · 𝑦) = (⟨𝑎, 𝑦⟩ · 𝑦))
45		eqidd 2763	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 )
46	44, 45, 32	oveq123d 7417	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟))
47	46, 32	eqeq12d 2778	. . . . . . . . . . . . 13 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓 ↔ ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟))
48	42, 47	imbi12d 346	. . . . . . . . . . . 12 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)))
49	48	sbiedvw 2129	. . . . . . . . . . 11 ⊢ (((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)))
50	49	sbiedvw 2129	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)))
51	50	sbiedvw 2129	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)))
52		iscatd2.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)
53	52	sbt 2095	. . . . . . . . . . 11 ⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)
54	53	sbt 2095	. . . . . . . . . 10 ⊢ [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)
55	54	sbt 2095	. . . . . . . . 9 ⊢ [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)
56	51, 55	chvarvv 2009	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)
57	13, 16, 15, 20, 56	syl13anc 1391	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)
58	57	ex 416	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟))
59	58	exlimdvv 1954	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟))
60	12, 59	biimtrrid 245	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟))
61	9, 11, 60	mp2and 709	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)
62	6	3ad2antr1 1202	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅)
63		n0 4305	. . . . 5 ⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
64	62, 63	sylib 220	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
65		id 22	. . . . . . . 8 ⊢ (𝑦 = 𝑎 → 𝑦 = 𝑎)
66	65, 65	oveq12d 7414	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎))
67	66	neeq1d 3016	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅))
68	6	ralrimiva 3154	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅)
69	68	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅)
70		simpr2 1209	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎 ∈ 𝐵)
71	67, 69, 70	rspcdva 3582	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅)
72		n0 4305	. . . . 5 ⊢ ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
73	71, 72	sylib 220	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
74		exdistrv 1975	. . . . 5 ⊢ (∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)))
75		simpll 776	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑)
76		simplr1 1229	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦 ∈ 𝐵)
77		simplr2 1230	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎 ∈ 𝐵)
78		simprl 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦))
79		simplr3 1231	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎))
80		simprr 782	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎))
81	78, 79, 80	3jca 1141	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))
82		simplll 784	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦)
83	82	eleq1d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
84	83	anbi1d 640	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
85	84, 30	bitrdi 289	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵))
86		simpllr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎)
87	86	eleq1d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
88		simplr 778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎)
89	88	eleq1d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
90	87, 89	anbi12d 641	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)))
91		anidm 572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵)
92	90, 91	bitrdi 289	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵))
93	82	oveq1d 7411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦))
94	93	eleq2d 2848	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦)))
95		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟)
96	86	oveq2d 7412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎))
97	95, 96	eleq12d 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
98	86, 88	oveq12d 7414	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎))
99	98	eleq2d 2848	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎)))
100	94, 97, 99	3anbi123d 1457	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))
101	85, 92, 100	3anbi123d 1457	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
102	21, 101	bitrid 285	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
103	102	anbi2d 639	. . . . . . . . . . . . 13 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))))
104	86	oveq2d 7412	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (⟨𝑦, 𝑦⟩ · 𝑧) = (⟨𝑦, 𝑦⟩ · 𝑎))
105		eqidd 2763	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 )
106	104, 95, 105	oveq123d 7417	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ))
107	106, 95	eqeq12d 2778	. . . . . . . . . . . . 13 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔 ↔ (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟))
108	103, 107	imbi12d 346	. . . . . . . . . . . 12 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)))
109	108	sbiedvw 2129	. . . . . . . . . . 11 ⊢ (((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)))
110	109	sbiedvw 2129	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)))
111	110	sbiedvw 2129	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)))
112		iscatd2.3	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)
113	112	sbt 2095	. . . . . . . . . . 11 ⊢ [𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)
114	113	sbt 2095	. . . . . . . . . 10 ⊢ [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)
115	114	sbt 2095	. . . . . . . . 9 ⊢ [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)
116	111, 115	chvarvv 2009	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)
117	75, 76, 77, 81, 116	syl13anc 1391	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)
118	117	ex 416	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟))
119	118	exlimdvv 1954	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟))
120	74, 119	biimtrrid 245	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟))
121	64, 73, 120	mp2and 709	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)
122		id 22	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
123	122, 122	oveq12d 7414	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧))
124	123	neeq1d 3016	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅))
125	68	3ad2ant1 1146	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅)
126		simp23 1222	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧 ∈ 𝐵)
127	124, 125, 126	rspcdva 3582	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅)
128		n0 4305	. . . . 5 ⊢ ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
129	127, 128	sylib 220	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
130		eleq1w 2845	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
131	130	3anbi1d 1461	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)))
132		oveq1 7403	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎))
133	132	eleq2d 2848	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
134	133	anbi1d 640	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))))
135	134	anbi1d 640	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
136	131, 135	anbi12d 641	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
137	136	anbi2d 639	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
138		opeq1 4831	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑎⟩ = ⟨𝑦, 𝑎⟩)
139	138	oveq1d 7411	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑎⟩ · 𝑧) = (⟨𝑦, 𝑎⟩ · 𝑧))
140	139	oveqd 7413	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) = (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟))
141		oveq1 7403	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧))
142	140, 141	eleq12d 2856	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
143	137, 142	imbi12d 346	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))
144		df-3an 1100	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
145	21, 144	bitri 277	. . . . . . . . . . . . . 14 ⊢ (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
146		simpll 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
147	146	eleq1d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
148	147	anbi2d 639	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)))
149		simplr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧)
150	149	eleq1d 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
151	150	anbi2d 639	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)))
152		anidm 572	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵)
153	151, 152	bitrdi 289	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵))
154	148, 153	anbi12d 641	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵)))
155		df-3an 1100	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵))
156	154, 155	bitr4di 291	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)))
157		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
158	146	oveq2d 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
159	157, 158	eleq12d 2856	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
160	146	oveq1d 7411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
161	160	eleq2d 2848	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
162	149	oveq2d 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧))
163	162	eleq2d 2848	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧)))
164	159, 161, 163	3anbi123d 1457	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
165		df-3an 1100	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))
166	164, 165	bitrdi 289	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
167	156, 166	anbi12d 641	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
168	145, 167	bitrid 285	. . . . . . . . . . . . 13 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
169	168	anbi2d 639	. . . . . . . . . . . 12 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
170	146	opeq2d 4838	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
171	170	oveq1d 7411	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦⟩ · 𝑧) = (⟨𝑥, 𝑎⟩ · 𝑧))
172		eqidd 2763	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
173	171, 172, 157	oveq123d 7417	. . . . . . . . . . . . 13 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟))
174	173	eleq1d 2847	. . . . . . . . . . . 12 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))
175	169, 174	imbi12d 346	. . . . . . . . . . 11 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
176	175	sbiedvw 2129	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
177	176	sbiedvw 2129	. . . . . . . . 9 ⊢ (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
178		iscatd2.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
179	178	sbt 2095	. . . . . . . . . 10 ⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
180	179	sbt 2095	. . . . . . . . 9 ⊢ [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
181	177, 180	chvarvv 2009	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))
182	143, 181	chvarvv 2009	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
183	182	exp45 442	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))))
184	183	3imp 1123	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
185	184	exlimdv 1953	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
186	129, 185	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
187	130	anbi1d 640	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)))
188	187	anbi1d 640	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))))
189	133	3anbi1d 1461	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
190	188, 189	3anbi23d 1460	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
191	138	oveq1d 7411	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑎⟩ · 𝑤) = (⟨𝑦, 𝑎⟩ · 𝑤))
192	191	oveqd 7413	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑦, 𝑎⟩ · 𝑤)𝑟))
193		opeq1 4831	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
194	193	oveq1d 7411	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑧⟩ · 𝑤) = (⟨𝑦, 𝑧⟩ · 𝑤))
195		eqidd 2763	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑘 = 𝑘)
196	194, 195, 140	oveq123d 7417	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)) = (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)(𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟)))
197	192, 196	eqeq12d 2778	. . . . 5 ⊢ (𝑥 = 𝑦 → (((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)) ↔ ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑦, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)(𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟))))
198	190, 197	imbi12d 346	. . . 4 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑦, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)(𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟)))))
199		simpl 486	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
200	199	eleq1d 2847	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
201	200	anbi2d 639	. . . . . . . . . . . 12 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)))
202		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
203	199	oveq2d 7412	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
204	202, 203	eleq12d 2856	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
205	199	oveq1d 7411	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
206	205	eleq2d 2848	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
207	204, 206	3anbi12d 1458	. . . . . . . . . . . 12 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
208	201, 207	3anbi13d 1459	. . . . . . . . . . 11 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
209	21, 208	bitrid 285	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
210		df-3an 1100	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
211	209, 210	bitrdi 289	. . . . . . . . 9 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
212	211	anbi2d 639	. . . . . . . 8 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))))
213		3anass 1106	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
214	212, 213	bitr4di 291	. . . . . . 7 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
215	199	opeq2d 4838	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
216	215	oveq1d 7411	. . . . . . . . 9 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦⟩ · 𝑤) = (⟨𝑥, 𝑎⟩ · 𝑤))
217	199	opeq1d 4837	. . . . . . . . . . 11 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ⟨𝑦, 𝑧⟩ = ⟨𝑎, 𝑧⟩)
218	217	oveq1d 7411	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (⟨𝑦, 𝑧⟩ · 𝑤) = (⟨𝑎, 𝑧⟩ · 𝑤))
219	218	oveqd 7413	. . . . . . . . 9 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔) = (𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔))
220	216, 219, 202	oveq123d 7417	. . . . . . . 8 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟))
221	215	oveq1d 7411	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦⟩ · 𝑧) = (⟨𝑥, 𝑎⟩ · 𝑧))
222		eqidd 2763	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
223	221, 222, 202	oveq123d 7417	. . . . . . . . 9 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟))
224	223	oveq2d 7412	. . . . . . . 8 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)))
225	220, 224	eqeq12d 2778	. . . . . . 7 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)) ↔ ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟))))
226	214, 225	imbi12d 346	. . . . . 6 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)))))
227	226	sbiedvw 2129	. . . . 5 ⊢ (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)))))
228		iscatd2.5	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))
229	228	sbt 2095	. . . . 5 ⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))
230	227, 229	chvarvv 2009	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)))
231	198, 230	chvarvv 2009	. . 3 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑦, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)(𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟)))
232	1, 2, 3, 4, 5, 61, 121, 186, 231	iscatd 17705	. 2 ⊢ (𝜑 → 𝐶 ∈ Cat)
233	1, 2, 3, 232, 5, 61, 121	catidd 17712	. 2 ⊢ (𝜑 → (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))
234	232, 233	jca 519	1 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1098   = wceq 1560  ∃wex 1799  [wsb 2090   ∈ wcel 2142   ≠ wne 2957  ∀wral 3076  ∅c0 4285  ⟨cop 4588   ↦ cmpt 5181  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  Hom chom 17297  compcco 17298  Catccat 17696  Idccid 17697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-cat 17700  df-cid 17701

This theorem is referenced by:  oppccatid  17751  subccatid  17879  fuccatid  18005  setccatid  18117  catccatid  18139  estrccatid  18164  xpccatid  18220  rngccatidALTV  48891  ringccatidALTV  48925  ssccatid  49690  isthincd2  50055  mndtccatid  50205  2arwcat  50218