Theorem cdleme31sn1

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

	Ref	Expression
Hypotheses	cdleme31sn1.i	$$⊢I=\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=G\right)\right)$$
	cdleme31sn1.n	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)$$
	cdleme31sn1.c	$$⊢C=\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)\right)$$
Assertion	cdleme31sn1	$$⊢\left(R\in A\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to ⦋R/s⦌N=C$$

Proof

Step	Hyp	Ref	Expression
1		cdleme31sn1.i	$$⊢I=\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=G\right)\right)$$
2		cdleme31sn1.n	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,D\right)$$
3		cdleme31sn1.c	$$⊢C=\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\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 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		iftrue	$$⊢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⦌I$$
8	1	csbeq2i	$$⊢⦋R/s⦌I=⦋R/s⦌\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=G\right)\right)$$
9	7 8	eqtrdi	$$⊢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(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=G\right)\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}sA$$
11		nfv	$$⊢Ⅎs\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
12		nfcsb1v	$$⊢\underset{\_}{Ⅎ}s⦋R/s⦌G$$
13	12	nfeq2	$$⊢Ⅎsy=⦋R/s⦌G$$
14	11 13	nfim	$$⊢Ⅎs\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)$$
15	10 14	nfralw	$$⊢Ⅎs\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}sB$$
17	15 16	nfriota	$$⊢\underset{\_}{Ⅎ}s\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)\right)$$
18	17	a1i	$$⊢R\in A\to \underset{\_}{Ⅎ}s\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)\right)$$
19		csbeq1a	$$⊢s=R\to G=⦋R/s⦌G$$
20	19	eqeq2d	$$⊢s=R\to \left(y=G\leftrightarrow y=⦋R/s⦌G\right)$$
21	20	imbi2d	$$⊢s=R\to \left(\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=G\right)\leftrightarrow \left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)\right)$$
22	21	ralbidv	$$⊢s=R\to \left(\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=G\right)\leftrightarrow \forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)\right)$$
23	22	riotabidv	$$⊢s=R\to \left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=G\right)\right)=\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)\right)$$
24	18 23	csbiegf	$$⊢R\in A\to ⦋R/s⦌\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=G\right)\right)=\left(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)\right)$$
25	9 24	sylan9eqr	$$⊢\left(R\in A\wedge 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(\iota y\in B|\forall t\in A\left(\left(\neg t\underset{\dot{}}{\le }W\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to y=⦋R/s⦌G\right)\right)$$
26	25 3	eqtr4di	$$⊢\left(R\in A\wedge 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)=C$$
27	6 26	eqtrd	$$⊢\left(R\in A\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to ⦋R/s⦌N=C$$