cdleme31fv2

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

		Ref	Expression
	Hypothesis	cdleme31fv2.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), O, x))$
	Assertion	cdleme31fv2	$⊢ (X \in B \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = X$

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

Metamath Proof Explorer