Theorem cdleme31so

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

	Ref	Expression
Hypotheses	cdleme31so.o	$$⊢O=\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to z=N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)$$
	cdleme31so.c	$$⊢C=\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\to z=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
Assertion	cdleme31so	$$⊢X\in B\to ⦋X/x⦌O=C$$

Proof

Step	Hyp	Ref	Expression
1		cdleme31so.o	$$⊢O=\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to z=N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)$$
2		cdleme31so.c	$$⊢C=\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\to z=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
3		nfcvd	$$⊢X\in B\to \underset{\_}{Ⅎ}x\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\to z=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
4		oveq1	$$⊢x=X\to x\underset{\dot{}}{\wedge }W=X\underset{\dot{}}{\wedge }W$$
5	4	oveq2d	$$⊢x=X\to s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)$$
6		id	$$⊢x=X\to x=X$$
7	5 6	eqeq12d	$$⊢x=X\to \left(s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\leftrightarrow s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)$$
8	7	anbi2d	$$⊢x=X\to \left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\leftrightarrow \left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\right)$$
9	4	oveq2d	$$⊢x=X\to N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)$$
10	9	eqeq2d	$$⊢x=X\to \left(z=N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)\leftrightarrow z=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)$$
11	8 10	imbi12d	$$⊢x=X\to \left(\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to z=N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)\right)\leftrightarrow \left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\to z=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
12	11	ralbidv	$$⊢x=X\to \left(\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to z=N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)\right)\leftrightarrow \forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\to z=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
13	12	riotabidv	$$⊢x=X\to \left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to z=N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)=\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\to z=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
14	3 13	csbiegf	$$⊢X\in B\to ⦋X/x⦌\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to z=N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)=\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\to z=N\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
15	1	csbeq2i	$$⊢⦋X/x⦌O=⦋X/x⦌\left(\iota z\in B|\forall s\in A\left(\left(\neg s\underset{\dot{}}{\le }W\wedge s\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to z=N\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)$$
16	14 15 2	3eqtr4g	$$⊢X\in B\to ⦋X/x⦌O=C$$