This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fpwwe2lem2

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

Ref Expression
Hypotheses 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 ) ) }
fpwwe2.2 
|- ( ph -> A e. V )
Assertion fpwwe2lem2 
|- ( ph -> ( X W 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 ) ) ) )

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 fpwwe2.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 [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) ) -> A e. V )
8 simprll 
 |-  ( ( ph /\ ( ( 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 ) ) ) -> X C_ A )
9 7 8 ssexd 
 |-  ( ( ph /\ ( ( 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 ) ) ) -> X e. _V )
10 9 9 xpexd 
 |-  ( ( ph /\ ( ( 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 ) ) ) -> ( X X. X ) e. _V )
11 simprlr 
 |-  ( ( ph /\ ( ( 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 ) ) ) -> 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 [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) ) -> R e. _V )
13 9 12 jca 
 |-  ( ( ph /\ ( ( 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 ) ) ) -> ( 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 16 14 weeq12d 
 |-  ( ( x = X /\ r = R ) -> ( r We x <-> R We X ) )
21 16 cnveqd 
 |-  ( ( x = X /\ r = R ) -> `' r = `' R )
22 21 imaeq1d 
 |-  ( ( x = X /\ r = R ) -> ( `' r " { y } ) = ( `' R " { y } ) )
23 16 ineq1d 
 |-  ( ( x = X /\ r = R ) -> ( r i^i ( u X. u ) ) = ( R i^i ( u X. u ) ) )
24 23 oveq2d 
 |-  ( ( x = X /\ r = R ) -> ( u F ( r i^i ( u X. u ) ) ) = ( u F ( R i^i ( u X. u ) ) ) )
25 24 eqeq1d 
 |-  ( ( x = X /\ r = R ) -> ( ( u F ( r i^i ( u X. u ) ) ) = y <-> ( u F ( R i^i ( u X. u ) ) ) = y ) )
26 22 25 sbceqbid 
 |-  ( ( x = X /\ r = R ) -> ( [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y <-> [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) )
27 14 26 raleqbidv 
 |-  ( ( x = X /\ r = R ) -> ( A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y <-> A. y e. X [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) )
28 20 27 anbi12d 
 |-  ( ( x = X /\ r = R ) -> ( ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) <-> ( R We X /\ A. y e. X [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) )
29 19 28 anbi12d 
 |-  ( ( x = X /\ r = 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 ) ) <-> ( ( 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 ) ) ) )
30 29 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 [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) ) )
31 6 13 30 pm5.21nd 
 |-  ( ph -> ( X W 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 ) ) ) )