Theorem isthincd2lem2 47176

Description: Lemma for isthincd2 47178. (Contributed by Zhi Wang, 17-Sep-2024.)

Hypotheses

Ref	Expression
isthincd2lem2.1	⊢ (𝜑 → 𝑋 ∈ 𝐵)
isthincd2lem2.2	⊢ (𝜑 → 𝑌 ∈ 𝐵)
isthincd2lem2.3	⊢ (𝜑 → 𝑍 ∈ 𝐵)
isthincd2lem2.4	⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))
isthincd2lem2.5	⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))
isthincd2lem2.6	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))

Assertion

Ref	Expression
isthincd2lem2	⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))

Distinct variable groups:   · ,𝑓,𝑔,𝑧,𝑥,𝑦   𝑧,𝐵,𝑥,𝑦   𝑓,𝐻,𝑔,𝑧,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐵(𝑓,𝑔)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐺(𝑥,𝑦,𝑧,𝑓,𝑔)   𝑋(𝑥,𝑦,𝑧,𝑓,𝑔)   𝑌(𝑥,𝑦,𝑧,𝑓,𝑔)   𝑍(𝑥,𝑦,𝑧,𝑓,𝑔)

Proof of Theorem isthincd2lem2

Dummy variables 𝑘 𝑢 𝑣 𝑤 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isthincd2lem2.6	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
2		oveq1 7369	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑥𝐻𝑦) = (𝑤𝐻𝑦))
3		opeq1 4835	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ⟨𝑥, 𝑦⟩ = ⟨𝑤, 𝑦⟩)
4	3	oveq1d 7377	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (⟨𝑥, 𝑦⟩ · 𝑧) = (⟨𝑤, 𝑦⟩ · 𝑧))
5	4	oveqd 7379	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓))
6		oveq1 7369	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥𝐻𝑧) = (𝑤𝐻𝑧))
7	5, 6	eleq12d 2826	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
8	7	ralbidv 3170	. . . . . 6 ⊢ (𝑥 = 𝑤 → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
9	2, 8	raleqbidv 3317	. . . . 5 ⊢ (𝑥 = 𝑤 → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
10		oveq2 7370	. . . . . 6 ⊢ (𝑦 = 𝑣 → (𝑤𝐻𝑦) = (𝑤𝐻𝑣))
11		oveq1 7369	. . . . . . 7 ⊢ (𝑦 = 𝑣 → (𝑦𝐻𝑧) = (𝑣𝐻𝑧))
12		opeq2 4836	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → ⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑣⟩)
13	12	oveq1d 7377	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → (⟨𝑤, 𝑦⟩ · 𝑧) = (⟨𝑤, 𝑣⟩ · 𝑧))
14	13	oveqd 7379	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → (𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓))
15	14	eleq1d 2817	. . . . . . 7 ⊢ (𝑦 = 𝑣 → ((𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
16	11, 15	raleqbidv 3317	. . . . . 6 ⊢ (𝑦 = 𝑣 → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
17	10, 16	raleqbidv 3317	. . . . 5 ⊢ (𝑦 = 𝑣 → (∀𝑓 ∈ (𝑤𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
18		oveq2 7370	. . . . . . . 8 ⊢ (𝑧 = 𝑢 → (𝑣𝐻𝑧) = (𝑣𝐻𝑢))
19		oveq2 7370	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (⟨𝑤, 𝑣⟩ · 𝑧) = (⟨𝑤, 𝑣⟩ · 𝑢))
20	19	oveqd 7379	. . . . . . . . 9 ⊢ (𝑧 = 𝑢 → (𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓))
21		oveq2 7370	. . . . . . . . 9 ⊢ (𝑧 = 𝑢 → (𝑤𝐻𝑧) = (𝑤𝐻𝑢))
22	20, 21	eleq12d 2826	. . . . . . . 8 ⊢ (𝑧 = 𝑢 → ((𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
23	18, 22	raleqbidv 3317	. . . . . . 7 ⊢ (𝑧 = 𝑢 → (∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
24	23	ralbidv 3170	. . . . . 6 ⊢ (𝑧 = 𝑢 → (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
25		oveq2 7370	. . . . . . . 8 ⊢ (𝑓 = 𝑘 → (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) = (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑘))
26	25	eleq1d 2817	. . . . . . 7 ⊢ (𝑓 = 𝑘 → ((𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢) ↔ (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
27		oveq1 7369	. . . . . . . 8 ⊢ (𝑔 = 𝑙 → (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) = (𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘))
28	27	eleq1d 2817	. . . . . . 7 ⊢ (𝑔 = 𝑙 → ((𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ (𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
29	26, 28	cbvral2vw 3225	. . . . . 6 ⊢ (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢) ↔ ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
30	24, 29	bitrdi 286	. . . . 5 ⊢ (𝑧 = 𝑢 → (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
31	9, 17, 30	cbvral3vw 3227	. . . 4 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
32	1, 31	sylib 217	. . 3 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
33		isthincd2lem2.1	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
34		isthincd2lem2.2	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
35		isthincd2lem2.3	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
36		oveq1 7369	. . . . . 6 ⊢ (𝑤 = 𝑋 → (𝑤𝐻𝑣) = (𝑋𝐻𝑣))
37		opeq1 4835	. . . . . . . . . 10 ⊢ (𝑤 = 𝑋 → ⟨𝑤, 𝑣⟩ = ⟨𝑋, 𝑣⟩)
38	37	oveq1d 7377	. . . . . . . . 9 ⊢ (𝑤 = 𝑋 → (⟨𝑤, 𝑣⟩ · 𝑢) = (⟨𝑋, 𝑣⟩ · 𝑢))
39	38	oveqd 7379	. . . . . . . 8 ⊢ (𝑤 = 𝑋 → (𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘))
40		oveq1 7369	. . . . . . . 8 ⊢ (𝑤 = 𝑋 → (𝑤𝐻𝑢) = (𝑋𝐻𝑢))
41	39, 40	eleq12d 2826	. . . . . . 7 ⊢ (𝑤 = 𝑋 → ((𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
42	41	ralbidv 3170	. . . . . 6 ⊢ (𝑤 = 𝑋 → (∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ ∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
43	36, 42	raleqbidv 3317	. . . . 5 ⊢ (𝑤 = 𝑋 → (∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
44		oveq2 7370	. . . . . 6 ⊢ (𝑣 = 𝑌 → (𝑋𝐻𝑣) = (𝑋𝐻𝑌))
45		oveq1 7369	. . . . . . 7 ⊢ (𝑣 = 𝑌 → (𝑣𝐻𝑢) = (𝑌𝐻𝑢))
46		opeq2 4836	. . . . . . . . . 10 ⊢ (𝑣 = 𝑌 → ⟨𝑋, 𝑣⟩ = ⟨𝑋, 𝑌⟩)
47	46	oveq1d 7377	. . . . . . . . 9 ⊢ (𝑣 = 𝑌 → (⟨𝑋, 𝑣⟩ · 𝑢) = (⟨𝑋, 𝑌⟩ · 𝑢))
48	47	oveqd 7379	. . . . . . . 8 ⊢ (𝑣 = 𝑌 → (𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘))
49	48	eleq1d 2817	. . . . . . 7 ⊢ (𝑣 = 𝑌 → ((𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
50	45, 49	raleqbidv 3317	. . . . . 6 ⊢ (𝑣 = 𝑌 → (∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
51	44, 50	raleqbidv 3317	. . . . 5 ⊢ (𝑣 = 𝑌 → (∀𝑘 ∈ (𝑋𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
52		oveq2 7370	. . . . . . 7 ⊢ (𝑢 = 𝑍 → (𝑌𝐻𝑢) = (𝑌𝐻𝑍))
53		oveq2 7370	. . . . . . . . 9 ⊢ (𝑢 = 𝑍 → (⟨𝑋, 𝑌⟩ · 𝑢) = (⟨𝑋, 𝑌⟩ · 𝑍))
54	53	oveqd 7379	. . . . . . . 8 ⊢ (𝑢 = 𝑍 → (𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘))
55		oveq2 7370	. . . . . . . 8 ⊢ (𝑢 = 𝑍 → (𝑋𝐻𝑢) = (𝑋𝐻𝑍))
56	54, 55	eleq12d 2826	. . . . . . 7 ⊢ (𝑢 = 𝑍 → ((𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
57	52, 56	raleqbidv 3317	. . . . . 6 ⊢ (𝑢 = 𝑍 → (∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
58	57	ralbidv 3170	. . . . 5 ⊢ (𝑢 = 𝑍 → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
59	43, 51, 58	rspc3v 3594	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
60	33, 34, 35, 59	syl3anc 1371	. . 3 ⊢ (𝜑 → (∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
61	32, 60	mpd 15	. 2 ⊢ (𝜑 → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍))
62		isthincd2lem2.4	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))
63		isthincd2lem2.5	. . 3 ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))
64		oveq2 7370	. . . . 5 ⊢ (𝑘 = 𝐹 → (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) = (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
65	64	eleq1d 2817	. . . 4 ⊢ (𝑘 = 𝐹 → ((𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) ↔ (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
66		oveq1 7369	. . . . 5 ⊢ (𝑙 = 𝐺 → (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
67	66	eleq1d 2817	. . . 4 ⊢ (𝑙 = 𝐺 → ((𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍) ↔ (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
68	65, 67	rspc2v 3591	. . 3 ⊢ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑍)) → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
69	62, 63, 68	syl2anc 584	. 2 ⊢ (𝜑 → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
70	61, 69	mpd 15	1 ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3060  ⟨cop 4597  (class class class)co 7362

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-ext 2702

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-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365

This theorem is referenced by:  isthincd2  47178