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 = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
Assertion	cdleme31fv2	|- ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) -> ( F ` X ) = X )

Proof

Step	Hyp	Ref	Expression
1		cdleme31fv2.f	|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
2		breq1	|- ( x = X -> ( x .<_ W <-> X .<_ W ) )
3	2	notbid	|- ( x = X -> ( -. x .<_ W <-> -. X .<_ W ) )
4	3	anbi2d	|- ( x = X -> ( ( P =/= Q /\ -. x .<_ W ) <-> ( P =/= Q /\ -. X .<_ W ) ) )
5	4	notbid	|- ( x = X -> ( -. ( P =/= Q /\ -. x .<_ W ) <-> -. ( P =/= Q /\ -. X .<_ W ) ) )
6	5	biimparc	|- ( ( -. ( P =/= Q /\ -. X .<_ W ) /\ x = X ) -> -. ( P =/= Q /\ -. x .<_ W ) )
7	6	adantll	|- ( ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) /\ x = X ) -> -. ( P =/= Q /\ -. x .<_ W ) )
8	7	iffalsed	|- ( ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) /\ x = X ) -> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) = x )
9		simpr	|- ( ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) /\ x = X ) -> x = X )
10	8 9	eqtrd	|- ( ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) /\ x = X ) -> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) = X )
11		simpl	|- ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) -> X e. B )
12	1 10 11 11	fvmptd2	|- ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) -> ( F ` X ) = X )