This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme31fv1s

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 25-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))$
	Assertion	cdleme31fv1s	$⊢ (X \in B \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = ⦋ X / x ⦌ O$

Proof

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		eqid	$⊢ (ι 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))) = (ι 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	cdleme31fv1	$⊢ (X \in B \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = (ι 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)))$
5	1 3	cdleme31so	$⊢ X \in B \to ⦋ X / x ⦌ 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)))$
6	5	adantr	$⊢ (X \in B \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to ⦋ X / x ⦌ 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)))$
7	4 6	eqtr4d	$⊢ (X \in B \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = ⦋ X / x ⦌ O$