cdleme31fv1

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

	Ref	Expression
Hypotheses	cdleme31.o	$⊢ O = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = N \underset{˙}{\lor} (x \underset{˙}{\land} W)))$
	cdleme31.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), O, x))$
	cdleme31.c	$⊢ C = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to z = N \underset{˙}{\lor} (X \underset{˙}{\land} W)))$
Assertion	cdleme31fv1	$⊢ (X \in B \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = C$

Step	Hyp	Ref	Expression
1		cdleme31.o	$⊢ O = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = N \underset{˙}{\lor} (x \underset{˙}{\land} W)))$
2		cdleme31.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), O, x))$
3		cdleme31.c	$⊢ C = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to z = N \underset{˙}{\lor} (X \underset{˙}{\land} W)))$
4	1 2 3	cdleme31fv	$⊢ X \in B \to F (X) = if ((P \neq Q \land \neg X \underset{˙}{\leq} W), C, X)$
5		iftrue	$⊢ (P \neq Q \land \neg X \underset{˙}{\leq} W) \to if ((P \neq Q \land \neg X \underset{˙}{\leq} W), C, X) = C$
6	4 5	sylan9eq	$⊢ (X \in B \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = C$

Metamath Proof Explorer