Metamath Proof Explorer

Theorem fpwwe2lem4

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-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 )
fpwwe2.3 
|- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
Assertion fpwwe2lem4 
|- ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( X F R ) e. A )

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 fpwwe2.3 
 |-  ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
4 2 adantr 
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> A e. V )
5 simpr1 
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> X C_ A )
6 4 5 ssexd 
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> X e. _V )
7 6 6 xpexd 
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( X X. X ) e. _V )
8 simpr2 
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> R C_ ( X X. X ) )
9 7 8 ssexd 
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> R e. _V )
10 6 9 jca 
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( X e. _V /\ R e. _V ) )
11 sseq1 
 |-  ( x = X -> ( x C_ A <-> X C_ A ) )
12 xpeq12 
 |-  ( ( x = X /\ x = X ) -> ( x X. x ) = ( X X. X ) )
13 12 anidms 
 |-  ( x = X -> ( x X. x ) = ( X X. X ) )
14 13 sseq2d 
 |-  ( x = X -> ( r C_ ( x X. x ) <-> r C_ ( X X. X ) ) )
15 weeq2 
 |-  ( x = X -> ( r We x <-> r We X ) )
16 11 14 15 3anbi123d 
 |-  ( x = X -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( X C_ A /\ r C_ ( X X. X ) /\ r We X ) ) )
17 16 anbi2d 
 |-  ( x = X -> ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) <-> ( ph /\ ( X C_ A /\ r C_ ( X X. X ) /\ r We X ) ) ) )
18 oveq1 
 |-  ( x = X -> ( x F r ) = ( X F r ) )
19 18 eleq1d 
 |-  ( x = X -> ( ( x F r ) e. A <-> ( X F r ) e. A ) )
20 17 19 imbi12d 
 |-  ( x = X -> ( ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A ) <-> ( ( ph /\ ( X C_ A /\ r C_ ( X X. X ) /\ r We X ) ) -> ( X F r ) e. A ) ) )
21 sseq1 
 |-  ( r = R -> ( r C_ ( X X. X ) <-> R C_ ( X X. X ) ) )
22 weeq1 
 |-  ( r = R -> ( r We X <-> R We X ) )
23 21 22 3anbi23d 
 |-  ( r = R -> ( ( X C_ A /\ r C_ ( X X. X ) /\ r We X ) <-> ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) )
24 23 anbi2d 
 |-  ( r = R -> ( ( ph /\ ( X C_ A /\ r C_ ( X X. X ) /\ r We X ) ) <-> ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) ) )
25 oveq2 
 |-  ( r = R -> ( X F r ) = ( X F R ) )
26 25 eleq1d 
 |-  ( r = R -> ( ( X F r ) e. A <-> ( X F R ) e. A ) )
27 24 26 imbi12d 
 |-  ( r = R -> ( ( ( ph /\ ( X C_ A /\ r C_ ( X X. X ) /\ r We X ) ) -> ( X F r ) e. A ) <-> ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( X F R ) e. A ) ) )
28 20 27 3 vtocl2g 
 |-  ( ( X e. _V /\ R e. _V ) -> ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( X F R ) e. A ) )
29 10 28 mpcom 
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( X F R ) e. A )