isthincd2lem2

	Ref	Expression
Hypotheses	isthincd2lem2.1	$⊢ φ \to X \in B$
	isthincd2lem2.2	$⊢ φ \to Y \in B$
	isthincd2lem2.3	$⊢ φ \to Z \in B$
	isthincd2lem2.4	$⊢ φ \to F \in (X H Y)$
	isthincd2lem2.5	$⊢ φ \to G \in (Y H Z)$
	isthincd2lem2.6	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
Assertion	isthincd2lem2	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z)$

Proof

Step	Hyp	Ref	Expression
1		isthincd2lem2.1	$⊢ φ \to X \in B$
2		isthincd2lem2.2	$⊢ φ \to Y \in B$
3		isthincd2lem2.3	$⊢ φ \to Z \in B$
4		isthincd2lem2.4	$⊢ φ \to F \in (X H Y)$
5		isthincd2lem2.5	$⊢ φ \to G \in (Y H Z)$
6		isthincd2lem2.6	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
7		oveq1	$⊢ x = w \to x H y = w H y$
8		opeq1	$⊢ x = w \to ⟨x, y⟩ = ⟨w, y⟩$
9	8	oveq1d	$⊢ x = w \to ⟨x, y⟩ \underset{˙}{\cdot} z = ⟨w, y⟩ \underset{˙}{\cdot} z$
10	9	oveqd	$⊢ x = w \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨w, y⟩ \underset{˙}{\cdot} z) f$
11		oveq1	$⊢ x = w \to x H z = w H z$
12	10 11	eleq12d	$⊢ x = w \to (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \leftrightarrow g (⟨w, y⟩ \underset{˙}{\cdot} z) f \in (w H z))$
13	12	ralbidv	$⊢ x = w \to (\forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \leftrightarrow \forall g \in (y H z) g (⟨w, y⟩ \underset{˙}{\cdot} z) f \in (w H z))$
14	7 13	raleqbidv	$⊢ x = w \to (\forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \leftrightarrow \forall f \in (w H y) \forall g \in (y H z) g (⟨w, y⟩ \underset{˙}{\cdot} z) f \in (w H z))$
15		oveq2	$⊢ y = v \to w H y = w H v$
16		oveq1	$⊢ y = v \to y H z = v H z$
17		opeq2	$⊢ y = v \to ⟨w, y⟩ = ⟨w, v⟩$
18	17	oveq1d	$⊢ y = v \to ⟨w, y⟩ \underset{˙}{\cdot} z = ⟨w, v⟩ \underset{˙}{\cdot} z$
19	18	oveqd	$⊢ y = v \to g (⟨w, y⟩ \underset{˙}{\cdot} z) f = g (⟨w, v⟩ \underset{˙}{\cdot} z) f$
20	19	eleq1d	$⊢ y = v \to (g (⟨w, y⟩ \underset{˙}{\cdot} z) f \in (w H z) \leftrightarrow g (⟨w, v⟩ \underset{˙}{\cdot} z) f \in (w H z))$
21	16 20	raleqbidv	$⊢ y = v \to (\forall g \in (y H z) g (⟨w, y⟩ \underset{˙}{\cdot} z) f \in (w H z) \leftrightarrow \forall g \in (v H z) g (⟨w, v⟩ \underset{˙}{\cdot} z) f \in (w H z))$
22	15 21	raleqbidv	$⊢ y = v \to (\forall f \in (w H y) \forall g \in (y H z) g (⟨w, y⟩ \underset{˙}{\cdot} z) f \in (w H z) \leftrightarrow \forall f \in (w H v) \forall g \in (v H z) g (⟨w, v⟩ \underset{˙}{\cdot} z) f \in (w H z))$
23		oveq2	$⊢ z = u \to v H z = v H u$
24		oveq2	$⊢ z = u \to ⟨w, v⟩ \underset{˙}{\cdot} z = ⟨w, v⟩ \underset{˙}{\cdot} u$
25	24	oveqd	$⊢ z = u \to g (⟨w, v⟩ \underset{˙}{\cdot} z) f = g (⟨w, v⟩ \underset{˙}{\cdot} u) f$
26		oveq2	$⊢ z = u \to w H z = w H u$
27	25 26	eleq12d	$⊢ z = u \to (g (⟨w, v⟩ \underset{˙}{\cdot} z) f \in (w H z) \leftrightarrow g (⟨w, v⟩ \underset{˙}{\cdot} u) f \in (w H u))$
28	23 27	raleqbidv	$⊢ z = u \to (\forall g \in (v H z) g (⟨w, v⟩ \underset{˙}{\cdot} z) f \in (w H z) \leftrightarrow \forall g \in (v H u) g (⟨w, v⟩ \underset{˙}{\cdot} u) f \in (w H u))$
29	28	ralbidv	$⊢ z = u \to (\forall f \in (w H v) \forall g \in (v H z) g (⟨w, v⟩ \underset{˙}{\cdot} z) f \in (w H z) \leftrightarrow \forall f \in (w H v) \forall g \in (v H u) g (⟨w, v⟩ \underset{˙}{\cdot} u) f \in (w H u))$
30		oveq2	$⊢ f = k \to g (⟨w, v⟩ \underset{˙}{\cdot} u) f = g (⟨w, v⟩ \underset{˙}{\cdot} u) k$
31	30	eleq1d	$⊢ f = k \to (g (⟨w, v⟩ \underset{˙}{\cdot} u) f \in (w H u) \leftrightarrow g (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u))$
32		oveq1	$⊢ g = l \to g (⟨w, v⟩ \underset{˙}{\cdot} u) k = l (⟨w, v⟩ \underset{˙}{\cdot} u) k$
33	32	eleq1d	$⊢ g = l \to (g (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u) \leftrightarrow l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u))$
34	31 33	cbvral2vw	$⊢ \forall f \in (w H v) \forall g \in (v H u) g (⟨w, v⟩ \underset{˙}{\cdot} u) f \in (w H u) \leftrightarrow \forall k \in (w H v) \forall l \in (v H u) l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u)$
35	29 34	bitrdi	$⊢ z = u \to (\forall f \in (w H v) \forall g \in (v H z) g (⟨w, v⟩ \underset{˙}{\cdot} z) f \in (w H z) \leftrightarrow \forall k \in (w H v) \forall l \in (v H u) l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u))$
36	14 22 35	cbvral3vw	$⊢ \forall x \in B \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \leftrightarrow \forall w \in B \forall v \in B \forall u \in B \forall k \in (w H v) \forall l \in (v H u) l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u)$
37	6 36	sylib	$⊢ φ \to \forall w \in B \forall v \in B \forall u \in B \forall k \in (w H v) \forall l \in (v H u) l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u)$
38		oveq1	$⊢ w = X \to w H v = X H v$
39		opeq1	$⊢ w = X \to ⟨w, v⟩ = ⟨X, v⟩$
40	39	oveq1d	$⊢ w = X \to ⟨w, v⟩ \underset{˙}{\cdot} u = ⟨X, v⟩ \underset{˙}{\cdot} u$
41	40	oveqd	$⊢ w = X \to l (⟨w, v⟩ \underset{˙}{\cdot} u) k = l (⟨X, v⟩ \underset{˙}{\cdot} u) k$
42		oveq1	$⊢ w = X \to w H u = X H u$
43	41 42	eleq12d	$⊢ w = X \to (l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u) \leftrightarrow l (⟨X, v⟩ \underset{˙}{\cdot} u) k \in (X H u))$
44	43	ralbidv	$⊢ w = X \to (\forall l \in (v H u) l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u) \leftrightarrow \forall l \in (v H u) l (⟨X, v⟩ \underset{˙}{\cdot} u) k \in (X H u))$
45	38 44	raleqbidv	$⊢ w = X \to (\forall k \in (w H v) \forall l \in (v H u) l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u) \leftrightarrow \forall k \in (X H v) \forall l \in (v H u) l (⟨X, v⟩ \underset{˙}{\cdot} u) k \in (X H u))$
46		oveq2	$⊢ v = Y \to X H v = X H Y$
47		oveq1	$⊢ v = Y \to v H u = Y H u$
48		opeq2	$⊢ v = Y \to ⟨X, v⟩ = ⟨X, Y⟩$
49	48	oveq1d	$⊢ v = Y \to ⟨X, v⟩ \underset{˙}{\cdot} u = ⟨X, Y⟩ \underset{˙}{\cdot} u$
50	49	oveqd	$⊢ v = Y \to l (⟨X, v⟩ \underset{˙}{\cdot} u) k = l (⟨X, Y⟩ \underset{˙}{\cdot} u) k$
51	50	eleq1d	$⊢ v = Y \to (l (⟨X, v⟩ \underset{˙}{\cdot} u) k \in (X H u) \leftrightarrow l (⟨X, Y⟩ \underset{˙}{\cdot} u) k \in (X H u))$
52	47 51	raleqbidv	$⊢ v = Y \to (\forall l \in (v H u) l (⟨X, v⟩ \underset{˙}{\cdot} u) k \in (X H u) \leftrightarrow \forall l \in (Y H u) l (⟨X, Y⟩ \underset{˙}{\cdot} u) k \in (X H u))$
53	46 52	raleqbidv	$⊢ v = Y \to (\forall k \in (X H v) \forall l \in (v H u) l (⟨X, v⟩ \underset{˙}{\cdot} u) k \in (X H u) \leftrightarrow \forall k \in (X H Y) \forall l \in (Y H u) l (⟨X, Y⟩ \underset{˙}{\cdot} u) k \in (X H u))$
54		oveq2	$⊢ u = Z \to Y H u = Y H Z$
55		oveq2	$⊢ u = Z \to ⟨X, Y⟩ \underset{˙}{\cdot} u = ⟨X, Y⟩ \underset{˙}{\cdot} Z$
56	55	oveqd	$⊢ u = Z \to l (⟨X, Y⟩ \underset{˙}{\cdot} u) k = l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k$
57		oveq2	$⊢ u = Z \to X H u = X H Z$
58	56 57	eleq12d	$⊢ u = Z \to (l (⟨X, Y⟩ \underset{˙}{\cdot} u) k \in (X H u) \leftrightarrow l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z))$
59	54 58	raleqbidv	$⊢ u = Z \to (\forall l \in (Y H u) l (⟨X, Y⟩ \underset{˙}{\cdot} u) k \in (X H u) \leftrightarrow \forall l \in (Y H Z) l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z))$
60	59	ralbidv	$⊢ u = Z \to (\forall k \in (X H Y) \forall l \in (Y H u) l (⟨X, Y⟩ \underset{˙}{\cdot} u) k \in (X H u) \leftrightarrow \forall k \in (X H Y) \forall l \in (Y H Z) l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z))$
61	45 53 60	rspc3v	$⊢ (X \in B \land Y \in B \land Z \in B) \to (\forall w \in B \forall v \in B \forall u \in B \forall k \in (w H v) \forall l \in (v H u) l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u) \to \forall k \in (X H Y) \forall l \in (Y H Z) l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z))$
62	1 2 3 61	syl3anc	$⊢ φ \to (\forall w \in B \forall v \in B \forall u \in B \forall k \in (w H v) \forall l \in (v H u) l (⟨w, v⟩ \underset{˙}{\cdot} u) k \in (w H u) \to \forall k \in (X H Y) \forall l \in (Y H Z) l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z))$
63	37 62	mpd	$⊢ φ \to \forall k \in (X H Y) \forall l \in (Y H Z) l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z)$
64		oveq2	$⊢ k = F \to l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k = l (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
65	64	eleq1d	$⊢ k = F \to (l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z) \leftrightarrow l (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
66		oveq1	$⊢ l = G \to l (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
67	66	eleq1d	$⊢ l = G \to (l (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z) \leftrightarrow G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
68	65 67	rspc2v	$⊢ (F \in (X H Y) \land G \in (Y H Z)) \to (\forall k \in (X H Y) \forall l \in (Y H Z) l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
69	4 5 68	syl2anc	$⊢ φ \to (\forall k \in (X H Y) \forall l \in (Y H Z) l (⟨X, Y⟩ \underset{˙}{\cdot} Z) k \in (X H Z) \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z))$
70	63 69	mpd	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X H Z)$

Metamath Proof Explorer

Theorem isthincd2lem2

Proof