This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme25cv

Description: Change bound variables in cdleme25c . (Contributed by NM, 2-Feb-2013)

Ref Expression
Hypotheses cdleme25cv.f 
|- F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
cdleme25cv.n 
|- N = ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ s ) ./\ W ) ) )
cdleme25cv.g 
|- G = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
cdleme25cv.o 
|- O = ( ( P .\/ Q ) ./\ ( G .\/ ( ( R .\/ z ) ./\ W ) ) )
cdleme25cv.i 
|- I = ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) )
cdleme25cv.e 
|- E = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) )
Assertion cdleme25cv 
|- I = E

Proof

Step Hyp Ref Expression
1 cdleme25cv.f 
 |-  F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
2 cdleme25cv.n 
 |-  N = ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ s ) ./\ W ) ) )
3 cdleme25cv.g 
 |-  G = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
4 cdleme25cv.o 
 |-  O = ( ( P .\/ Q ) ./\ ( G .\/ ( ( R .\/ z ) ./\ W ) ) )
5 cdleme25cv.i 
 |-  I = ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) )
6 cdleme25cv.e 
 |-  E = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) )
7 breq1 
 |-  ( s = z -> ( s .<_ W <-> z .<_ W ) )
8 7 notbid 
 |-  ( s = z -> ( -. s .<_ W <-> -. z .<_ W ) )
9 breq1 
 |-  ( s = z -> ( s .<_ ( P .\/ Q ) <-> z .<_ ( P .\/ Q ) ) )
10 9 notbid 
 |-  ( s = z -> ( -. s .<_ ( P .\/ Q ) <-> -. z .<_ ( P .\/ Q ) ) )
11 8 10 anbi12d 
 |-  ( s = z -> ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) <-> ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) ) )
12 oveq1 
 |-  ( s = z -> ( s .\/ U ) = ( z .\/ U ) )
13 oveq2 
 |-  ( s = z -> ( P .\/ s ) = ( P .\/ z ) )
14 13 oveq1d 
 |-  ( s = z -> ( ( P .\/ s ) ./\ W ) = ( ( P .\/ z ) ./\ W ) )
15 14 oveq2d 
 |-  ( s = z -> ( Q .\/ ( ( P .\/ s ) ./\ W ) ) = ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
16 12 15 oveq12d 
 |-  ( s = z -> ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) )
17 oveq2 
 |-  ( s = z -> ( R .\/ s ) = ( R .\/ z ) )
18 17 oveq1d 
 |-  ( s = z -> ( ( R .\/ s ) ./\ W ) = ( ( R .\/ z ) ./\ W ) )
19 16 18 oveq12d 
 |-  ( s = z -> ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) = ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) )
20 19 oveq2d 
 |-  ( s = z -> ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) ) )
21 20 eqeq2d 
 |-  ( s = z -> ( u = ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) ) <-> u = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) ) ) )
22 11 21 imbi12d 
 |-  ( s = z -> ( ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) ) ) <-> ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) ) ) ) )
23 22 cbvralvw 
 |-  ( A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) ) ) <-> A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) ) ) )
24 1 oveq1i 
 |-  ( F .\/ ( ( R .\/ s ) ./\ W ) ) = ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) )
25 24 oveq2i 
 |-  ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ s ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) )
26 2 25 eqtri 
 |-  N = ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) )
27 26 eqeq2i 
 |-  ( u = N <-> u = ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) ) )
28 27 imbi2i 
 |-  ( ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) <-> ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) ) ) )
29 28 ralbii 
 |-  ( A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) <-> A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) .\/ ( ( R .\/ s ) ./\ W ) ) ) ) )
30 3 oveq1i 
 |-  ( G .\/ ( ( R .\/ z ) ./\ W ) ) = ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) )
31 30 oveq2i 
 |-  ( ( P .\/ Q ) ./\ ( G .\/ ( ( R .\/ z ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) )
32 4 31 eqtri 
 |-  O = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) )
33 32 eqeq2i 
 |-  ( u = O <-> u = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) ) )
34 33 imbi2i 
 |-  ( ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) <-> ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) ) ) )
35 34 ralbii 
 |-  ( A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) <-> A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) ) .\/ ( ( R .\/ z ) ./\ W ) ) ) ) )
36 23 29 35 3bitr4i 
 |-  ( A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) <-> A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) )
37 36 a1i 
 |-  ( u e. B -> ( A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) <-> A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) ) )
38 37 riotabiia 
 |-  ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) ) = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) )
39 38 5 6 3eqtr4i 
 |-  I = E