Theorem cdleme31sn2

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 26-Feb-2013)

	Ref	Expression
Hypotheses	cdleme32sn2.d	$$⊢D=\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)$$
	cdleme31sn2.n	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)$$
	cdleme31sn2.c	$$⊢C=\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme31sn2	$$⊢\left(R\in A\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to ⦋R/s⦌N=C$$

Proof

Step	Hyp	Ref	Expression
1		cdleme32sn2.d	$$⊢D=\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		cdleme31sn2.n	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)$$
3		cdleme31sn2.c	$$⊢C=\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
4		eqid	$$⊢if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)=if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
5	2 4	cdleme31sn	$$⊢R\in A\to ⦋R/s⦌N=if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
6	5	adantr	$$⊢\left(R\in A\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to ⦋R/s⦌N=if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
7		iffalse	$$⊢\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\to if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)=⦋R/s⦌D$$
8	1	csbeq2i	$$⊢⦋R/s⦌D=⦋R/s⦌\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)$$
9	7 8	eqtrdi	$$⊢\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\to if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)=⦋R/s⦌\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)$$
10		nfcvd	$$⊢R\in A\to \underset{\_}{Ⅎ}s\left(\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
11		oveq1	$$⊢s=R\to s\underset{\dot{}}{\vee }U=R\underset{\dot{}}{\vee }U$$
12		oveq2	$$⊢s=R\to P\underset{\dot{}}{\vee }s=P\underset{\dot{}}{\vee }R$$
13	12	oveq1d	$$⊢s=R\to \left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W=\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W$$
14	13	oveq2d	$$⊢s=R\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 }R\right)\underset{\dot{}}{\wedge }W\right)$$
15	11 14	oveq12d	$$⊢s=R\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(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
16	10 15	csbiegf	$$⊢R\in A\to ⦋R/s⦌\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)=\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
17	9 16	sylan9eqr	$$⊢\left(R\in A\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)=\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
18	6 17	eqtrd	$$⊢\left(R\in A\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to ⦋R/s⦌N=\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
19	18 3	eqtr4di	$$⊢\left(R\in A\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to ⦋R/s⦌N=C$$