Metamath Proof Explorer

Theorem fpwwecbv

Description: Lemma for fpwwe . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypothesis fpwwe.1 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
Assertion fpwwecbv 
|- W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( F ` ( `' s " { z } ) ) = z ) ) }

Proof

Step Hyp Ref Expression
1 fpwwe.1 
 |-  W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = 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 sneq 
 |-  ( y = z -> { y } = { z } )
10 9 imaeq2d 
 |-  ( y = z -> ( `' r " { y } ) = ( `' r " { z } ) )
11 10 fveq2d 
 |-  ( y = z -> ( F ` ( `' r " { y } ) ) = ( F ` ( `' r " { z } ) ) )
12 id 
 |-  ( y = z -> y = z )
13 11 12 eqeq12d 
 |-  ( y = z -> ( ( F ` ( `' r " { y } ) ) = y <-> ( F ` ( `' r " { z } ) ) = z ) )
14 13 cbvralvw 
 |-  ( A. y e. x ( F ` ( `' r " { y } ) ) = y <-> A. z e. x ( F ` ( `' r " { z } ) ) = z )
15 4 cnveqd 
 |-  ( ( x = a /\ r = s ) -> `' r = `' s )
16 15 imaeq1d 
 |-  ( ( x = a /\ r = s ) -> ( `' r " { z } ) = ( `' s " { z } ) )
17 16 fveqeq2d 
 |-  ( ( x = a /\ r = s ) -> ( ( F ` ( `' r " { z } ) ) = z <-> ( F ` ( `' s " { z } ) ) = z ) )
18 2 17 raleqbidv 
 |-  ( ( x = a /\ r = s ) -> ( A. z e. x ( F ` ( `' r " { z } ) ) = z <-> A. z e. a ( F ` ( `' s " { z } ) ) = z ) )
19 14 18 bitrid 
 |-  ( ( x = a /\ r = s ) -> ( A. y e. x ( F ` ( `' r " { y } ) ) = y <-> A. z e. a ( F ` ( `' s " { z } ) ) = z ) )
20 8 19 anbi12d 
 |-  ( ( x = a /\ r = s ) -> ( ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) <-> ( s We a /\ A. z e. a ( F ` ( `' s " { z } ) ) = z ) ) )
21 7 20 anbi12d 
 |-  ( ( x = a /\ r = s ) -> ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) <-> ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( F ` ( `' s " { z } ) ) = z ) ) ) )
22 21 cbvopabv 
 |-  { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) } = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( F ` ( `' s " { z } ) ) = z ) ) }
23 1 22 eqtri 
 |-  W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( F ` ( `' s " { z } ) ) = z ) ) }