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 weeq2 
 |-  ( x = a -> ( r We x <-> r We a ) )
9 weeq1 
 |-  ( r = s -> ( r We a <-> s We a ) )
10 8 9 sylan9bb 
 |-  ( ( x = a /\ r = s ) -> ( r We x <-> s We a ) )
11 id 
 |-  ( u = v -> u = v )
12 11 sqxpeqd 
 |-  ( u = v -> ( u X. u ) = ( v X. v ) )
13 12 ineq2d 
 |-  ( u = v -> ( r i^i ( u X. u ) ) = ( r i^i ( v X. v ) ) )
14 11 13 oveq12d 
 |-  ( u = v -> ( u F ( r i^i ( u X. u ) ) ) = ( v F ( r i^i ( v X. v ) ) ) )
15 14 eqeq1d 
 |-  ( u = v -> ( ( u F ( r i^i ( u X. u ) ) ) = y <-> ( v F ( r i^i ( v X. v ) ) ) = y ) )
16 15 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 )
17 sneq 
 |-  ( y = z -> { y } = { z } )
18 17 imaeq2d 
 |-  ( y = z -> ( `' r " { y } ) = ( `' r " { z } ) )
19 eqeq2 
 |-  ( y = z -> ( ( v F ( r i^i ( v X. v ) ) ) = y <-> ( v F ( r i^i ( v X. v ) ) ) = z ) )
20 18 19 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 ) )
21 16 20 syl5bb 
 |-  ( 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 ) )
22 21 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 )
23 4 cnveqd 
 |-  ( ( x = a /\ r = s ) -> `' r = `' s )
24 23 imaeq1d 
 |-  ( ( x = a /\ r = s ) -> ( `' r " { z } ) = ( `' s " { z } ) )
25 4 ineq1d 
 |-  ( ( x = a /\ r = s ) -> ( r i^i ( v X. v ) ) = ( s i^i ( v X. v ) ) )
26 25 oveq2d 
 |-  ( ( x = a /\ r = s ) -> ( v F ( r i^i ( v X. v ) ) ) = ( v F ( s i^i ( v X. v ) ) ) )
27 26 eqeq1d 
 |-  ( ( x = a /\ r = s ) -> ( ( v F ( r i^i ( v X. v ) ) ) = z <-> ( v F ( s i^i ( v X. v ) ) ) = z ) )
28 24 27 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 ) )
29 2 28 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 ) )
30 22 29 syl5bb 
 |-  ( ( 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 ) )
31 10 30 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 ) ) )
32 7 31 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 ) ) ) )
33 32 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 ) ) }
34 1 33 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 ) ) }