Theorem cdleme31id

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 18-Apr-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	cdleme31id	$$⊢\left(X\in B\wedge P=Q\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		simpl	$$⊢\left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)\to P\ne Q$$
3	2	necon2bi	$$⊢P=Q\to \neg \left(P\ne Q\wedge \neg X\underset{\dot{}}{\le }W\right)$$
4	1	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$$
5	3 4	sylan2	$$⊢\left(X\in B\wedge P=Q\right)\to F\left(X\right)=X$$