Theorem cdleme31sn

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

	Ref	Expression
Hypotheses	cdleme31sn.n	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)$$
	cdleme31sn.c	$$⊢C=if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
Assertion	cdleme31sn	$$⊢R\in A\to ⦋R/s⦌N=C$$

Proof

Step	Hyp	Ref	Expression
1		cdleme31sn.n	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)$$
2		cdleme31sn.c	$$⊢C=if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
3		nfv	$$⊢ℲsR\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
4		nfcsb1v	$$⊢\underset{\_}{Ⅎ}s⦋R/s⦌I$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}s⦋R/s⦌D$$
6	3 4 5	nfif	$$⊢\underset{\_}{Ⅎ}sif\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
7	6	a1i	$$⊢R\in A\to \underset{\_}{Ⅎ}sif\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
8		breq1	$$⊢s=R\to \left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
9		csbeq1a	$$⊢s=R\to I=⦋R/s⦌I$$
10		csbeq1a	$$⊢s=R\to D=⦋R/s⦌D$$
11	8 9 10	ifbieq12d	$$⊢s=R\to if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)=if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
12	7 11	csbiegf	$$⊢R\in A\to ⦋R/s⦌if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)=if\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),⦋R/s⦌I,⦋R/s⦌D\right)$$
13	1	csbeq2i	$$⊢⦋R/s⦌N=⦋R/s⦌if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)$$
14	12 13 2	3eqtr4g	$$⊢R\in A\to ⦋R/s⦌N=C$$