Theorem cdleme25cv

Description: Change bound variables in cdleme25c . (Contributed by NM, 2-Feb-2013)

	Ref	Expression
Hypotheses	cdleme25cv.f	$$⊢F=\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme25cv.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme25cv.g	$$⊢G=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme25cv.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme25cv.i	$$⊢I=\left(\iota u\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\right)$$
	cdleme25cv.e	$$⊢E=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
Assertion	cdleme25cv	$$⊢I=E$$

Proof

Step	Hyp	Ref	Expression
1		cdleme25cv.f	$$⊢F=\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
2		cdleme25cv.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
3		cdleme25cv.g	$$⊢G=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
4		cdleme25cv.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
5		cdleme25cv.i	$$⊢I=\left(\iota u\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\right)$$
6		cdleme25cv.e	$$⊢E=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
7		breq1	$$⊢s=z\to \left(s\underset{\dot{}}{\le }W\leftrightarrow z\underset{\dot{}}{\le }W\right)$$
8	7	notbid	$$⊢s=z\to \left(\neg s\underset{\dot{}}{\le }W\leftrightarrow \neg z\underset{\dot{}}{\le }W\right)$$
9		breq1	$$⊢s=z\to \left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
10	9	notbid	$$⊢s=z\to \left(\neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
11	8 10	anbi12d	$$⊢s=z\to \left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
12		oveq1	$$⊢s=z\to s\underset{\dot{}}{\vee }U=z\underset{\dot{}}{\vee }U$$
13		oveq2	$$⊢s=z\to P\underset{\dot{}}{\vee }s=P\underset{\dot{}}{\vee }z$$
14	13	oveq1d	$$⊢s=z\to \left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W=\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W$$
15	14	oveq2d	$$⊢s=z\to Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)=Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
16	12 15	oveq12d	$$⊢s=z\to \left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
17		oveq2	$$⊢s=z\to R\underset{\dot{}}{\vee }s=R\underset{\dot{}}{\vee }z$$
18	17	oveq1d	$$⊢s=z\to \left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W=\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W$$
19	16 18	oveq12d	$$⊢s=z\to \left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)=\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
20	19	oveq2d	$$⊢s=z\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
21	20	eqeq2d	$$⊢s=z\to \left(u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\leftrightarrow u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
22	11 21	imbi12d	$$⊢s=z\to \left(\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\leftrightarrow \left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\right)$$
23	22	cbvralvw	$$⊢\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\leftrightarrow \forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
24	1	oveq1i	$$⊢F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)=\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)$$
25	24	oveq2i	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
26	2 25	eqtri	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
27	26	eqeq2i	$$⊢u=N\leftrightarrow u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
28	27	imbi2i	$$⊢\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\leftrightarrow \left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
29	28	ralbii	$$⊢\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\leftrightarrow \forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
30	3	oveq1i	$$⊢G\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)=\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)$$
31	30	oveq2i	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
32	4 31	eqtri	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
33	32	eqeq2i	$$⊢u=O\leftrightarrow u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
34	33	imbi2i	$$⊢\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\leftrightarrow \left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
35	34	ralbii	$$⊢\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\leftrightarrow \forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(\left(\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
36	23 29 35	3bitr4i	$$⊢\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\leftrightarrow \forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)$$
37	36	a1i	$$⊢u\in B\to \left(\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\leftrightarrow \forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
38	37	riotabiia	$$⊢\left(\iota u\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge \neg s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\right)=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
39	38 5 6	3eqtr4i	$$⊢I=E$$