Theorem hdmap1cbv

Description: Frequently used lemma to change bound variables in L hypothesis. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypothesis	hdmap1cbv.l	$$⊢L=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
Assertion	hdmap1cbv	$$⊢L=\left(y\in \mathrm{V}⟼if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota i\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1cbv.l	$$⊢L=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
2		fveq2	$$⊢x=y\to 2^{nd}\left(x\right)=2^{nd}\left(y\right)$$
3	2	eqeq1d	$$⊢x=y\to \left(2^{nd}\left(x\right)=\underset{\dot{}}{0}\leftrightarrow 2^{nd}\left(y\right)=\underset{\dot{}}{0}\right)$$
4	2	sneqd	$$⊢x=y\to \left\{2^{nd}\left(x\right)\right\}=\left\{2^{nd}\left(y\right)\right\}$$
5	4	fveq2d	$$⊢x=y\to N\left(\left\{2^{nd}\left(x\right)\right\}\right)=N\left(\left\{2^{nd}\left(y\right)\right\}\right)$$
6	5	fveq2d	$$⊢x=y\to M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)$$
7	6	eqeq1d	$$⊢x=y\to \left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\leftrightarrow M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\right)$$
8		2fveq3	$$⊢x=y\to 1^{st}\left(1^{st}\left(x\right)\right)=1^{st}\left(1^{st}\left(y\right)\right)$$
9	8 2	oveq12d	$$⊢x=y\to 1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)=1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)$$
10	9	sneqd	$$⊢x=y\to \left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}=\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}$$
11	10	fveq2d	$$⊢x=y\to N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)=N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)$$
12	11	fveq2d	$$⊢x=y\to M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)$$
13		2fveq3	$$⊢x=y\to 2^{nd}\left(1^{st}\left(x\right)\right)=2^{nd}\left(1^{st}\left(y\right)\right)$$
14	13	oveq1d	$$⊢x=y\to 2^{nd}\left(1^{st}\left(x\right)\right)Rh=2^{nd}\left(1^{st}\left(y\right)\right)Rh$$
15	14	sneqd	$$⊢x=y\to \left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}=\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}$$
16	15	fveq2d	$$⊢x=y\to J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)$$
17	12 16	eqeq12d	$$⊢x=y\to \left(M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\leftrightarrow M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)$$
18	7 17	anbi12d	$$⊢x=y\to \left(\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\leftrightarrow \left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)$$
19	18	riotabidv	$$⊢x=y\to \left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)$$
20	3 19	ifbieq2d	$$⊢x=y\to if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)=if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)\right)$$
21	20	cbvmptv	$$⊢\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)=\left(y\in \mathrm{V}⟼if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
22		sneq	$$⊢h=i\to \left\{h\right\}=\left\{i\right\}$$
23	22	fveq2d	$$⊢h=i\to J\left(\left\{h\right\}\right)=J\left(\left\{i\right\}\right)$$
24	23	eqeq2d	$$⊢h=i\to \left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\leftrightarrow M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\right)$$
25		oveq2	$$⊢h=i\to 2^{nd}\left(1^{st}\left(y\right)\right)Rh=2^{nd}\left(1^{st}\left(y\right)\right)Ri$$
26	25	sneqd	$$⊢h=i\to \left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}=\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}$$
27	26	fveq2d	$$⊢h=i\to J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)$$
28	27	eqeq2d	$$⊢h=i\to \left(M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\leftrightarrow M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)$$
29	24 28	anbi12d	$$⊢h=i\to \left(\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\leftrightarrow \left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)\right)$$
30	29	cbvriotavw	$$⊢\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)=\left(\iota i\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)\right)$$
31		ifeq2	$$⊢\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)=\left(\iota i\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)\right)\to if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)\right)=if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota i\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)\right)\right)$$
32	30 31	ax-mp	$$⊢if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)\right)=if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota i\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)\right)\right)$$
33	32	mpteq2i	$$⊢\left(y\in \mathrm{V}⟼if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Rh\right\}\right)\right)\right)\right)\right)=\left(y\in \mathrm{V}⟼if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota i\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)\right)\right)\right)$$
34	1 21 33	3eqtri	$$⊢L=\left(y\in \mathrm{V}⟼if\left(2^{nd}\left(y\right)=\underset{\dot{}}{0},Q,\left(\iota i\in D|\left(M\left(N\left(\left\{2^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(y\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(y\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(y\right)\right)Ri\right\}\right)\right)\right)\right)\right)$$