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 ) |