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 = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
cdleme31.f 
|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
Assertion cdleme31fv1s 
|- ( ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) -> ( F ` X ) = [_ X / x ]_ O )

Proof

Step Hyp Ref Expression
1 cdleme31.o 
 |-  O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
2 cdleme31.f 
 |-  F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
3 eqid 
 |-  ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) )
4 1 2 3 cdleme31fv1 
 |-  ( ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) -> ( F ` X ) = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) )
5 1 3 cdleme31so 
 |-  ( X e. B -> [_ X / x ]_ O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) )
6 5 adantr 
 |-  ( ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) -> [_ X / x ]_ O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) )
7 4 6 eqtr4d 
 |-  ( ( X e. B /\ ( P =/= Q /\ -. X .<_ W ) ) -> ( F ` X ) = [_ X / x ]_ O )