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 )