Metamath Proof Explorer

Theorem fpwwe2cbv

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 3-Jun-2015)

Ref Expression
Hypothesis fpwwe2.1 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
Assertion fpwwe2cbv 
|- W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) ) }

Proof

Step Hyp Ref Expression
1 fpwwe2.1 
 |-  W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
2 simpl 
 |-  ( ( x = a /\ r = s ) -> x = a )
3 2 sseq1d 
 |-  ( ( x = a /\ r = s ) -> ( x C_ A <-> a C_ A ) )
4 simpr 
 |-  ( ( x = a /\ r = s ) -> r = s )
5 2 sqxpeqd 
 |-  ( ( x = a /\ r = s ) -> ( x X. x ) = ( a X. a ) )
6 4 5 sseq12d 
 |-  ( ( x = a /\ r = s ) -> ( r C_ ( x X. x ) <-> s C_ ( a X. a ) ) )
7 3 6 anbi12d 
 |-  ( ( x = a /\ r = s ) -> ( ( x C_ A /\ r C_ ( x X. x ) ) <-> ( a C_ A /\ s C_ ( a X. a ) ) ) )
8 4 2 weeq12d 
 |-  ( ( x = a /\ r = s ) -> ( r We x <-> s We a ) )
9 id 
 |-  ( u = v -> u = v )
10 9 sqxpeqd 
 |-  ( u = v -> ( u X. u ) = ( v X. v ) )
11 10 ineq2d 
 |-  ( u = v -> ( r i^i ( u X. u ) ) = ( r i^i ( v X. v ) ) )
12 9 11 oveq12d 
 |-  ( u = v -> ( u F ( r i^i ( u X. u ) ) ) = ( v F ( r i^i ( v X. v ) ) ) )
13 12 eqeq1d 
 |-  ( u = v -> ( ( u F ( r i^i ( u X. u ) ) ) = y <-> ( v F ( r i^i ( v X. v ) ) ) = y ) )
14 13 cbvsbcvw 
 |-  ( [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y <-> [. ( `' r " { y } ) / v ]. ( v F ( r i^i ( v X. v ) ) ) = y )
15 sneq 
 |-  ( y = z -> { y } = { z } )
16 15 imaeq2d 
 |-  ( y = z -> ( `' r " { y } ) = ( `' r " { z } ) )
17 eqeq2 
 |-  ( y = z -> ( ( v F ( r i^i ( v X. v ) ) ) = y <-> ( v F ( r i^i ( v X. v ) ) ) = z ) )
18 16 17 sbceqbid 
 |-  ( y = z -> ( [. ( `' r " { y } ) / v ]. ( v F ( r i^i ( v X. v ) ) ) = y <-> [. ( `' r " { z } ) / v ]. ( v F ( r i^i ( v X. v ) ) ) = z ) )
19 14 18 bitrid 
 |-  ( y = z -> ( [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y <-> [. ( `' r " { z } ) / v ]. ( v F ( r i^i ( v X. v ) ) ) = z ) )
20 19 cbvralvw 
 |-  ( A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y <-> A. z e. x [. ( `' r " { z } ) / v ]. ( v F ( r i^i ( v X. v ) ) ) = z )
21 4 cnveqd 
 |-  ( ( x = a /\ r = s ) -> `' r = `' s )
22 21 imaeq1d 
 |-  ( ( x = a /\ r = s ) -> ( `' r " { z } ) = ( `' s " { z } ) )
23 4 ineq1d 
 |-  ( ( x = a /\ r = s ) -> ( r i^i ( v X. v ) ) = ( s i^i ( v X. v ) ) )
24 23 oveq2d 
 |-  ( ( x = a /\ r = s ) -> ( v F ( r i^i ( v X. v ) ) ) = ( v F ( s i^i ( v X. v ) ) ) )
25 24 eqeq1d 
 |-  ( ( x = a /\ r = s ) -> ( ( v F ( r i^i ( v X. v ) ) ) = z <-> ( v F ( s i^i ( v X. v ) ) ) = z ) )
26 22 25 sbceqbid 
 |-  ( ( x = a /\ r = s ) -> ( [. ( `' r " { z } ) / v ]. ( v F ( r i^i ( v X. v ) ) ) = z <-> [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) )
27 2 26 raleqbidv 
 |-  ( ( x = a /\ r = s ) -> ( A. z e. x [. ( `' r " { z } ) / v ]. ( v F ( r i^i ( v X. v ) ) ) = z <-> A. z e. a [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) )
28 20 27 bitrid 
 |-  ( ( x = a /\ r = s ) -> ( A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y <-> A. z e. a [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) )
29 8 28 anbi12d 
 |-  ( ( x = a /\ r = s ) -> ( ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) <-> ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) ) )
30 7 29 anbi12d 
 |-  ( ( x = a /\ r = s ) -> ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) <-> ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) ) ) )
31 30 cbvopabv 
 |-  { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) } = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) ) }
32 1 31 eqtri 
 |-  W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) ) }