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

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 )