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