Theorem cdleme31fv2

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

	Ref	Expression
Hypothesis	cdleme31fv2.f	$$⊢F=\left(x\in B⟼if\left(\left(P\ne Q\wedge \neg x\underset{\dot{}}{\le }W\right),O,x\right)\right)$$
Assertion	cdleme31fv2	$$⊢\left(X\in B\wedge \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to F\left(X\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		cdleme31fv2.f	$$⊢F=\left(x\in B⟼if\left(\left(P\ne Q\wedge \neg x\underset{\dot{}}{\le }W\right),O,x\right)\right)$$
2		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }W\leftrightarrow X\underset{\dot{}}{\le }W\right)$$
3	2	notbid	$$⊢x=X\to \left(\neg x\underset{\dot{}}{\le }W\leftrightarrow \neg X\underset{\dot{}}{\le }W\right)$$
4	3	anbi2d	$$⊢x=X\to \left(\left(P\ne Q\wedge \neg x\underset{\dot{}}{\le }W\right)\leftrightarrow \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)$$
5	4	notbid	$$⊢x=X\to \left(\neg \left(P\ne Q\wedge \neg x\underset{\dot{}}{\le }W\right)\leftrightarrow \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)$$
6	5	biimparc	$$⊢\left(\neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\wedge x=X\right)\to \neg \left(P\ne Q\wedge \neg x\underset{\dot{}}{\le }W\right)$$
7	6	adantll	$$⊢\left(\left(X\in B\wedge \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\wedge x=X\right)\to \neg \left(P\ne Q\wedge \neg x\underset{\dot{}}{\le }W\right)$$
8	7	iffalsed	$$⊢\left(\left(X\in B\wedge \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\wedge x=X\right)\to if\left(\left(P\ne Q\wedge \neg x\underset{\dot{}}{\le }W\right),O,x\right)=x$$
9		simpr	$$⊢\left(\left(X\in B\wedge \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\wedge x=X\right)\to x=X$$
10	8 9	eqtrd	$$⊢\left(\left(X\in B\wedge \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\wedge x=X\right)\to if\left(\left(P\ne Q\wedge \neg x\underset{\dot{}}{\le }W\right),O,x\right)=X$$
11		simpl	$$⊢\left(X\in B\wedge \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to X\in B$$
12	1 10 11 11	fvmptd2	$$⊢\left(X\in B\wedge \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to F\left(X\right)=X$$