Theorem iscatd2 17607

Description: Version of iscatd 17599 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 4331	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝐻𝑦) ≠ ∅)
7	6	3ad2antr1 1188	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅)
8		n0 4342	. . . . 5 ⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
9	7, 8	sylib 217	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦))
10		n0 4342	. . . . 5 ⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
11	7, 10	sylib 217	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))
12		exdistrv 1959	. . . . 5 ⊢ (∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)))
13		simpll 765	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑)
14		simplr2 1216	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎 ∈ 𝐵)
15		simplr1 1215	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦 ∈ 𝐵)
16	14, 15	jca 512	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
17		simplr3 1217	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦))
18		simprl 769	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦))
19		simprr 771	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦))
20	17, 18, 19	3jca 1128	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))
21		iscatd2.ps	. . . . . . . . . . . . . . 15 ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
22		simplll 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎)
23	22	eleq1d 2817	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
24	23	anbi1d 630	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
25		simpllr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦)
26	25	eleq1d 2817	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
27		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦)
28	27	eleq1d 2817	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
29	26, 28	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
30		anidm 565	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵)
31	29, 30	bitrdi 286	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵))
32		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
33	22	oveq1d 7408	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦))
34	32, 33	eleq12d 2826	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦)))
35	25	oveq2d 7409	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦))
36	35	eleq2d 2818	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦)))
37	25, 27	oveq12d 7411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦))
38	37	eleq2d 2818	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦)))
39	34, 36, 38	3anbi123d 1436	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))
40	24, 31, 39	3anbi123d 1436	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
41	21, 40	bitrid 282	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))
42	41	anbi2d 629	. . . . . . . . . . . . 13 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))))
43	22	opeq1d 4872	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑦⟩)
44	43	oveq1d 7408	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦⟩ · 𝑦) = (⟨𝑎, 𝑦⟩ · 𝑦))
45		eqidd 2732	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 )
46	44, 45, 32	oveq123d 7414	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟))
47	46, 32	eqeq12d 2747	. . . . . . . . . . . . 13 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓 ↔ ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟))
48	42, 47	imbi12d 344	. . . . . . . . . . . 12 ⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)))
49	48	sbiedvw 2096	. . . . . . . . . . 11 ⊢ (((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)))
50	49	sbiedvw 2096	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)))
51	50	sbiedvw 2096	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)))
52		iscatd2.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)
53	52	sbt 2069	. . . . . . . . . . 11 ⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)
54	53	sbt 2069	. . . . . . . . . 10 ⊢ [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)
55	54	sbt 2069	. . . . . . . . 9 ⊢ [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (⟨𝑥, 𝑦⟩ · 𝑦)𝑓) = 𝑓)
56	51, 55	chvarvv 2002	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)
57	13, 16, 15, 20, 56	syl13anc 1372	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)
58	57	ex 413	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟))
59	58	exlimdvv 1937	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟))
60	12, 59	biimtrrid 242	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟))
61	9, 11, 60	mp2and 697	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (⟨𝑎, 𝑦⟩ · 𝑦)𝑟) = 𝑟)
62	6	3ad2antr1 1188	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅)
63		n0 4342	. . . . 5 ⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
64	62, 63	sylib 217	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦))
65		id 22	. . . . . . . 8 ⊢ (𝑦 = 𝑎 → 𝑦 = 𝑎)
66	65, 65	oveq12d 7411	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎))
67	66	neeq1d 2999	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅))
68	6	ralrimiva 3145	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅)
69	68	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅)
70		simpr2 1195	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎 ∈ 𝐵)
71	67, 69, 70	rspcdva 3610	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅)
72		n0 4342	. . . . 5 ⊢ ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
73	71, 72	sylib 217	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))
74		exdistrv 1959	. . . . 5 ⊢ (∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)))
75		simpll 765	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑)
76		simplr1 1215	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦 ∈ 𝐵)
77		simplr2 1216	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎 ∈ 𝐵)
78		simprl 769	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦))
79		simplr3 1217	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎))
80		simprr 771	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎))
81	78, 79, 80	3jca 1128	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))
82		simplll 773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦)
83	82	eleq1d 2817	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
84	83	anbi1d 630	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
85	84, 30	bitrdi 286	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵))
86		simpllr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎)
87	86	eleq1d 2817	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
88		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎)
89	88	eleq1d 2817	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
90	87, 89	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)))
91		anidm 565	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵)
92	90, 91	bitrdi 286	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵))
93	82	oveq1d 7408	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦))
94	93	eleq2d 2818	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦)))
95		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟)
96	86	oveq2d 7409	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎))
97	95, 96	eleq12d 2826	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
98	86, 88	oveq12d 7411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎))
99	98	eleq2d 2818	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎)))
100	94, 97, 99	3anbi123d 1436	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))
101	85, 92, 100	3anbi123d 1436	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
102	21, 101	bitrid 282	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))
103	102	anbi2d 629	. . . . . . . . . . . . 13 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))))
104	86	oveq2d 7409	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (⟨𝑦, 𝑦⟩ · 𝑧) = (⟨𝑦, 𝑦⟩ · 𝑎))
105		eqidd 2732	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 )
106	104, 95, 105	oveq123d 7414	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ))
107	106, 95	eqeq12d 2747	. . . . . . . . . . . . 13 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔 ↔ (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟))
108	103, 107	imbi12d 344	. . . . . . . . . . . 12 ⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)))
109	108	sbiedvw 2096	. . . . . . . . . . 11 ⊢ (((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)))
110	109	sbiedvw 2096	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)))
111	110	sbiedvw 2096	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)))
112		iscatd2.3	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)
113	112	sbt 2069	. . . . . . . . . . 11 ⊢ [𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)
114	113	sbt 2069	. . . . . . . . . 10 ⊢ [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)
115	114	sbt 2069	. . . . . . . . 9 ⊢ [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑦, 𝑦⟩ · 𝑧) 1 ) = 𝑔)
116	111, 115	chvarvv 2002	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)
117	75, 76, 77, 81, 116	syl13anc 1372	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)
118	117	ex 413	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟))
119	118	exlimdvv 1937	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟))
120	74, 119	biimtrrid 242	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟))
121	64, 73, 120	mp2and 697	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(⟨𝑦, 𝑦⟩ · 𝑎) 1 ) = 𝑟)
122		id 22	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
123	122, 122	oveq12d 7411	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧))
124	123	neeq1d 2999	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅))
125	68	3ad2ant1 1133	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅)
126		simp23 1208	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧 ∈ 𝐵)
127	124, 125, 126	rspcdva 3610	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅)
128		n0 4342	. . . . 5 ⊢ ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
129	127, 128	sylib 217	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧))
130		eleq1w 2815	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
131	130	3anbi1d 1440	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)))
132		oveq1 7400	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎))
133	132	eleq2d 2818	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎)))
134	133	anbi1d 630	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))))
135	134	anbi1d 630	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
136	131, 135	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
137	136	anbi2d 629	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
138		opeq1 4866	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑎⟩ = ⟨𝑦, 𝑎⟩)
139	138	oveq1d 7408	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑎⟩ · 𝑧) = (⟨𝑦, 𝑎⟩ · 𝑧))
140	139	oveqd 7410	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) = (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟))
141		oveq1 7400	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧))
142	140, 141	eleq12d 2826	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
143	137, 142	imbi12d 344	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))
144		df-3an 1089	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
145	21, 144	bitri 274	. . . . . . . . . . . . . 14 ⊢ (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
146		simpll 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
147	146	eleq1d 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
148	147	anbi2d 629	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)))
149		simplr 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧)
150	149	eleq1d 2817	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
151	150	anbi2d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)))
152		anidm 565	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵)
153	151, 152	bitrdi 286	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵))
154	148, 153	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵)))
155		df-3an 1089	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵))
156	154, 155	bitr4di 288	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)))
157		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
158	146	oveq2d 7409	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
159	157, 158	eleq12d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
160	146	oveq1d 7408	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
161	160	eleq2d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
162	149	oveq2d 7409	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧))
163	162	eleq2d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧)))
164	159, 161, 163	3anbi123d 1436	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
165		df-3an 1089	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))
166	164, 165	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))
167	156, 166	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
168	145, 167	bitrid 282	. . . . . . . . . . . . 13 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))
169	168	anbi2d 629	. . . . . . . . . . . 12 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))))
170	146	opeq2d 4873	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
171	170	oveq1d 7408	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦⟩ · 𝑧) = (⟨𝑥, 𝑎⟩ · 𝑧))
172		eqidd 2732	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
173	171, 172, 157	oveq123d 7414	. . . . . . . . . . . . 13 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟))
174	173	eleq1d 2817	. . . . . . . . . . . 12 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))
175	169, 174	imbi12d 344	. . . . . . . . . . 11 ⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
176	175	sbiedvw 2096	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
177	176	sbiedvw 2096	. . . . . . . . 9 ⊢ (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))))
178		iscatd2.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
179	178	sbt 2069	. . . . . . . . . 10 ⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
180	179	sbt 2069	. . . . . . . . 9 ⊢ [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
181	177, 180	chvarvv 2002	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))
182	143, 181	chvarvv 2002	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
183	182	exp45 439	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))))
184	183	3imp 1111	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
185	184	exlimdv 1936	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))
186	129, 185	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))
187	130	anbi1d 630	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)))
188	187	anbi1d 630	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))))
189	133	3anbi1d 1440	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
190	188, 189	3anbi23d 1439	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
191	138	oveq1d 7408	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑎⟩ · 𝑤) = (⟨𝑦, 𝑎⟩ · 𝑤))
192	191	oveqd 7410	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑦, 𝑎⟩ · 𝑤)𝑟))
193		opeq1 4866	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
194	193	oveq1d 7408	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑧⟩ · 𝑤) = (⟨𝑦, 𝑧⟩ · 𝑤))
195		eqidd 2732	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑘 = 𝑘)
196	194, 195, 140	oveq123d 7414	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)) = (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)(𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟)))
197	192, 196	eqeq12d 2747	. . . . 5 ⊢ (𝑥 = 𝑦 → (((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)) ↔ ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑦, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)(𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟))))
198	190, 197	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑦, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)(𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟)))))
199		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎)
200	199	eleq1d 2817	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵))
201	200	anbi2d 629	. . . . . . . . . . . 12 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)))
202		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟)
203	199	oveq2d 7409	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎))
204	202, 203	eleq12d 2826	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎)))
205	199	oveq1d 7408	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧))
206	205	eleq2d 2818	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧)))
207	204, 206	3anbi12d 1437	. . . . . . . . . . . 12 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
208	201, 207	3anbi13d 1438	. . . . . . . . . . 11 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
209	21, 208	bitrid 282	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
210		df-3an 1089	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
211	209, 210	bitrdi 286	. . . . . . . . 9 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
212	211	anbi2d 629	. . . . . . . 8 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))))
213		3anass 1095	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
214	212, 213	bitr4di 288	. . . . . . 7 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))
215	199	opeq2d 4873	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑎⟩)
216	215	oveq1d 7408	. . . . . . . . 9 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦⟩ · 𝑤) = (⟨𝑥, 𝑎⟩ · 𝑤))
217	199	opeq1d 4872	. . . . . . . . . . 11 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ⟨𝑦, 𝑧⟩ = ⟨𝑎, 𝑧⟩)
218	217	oveq1d 7408	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (⟨𝑦, 𝑧⟩ · 𝑤) = (⟨𝑎, 𝑧⟩ · 𝑤))
219	218	oveqd 7410	. . . . . . . . 9 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔) = (𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔))
220	216, 219, 202	oveq123d 7414	. . . . . . . 8 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟))
221	215	oveq1d 7408	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (⟨𝑥, 𝑦⟩ · 𝑧) = (⟨𝑥, 𝑎⟩ · 𝑧))
222		eqidd 2732	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔)
223	221, 222, 202	oveq123d 7414	. . . . . . . . 9 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟))
224	223	oveq2d 7409	. . . . . . . 8 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)))
225	220, 224	eqeq12d 2747	. . . . . . 7 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)) ↔ ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟))))
226	214, 225	imbi12d 344	. . . . . 6 ⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)))))
227	226	sbiedvw 2096	. . . . 5 ⊢ (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)))))
228		iscatd2.5	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))
229	228	sbt 2069	. . . . 5 ⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))
230	227, 229	chvarvv 2002	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑎⟩ · 𝑧)𝑟)))
231	198, 230	chvarvv 2002	. . 3 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑎, 𝑧⟩ · 𝑤)𝑔)(⟨𝑦, 𝑎⟩ · 𝑤)𝑟) = (𝑘(⟨𝑦, 𝑧⟩ · 𝑤)(𝑔(⟨𝑦, 𝑎⟩ · 𝑧)𝑟)))
232	1, 2, 3, 4, 5, 61, 121, 186, 231	iscatd 17599	. 2 ⊢ (𝜑 → 𝐶 ∈ Cat)
233	1, 2, 3, 232, 5, 61, 121	catidd 17606	. 2 ⊢ (𝜑 → (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))
234	232, 233	jca 512	1 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  ∃wex 1781  [wsb 2067   ∈ wcel 2106   ≠ wne 2939  ∀wral 3060  ∅c0 4318  ⟨cop 4628   ↦ cmpt 5224  ‘cfv 6532  (class class class)co 7393  Basecbs 17126  Hom chom 17190  compcco 17191  Catccat 17590  Idccid 17591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-cat 17594  df-cid 17595

This theorem is referenced by:  oppccatid  17647  subccatid  17778  fuccatid  17904  setccatid  18016  catccatid  18038  estrccatid  18065  xpccatid  18122  rngccatidALTV  46535  ringccatidALTV  46598  isthincd2  47306  mndtccatid  47361