Metamath Proof Explorer

Theorem cdleme31so

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

Ref Expression
Hypotheses cdleme31so.o 
|- O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
cdleme31so.c 
|- C = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) )
Assertion cdleme31so 
|- ( X e. B -> [_ X / x ]_ O = C )

Proof

Step Hyp Ref Expression
1 cdleme31so.o 
 |-  O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
2 cdleme31so.c 
 |-  C = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) )
3 nfcvd 
 |-  ( X e. B -> F/_ x ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) )
4 oveq1 
 |-  ( x = X -> ( x ./\ W ) = ( X ./\ W ) )
5 4 oveq2d 
 |-  ( x = X -> ( s .\/ ( x ./\ W ) ) = ( s .\/ ( X ./\ W ) ) )
6 id 
 |-  ( x = X -> x = X )
7 5 6 eqeq12d 
 |-  ( x = X -> ( ( s .\/ ( x ./\ W ) ) = x <-> ( s .\/ ( X ./\ W ) ) = X ) )
8 7 anbi2d 
 |-  ( x = X -> ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) <-> ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) ) )
9 4 oveq2d 
 |-  ( x = X -> ( N .\/ ( x ./\ W ) ) = ( N .\/ ( X ./\ W ) ) )
10 9 eqeq2d 
 |-  ( x = X -> ( z = ( N .\/ ( x ./\ W ) ) <-> z = ( N .\/ ( X ./\ W ) ) ) )
11 8 10 imbi12d 
 |-  ( x = X -> ( ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) <-> ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> z = ( N .\/ ( X ./\ W ) ) ) ) )
12 11 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 ) ) ) ) )
13 12 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 ) ) ) ) )
14 3 13 csbiegf 
 |-  ( X e. B -> [_ 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 ) ) ) ) )
15 1 csbeq2i 
 |-  [_ X / x ]_ O = [_ X / x ]_ ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
16 14 15 2 3eqtr4g 
 |-  ( X e. B -> [_ X / x ]_ O = C )