Theorem isthincd2lem2 50254

Description: Lemma for isthincd2 50256. (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 7430	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑥𝐻𝑦) = (𝑤𝐻𝑦))
3		opeq1 4843	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ⟨𝑥, 𝑦⟩ = ⟨𝑤, 𝑦⟩)
4	3	oveq1d 7438	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (⟨𝑥, 𝑦⟩ · 𝑧) = (⟨𝑤, 𝑦⟩ · 𝑧))
5	4	oveqd 7440	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓))
6		oveq1 7430	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥𝐻𝑧) = (𝑤𝐻𝑧))
7	5, 6	eleq12d 2860	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
8	7	ralbidv 3191	. . . . . 6 ⊢ (𝑥 = 𝑤 → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
9	2, 8	raleqbidv 3341	. . . . 5 ⊢ (𝑥 = 𝑤 → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
10		oveq2 7431	. . . . . 6 ⊢ (𝑦 = 𝑣 → (𝑤𝐻𝑦) = (𝑤𝐻𝑣))
11		oveq1 7430	. . . . . . 7 ⊢ (𝑦 = 𝑣 → (𝑦𝐻𝑧) = (𝑣𝐻𝑧))
12		opeq2 4844	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → ⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑣⟩)
13	12	oveq1d 7438	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → (⟨𝑤, 𝑦⟩ · 𝑧) = (⟨𝑤, 𝑣⟩ · 𝑧))
14	13	oveqd 7440	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → (𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓))
15	14	eleq1d 2851	. . . . . . 7 ⊢ (𝑦 = 𝑣 → ((𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
16	11, 15	raleqbidv 3341	. . . . . 6 ⊢ (𝑦 = 𝑣 → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
17	10, 16	raleqbidv 3341	. . . . 5 ⊢ (𝑦 = 𝑣 → (∀𝑓 ∈ (𝑤𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
18		oveq2 7431	. . . . . . . 8 ⊢ (𝑧 = 𝑢 → (𝑣𝐻𝑧) = (𝑣𝐻𝑢))
19		oveq2 7431	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (⟨𝑤, 𝑣⟩ · 𝑧) = (⟨𝑤, 𝑣⟩ · 𝑢))
20	19	oveqd 7440	. . . . . . . . 9 ⊢ (𝑧 = 𝑢 → (𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓))
21		oveq2 7431	. . . . . . . . 9 ⊢ (𝑧 = 𝑢 → (𝑤𝐻𝑧) = (𝑤𝐻𝑢))
22	20, 21	eleq12d 2860	. . . . . . . 8 ⊢ (𝑧 = 𝑢 → ((𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
23	18, 22	raleqbidv 3341	. . . . . . 7 ⊢ (𝑧 = 𝑢 → (∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
24	23	ralbidv 3191	. . . . . 6 ⊢ (𝑧 = 𝑢 → (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
25		oveq2 7431	. . . . . . . 8 ⊢ (𝑓 = 𝑘 → (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) = (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑘))
26	25	eleq1d 2851	. . . . . . 7 ⊢ (𝑓 = 𝑘 → ((𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢) ↔ (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
27		oveq1 7430	. . . . . . . 8 ⊢ (𝑔 = 𝑙 → (𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) = (𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘))
28	27	eleq1d 2851	. . . . . . 7 ⊢ (𝑔 = 𝑙 → ((𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ (𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
29	26, 28	cbvral2vw 3250	. . . . . 6 ⊢ (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣⟩ · 𝑢)𝑓) ∈ (𝑤𝐻𝑢) ↔ ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
30	24, 29	bitrdi 290	. . . . 5 ⊢ (𝑧 = 𝑢 → (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣⟩ · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
31	9, 17, 30	cbvral3vw 3252	. . . 4 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
32	1, 31	sylib 221	. . 3 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
33		isthincd2lem2.1	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
34		isthincd2lem2.2	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
35		isthincd2lem2.3	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
36		oveq1 7430	. . . . . 6 ⊢ (𝑤 = 𝑋 → (𝑤𝐻𝑣) = (𝑋𝐻𝑣))
37		opeq1 4843	. . . . . . . . . 10 ⊢ (𝑤 = 𝑋 → ⟨𝑤, 𝑣⟩ = ⟨𝑋, 𝑣⟩)
38	37	oveq1d 7438	. . . . . . . . 9 ⊢ (𝑤 = 𝑋 → (⟨𝑤, 𝑣⟩ · 𝑢) = (⟨𝑋, 𝑣⟩ · 𝑢))
39	38	oveqd 7440	. . . . . . . 8 ⊢ (𝑤 = 𝑋 → (𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘))
40		oveq1 7430	. . . . . . . 8 ⊢ (𝑤 = 𝑋 → (𝑤𝐻𝑢) = (𝑋𝐻𝑢))
41	39, 40	eleq12d 2860	. . . . . . 7 ⊢ (𝑤 = 𝑋 → ((𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
42	41	ralbidv 3191	. . . . . 6 ⊢ (𝑤 = 𝑋 → (∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ ∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
43	36, 42	raleqbidv 3341	. . . . 5 ⊢ (𝑤 = 𝑋 → (∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
44		oveq2 7431	. . . . . 6 ⊢ (𝑣 = 𝑌 → (𝑋𝐻𝑣) = (𝑋𝐻𝑌))
45		oveq1 7430	. . . . . . 7 ⊢ (𝑣 = 𝑌 → (𝑣𝐻𝑢) = (𝑌𝐻𝑢))
46		opeq2 4844	. . . . . . . . . 10 ⊢ (𝑣 = 𝑌 → ⟨𝑋, 𝑣⟩ = ⟨𝑋, 𝑌⟩)
47	46	oveq1d 7438	. . . . . . . . 9 ⊢ (𝑣 = 𝑌 → (⟨𝑋, 𝑣⟩ · 𝑢) = (⟨𝑋, 𝑌⟩ · 𝑢))
48	47	oveqd 7440	. . . . . . . 8 ⊢ (𝑣 = 𝑌 → (𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘))
49	48	eleq1d 2851	. . . . . . 7 ⊢ (𝑣 = 𝑌 → ((𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
50	45, 49	raleqbidv 3341	. . . . . 6 ⊢ (𝑣 = 𝑌 → (∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
51	44, 50	raleqbidv 3341	. . . . 5 ⊢ (𝑣 = 𝑌 → (∀𝑘 ∈ (𝑋𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
52		oveq2 7431	. . . . . . 7 ⊢ (𝑢 = 𝑍 → (𝑌𝐻𝑢) = (𝑌𝐻𝑍))
53		oveq2 7431	. . . . . . . . 9 ⊢ (𝑢 = 𝑍 → (⟨𝑋, 𝑌⟩ · 𝑢) = (⟨𝑋, 𝑌⟩ · 𝑍))
54	53	oveqd 7440	. . . . . . . 8 ⊢ (𝑢 = 𝑍 → (𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘))
55		oveq2 7431	. . . . . . . 8 ⊢ (𝑢 = 𝑍 → (𝑋𝐻𝑢) = (𝑋𝐻𝑍))
56	54, 55	eleq12d 2860	. . . . . . 7 ⊢ (𝑢 = 𝑍 → ((𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
57	52, 56	raleqbidv 3341	. . . . . 6 ⊢ (𝑢 = 𝑍 → (∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
58	57	ralbidv 3191	. . . . 5 ⊢ (𝑢 = 𝑍 → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌⟩ · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
59	43, 51, 58	rspc3v 3600	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
60	33, 34, 35, 59	syl3anc 1398	. . 3 ⊢ (𝜑 → (∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣⟩ · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
61	32, 60	mpd 16	. 2 ⊢ (𝜑 → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍))
62		isthincd2lem2.4	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))
63		isthincd2lem2.5	. . 3 ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))
64		oveq2 7431	. . . . 5 ⊢ (𝑘 = 𝐹 → (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) = (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
65	64	eleq1d 2851	. . . 4 ⊢ (𝑘 = 𝐹 → ((𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) ↔ (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
66		oveq1 7430	. . . . 5 ⊢ (𝑙 = 𝐺 → (𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
67	66	eleq1d 2851	. . . 4 ⊢ (𝑙 = 𝐺 → ((𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍) ↔ (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
68	65, 67	rspc2v 3595	. . 3 ⊢ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑍)) → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
69	62, 63, 68	syl2anc 596	. 2 ⊢ (𝜑 → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌⟩ · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
70	61, 69	mpd 16	1 ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∀wral 3082  ⟨cop 4600  (class class class)co 7423

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  isthincd2  50256