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

Metamath Proof Explorer

Theorem fpwwe2lem3

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 )
fpwwe2lem3.4 
|- ( ph -> X W R )
Assertion fpwwe2lem3 
|- ( ( ph /\ B e. X ) -> ( ( `' R " { B } ) F ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) ) = B )

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 fpwwe2lem3.4 
 |-  ( ph -> X W R )
4 1 2 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 ) ) ) )
5 3 4 mpbid 
 |-  ( 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 ) ) )
6 5 simprrd 
 |-  ( ph -> A. y e. X [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y )
7 sneq 
 |-  ( y = B -> { y } = { B } )
8 7 imaeq2d 
 |-  ( y = B -> ( `' R " { y } ) = ( `' R " { B } ) )
9 eqeq2 
 |-  ( y = B -> ( ( u F ( R i^i ( u X. u ) ) ) = y <-> ( u F ( R i^i ( u X. u ) ) ) = B ) )
10 8 9 sbceqbid 
 |-  ( y = B -> ( [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y <-> [. ( `' R " { B } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = B ) )
11 10 rspccva 
 |-  ( ( A. y e. X [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y /\ B e. X ) -> [. ( `' R " { B } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = B )
12 6 11 sylan 
 |-  ( ( ph /\ B e. X ) -> [. ( `' R " { B } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = B )
13 cnvimass 
 |-  ( `' R " { B } ) C_ dom R
14 1 relopabiv 
 |-  Rel W
15 14 brrelex2i 
 |-  ( X W R -> R e. _V )
16 dmexg 
 |-  ( R e. _V -> dom R e. _V )
17 3 15 16 3syl 
 |-  ( ph -> dom R e. _V )
18 ssexg 
 |-  ( ( ( `' R " { B } ) C_ dom R /\ dom R e. _V ) -> ( `' R " { B } ) e. _V )
19 13 17 18 sylancr 
 |-  ( ph -> ( `' R " { B } ) e. _V )
20 id 
 |-  ( u = ( `' R " { B } ) -> u = ( `' R " { B } ) )
21 20 sqxpeqd 
 |-  ( u = ( `' R " { B } ) -> ( u X. u ) = ( ( `' R " { B } ) X. ( `' R " { B } ) ) )
22 21 ineq2d 
 |-  ( u = ( `' R " { B } ) -> ( R i^i ( u X. u ) ) = ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) )
23 20 22 oveq12d 
 |-  ( u = ( `' R " { B } ) -> ( u F ( R i^i ( u X. u ) ) ) = ( ( `' R " { B } ) F ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) ) )
24 23 eqeq1d 
 |-  ( u = ( `' R " { B } ) -> ( ( u F ( R i^i ( u X. u ) ) ) = B <-> ( ( `' R " { B } ) F ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) ) = B ) )
25 24 sbcieg 
 |-  ( ( `' R " { B } ) e. _V -> ( [. ( `' R " { B } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = B <-> ( ( `' R " { B } ) F ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) ) = B ) )
26 19 25 syl 
 |-  ( ph -> ( [. ( `' R " { B } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = B <-> ( ( `' R " { B } ) F ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) ) = B ) )
27 26 adantr 
 |-  ( ( ph /\ B e. X ) -> ( [. ( `' R " { B } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = B <-> ( ( `' R " { B } ) F ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) ) = B ) )
28 12 27 mpbid 
 |-  ( ( ph /\ B e. X ) -> ( ( `' R " { B } ) F ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) ) = B )