Metamath Proof Explorer


Theorem fpwwe2lem4

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024) (Proof shortened by Matthew House, 10-Sep-2025)

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 simpl
 |-  ( ( x = X /\ r = R ) -> x = X )
11 10 sseq1d
 |-  ( ( x = X /\ r = R ) -> ( x C_ A <-> X C_ A ) )
12 simpr
 |-  ( ( x = X /\ r = R ) -> r = R )
13 10 sqxpeqd
 |-  ( ( x = X /\ r = R ) -> ( x X. x ) = ( X X. X ) )
14 12 13 sseq12d
 |-  ( ( x = X /\ r = R ) -> ( r C_ ( x X. x ) <-> R C_ ( X X. X ) ) )
15 12 10 weeq12d
 |-  ( ( x = X /\ r = R ) -> ( r We x <-> R We X ) )
16 11 14 15 3anbi123d
 |-  ( ( x = X /\ r = R ) -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) )
17 oveq12
 |-  ( ( x = X /\ r = R ) -> ( x F r ) = ( X F R ) )
18 17 eleq1d
 |-  ( ( x = X /\ r = R ) -> ( ( x F r ) e. A <-> ( X F R ) e. A ) )
19 16 18 imbi12d
 |-  ( ( x = X /\ r = R ) -> ( ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x F r ) e. A ) <-> ( ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) -> ( X F R ) e. A ) ) )
20 3 ex
 |-  ( ph -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x F r ) e. A ) )
21 20 adantr
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x F r ) e. A ) )
22 6 9 19 21 vtocl2d
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) -> ( X F R ) e. A ) )
23 22 syldbl2
 |-  ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( X F R ) e. A )