Metamath Proof Explorer

Theorem fpwwelem

Description: Lemma for fpwwe . (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe.1 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
fpwwe.2 
|- ( ph -> A e. V )
Assertion fpwwelem 
|- ( ph -> ( X W R <-> ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) )

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 fpwwe.2 
 |-  ( ph -> A e. V )
3 1 relopabiv 
 |-  Rel W
4 3 a1i 
 |-  ( ph -> Rel W )
5 brrelex12 
 |-  ( ( Rel W /\ X W R ) -> ( X e. _V /\ R e. _V ) )
6 4 5 sylan 
 |-  ( ( ph /\ X W R ) -> ( X e. _V /\ R e. _V ) )
7 2 adantr 
 |-  ( ( ph /\ ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) -> A e. V )
8 simprll 
 |-  ( ( ph /\ ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) -> X C_ A )
9 7 8 ssexd 
 |-  ( ( ph /\ ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) -> X e. _V )
10 9 9 xpexd 
 |-  ( ( ph /\ ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) -> ( X X. X ) e. _V )
11 simprlr 
 |-  ( ( ph /\ ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) -> R C_ ( X X. X ) )
12 10 11 ssexd 
 |-  ( ( ph /\ ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) -> R e. _V )
13 9 12 jca 
 |-  ( ( ph /\ ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) -> ( X e. _V /\ R e. _V ) )
14 simpl 
 |-  ( ( x = X /\ r = R ) -> x = X )
15 14 sseq1d 
 |-  ( ( x = X /\ r = R ) -> ( x C_ A <-> X C_ A ) )
16 simpr 
 |-  ( ( x = X /\ r = R ) -> r = R )
17 14 sqxpeqd 
 |-  ( ( x = X /\ r = R ) -> ( x X. x ) = ( X X. X ) )
18 16 17 sseq12d 
 |-  ( ( x = X /\ r = R ) -> ( r C_ ( x X. x ) <-> R C_ ( X X. X ) ) )
19 15 18 anbi12d 
 |-  ( ( x = X /\ r = R ) -> ( ( x C_ A /\ r C_ ( x X. x ) ) <-> ( X C_ A /\ R C_ ( X X. X ) ) ) )
20 weeq2 
 |-  ( x = X -> ( r We x <-> r We X ) )
21 weeq1 
 |-  ( r = R -> ( r We X <-> R We X ) )
22 20 21 sylan9bb 
 |-  ( ( x = X /\ r = R ) -> ( r We x <-> R We X ) )
23 16 cnveqd 
 |-  ( ( x = X /\ r = R ) -> `' r = `' R )
24 23 imaeq1d 
 |-  ( ( x = X /\ r = R ) -> ( `' r " { y } ) = ( `' R " { y } ) )
25 24 fveqeq2d 
 |-  ( ( x = X /\ r = R ) -> ( ( F ` ( `' r " { y } ) ) = y <-> ( F ` ( `' R " { y } ) ) = y ) )
26 14 25 raleqbidv 
 |-  ( ( x = X /\ r = R ) -> ( A. y e. x ( F ` ( `' r " { y } ) ) = y <-> A. y e. X ( F ` ( `' R " { y } ) ) = y ) )
27 22 26 anbi12d 
 |-  ( ( x = X /\ r = R ) -> ( ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) <-> ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) )
28 19 27 anbi12d 
 |-  ( ( x = X /\ r = R ) -> ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) <-> ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) )
29 28 1 brabga 
 |-  ( ( X e. _V /\ R e. _V ) -> ( X W R <-> ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) )
30 6 13 29 pm5.21nd 
 |-  ( ph -> ( X W R <-> ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) )