Metamath Proof Explorer

Theorem cdleme31fv

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 10-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 ) )
cdleme31.c 
|- C = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) )
Assertion cdleme31fv 
|- ( X e. B -> ( F ` X ) = if ( ( P =/= Q /\ -. X .<_ W ) , C , X ) )

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 cdleme31.c 
 |-  C = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) )
4 riotaex 
 |-  ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) e. _V
5 3 4 eqeltri 
 |-  C e. _V
6 ifexg 
 |-  ( ( C e. _V /\ X e. B ) -> if ( ( P =/= Q /\ -. X .<_ W ) , C , X ) e. _V )
7 5 6 mpan 
 |-  ( X e. B -> if ( ( P =/= Q /\ -. X .<_ W ) , C , X ) e. _V )
8 breq1 
 |-  ( x = X -> ( x .<_ W <-> X .<_ W ) )
9 8 notbid 
 |-  ( x = X -> ( -. x .<_ W <-> -. X .<_ W ) )
10 9 anbi2d 
 |-  ( x = X -> ( ( P =/= Q /\ -. x .<_ W ) <-> ( P =/= Q /\ -. X .<_ W ) ) )
11 oveq1 
 |-  ( x = X -> ( x ./\ W ) = ( X ./\ W ) )
12 11 oveq2d 
 |-  ( x = X -> ( s .\/ ( x ./\ W ) ) = ( s .\/ ( X ./\ W ) ) )
13 id 
 |-  ( x = X -> x = X )
14 12 13 eqeq12d 
 |-  ( x = X -> ( ( s .\/ ( x ./\ W ) ) = x <-> ( s .\/ ( X ./\ W ) ) = X ) )
15 14 anbi2d 
 |-  ( x = X -> ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) <-> ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) ) )
16 11 oveq2d 
 |-  ( x = X -> ( N .\/ ( x ./\ W ) ) = ( N .\/ ( X ./\ W ) ) )
17 16 eqeq2d 
 |-  ( x = X -> ( z = ( N .\/ ( x ./\ W ) ) <-> z = ( N .\/ ( X ./\ W ) ) ) )
18 15 17 imbi12d 
 |-  ( x = X -> ( ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) <-> ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) )
19 18 ralbidv 
 |-  ( x = X -> ( A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) <-> A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) )
20 19 riotabidv 
 |-  ( x = X -> ( 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 ) ) ) ) )
21 20 1 3 3eqtr4g 
 |-  ( x = X -> O = C )
22 10 21 13 ifbieq12d 
 |-  ( x = X -> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) = if ( ( P =/= Q /\ -. X .<_ W ) , C , X ) )
23 22 2 fvmptg 
 |-  ( ( X e. B /\ if ( ( P =/= Q /\ -. X .<_ W ) , C , X ) e. _V ) -> ( F ` X ) = if ( ( P =/= Q /\ -. X .<_ W ) , C , X ) )
24 7 23 mpdan 
 |-  ( X e. B -> ( F ` X ) = if ( ( P =/= Q /\ -. X .<_ W ) , C , X ) )