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

Metamath Proof Explorer

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 )