Metamath Proof Explorer


Theorem cdleme31id

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

Ref Expression
Hypothesis cdleme31fv2.f
|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
Assertion cdleme31id
|- ( ( X e. B /\ P = Q ) -> ( F ` X ) = X )

Proof

Step Hyp Ref Expression
1 cdleme31fv2.f
 |-  F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
2 simpl
 |-  ( ( P =/= Q /\ -. X .<_ W ) -> P =/= Q )
3 2 necon2bi
 |-  ( P = Q -> -. ( P =/= Q /\ -. X .<_ W ) )
4 1 cdleme31fv2
 |-  ( ( X e. B /\ -. ( P =/= Q /\ -. X .<_ W ) ) -> ( F ` X ) = X )
5 3 4 sylan2
 |-  ( ( X e. B /\ P = Q ) -> ( F ` X ) = X )