Metamath Proof Explorer

Theorem fpwwe2lem10

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 )
fpwwe2.4 
|- X = U. dom W
Assertion fpwwe2lem10 
|- ( ph -> W : dom W --> ~P ( X X. X ) )

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 fpwwe2.4 
 |-  X = U. dom W
5 1 relopabi 
 |-  Rel W
6 5 a1i 
 |-  ( ph -> Rel W )
7 simprr 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( w C_ w /\ s = ( t i^i ( w X. w ) ) ) ) -> s = ( t i^i ( w X. w ) ) )
8 1 2 fpwwe2lem2 
 |-  ( ph -> ( w W t <-> ( ( w C_ A /\ t C_ ( w X. w ) ) /\ ( t We w /\ A. y e. w [. ( `' t " { y } ) / u ]. ( u F ( t i^i ( u X. u ) ) ) = y ) ) ) )
9 8 simprbda 
 |-  ( ( ph /\ w W t ) -> ( w C_ A /\ t C_ ( w X. w ) ) )
10 9 simprd 
 |-  ( ( ph /\ w W t ) -> t C_ ( w X. w ) )
11 10 adantrl 
 |-  ( ( ph /\ ( w W s /\ w W t ) ) -> t C_ ( w X. w ) )
12 11 adantr 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( w C_ w /\ s = ( t i^i ( w X. w ) ) ) ) -> t C_ ( w X. w ) )
13 df-ss 
 |-  ( t C_ ( w X. w ) <-> ( t i^i ( w X. w ) ) = t )
14 12 13 sylib 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( w C_ w /\ s = ( t i^i ( w X. w ) ) ) ) -> ( t i^i ( w X. w ) ) = t )
15 7 14 eqtrd 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( w C_ w /\ s = ( t i^i ( w X. w ) ) ) ) -> s = t )
16 simprr 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( w C_ w /\ t = ( s i^i ( w X. w ) ) ) ) -> t = ( s i^i ( w X. w ) ) )
17 1 2 fpwwe2lem2 
 |-  ( ph -> ( w W s <-> ( ( w C_ A /\ s C_ ( w X. w ) ) /\ ( s We w /\ A. y e. w [. ( `' s " { y } ) / u ]. ( u F ( s i^i ( u X. u ) ) ) = y ) ) ) )
18 17 simprbda 
 |-  ( ( ph /\ w W s ) -> ( w C_ A /\ s C_ ( w X. w ) ) )
19 18 simprd 
 |-  ( ( ph /\ w W s ) -> s C_ ( w X. w ) )
20 19 adantrr 
 |-  ( ( ph /\ ( w W s /\ w W t ) ) -> s C_ ( w X. w ) )
21 20 adantr 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( w C_ w /\ t = ( s i^i ( w X. w ) ) ) ) -> s C_ ( w X. w ) )
22 df-ss 
 |-  ( s C_ ( w X. w ) <-> ( s i^i ( w X. w ) ) = s )
23 21 22 sylib 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( w C_ w /\ t = ( s i^i ( w X. w ) ) ) ) -> ( s i^i ( w X. w ) ) = s )
24 16 23 eqtr2d 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( w C_ w /\ t = ( s i^i ( w X. w ) ) ) ) -> s = t )
25 2 adantr 
 |-  ( ( ph /\ ( w W s /\ w W t ) ) -> A e. V )
26 3 adantlr 
 |-  ( ( ( ph /\ ( w W s /\ w W t ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
27 simprl 
 |-  ( ( ph /\ ( w W s /\ w W t ) ) -> w W s )
28 simprr 
 |-  ( ( ph /\ ( w W s /\ w W t ) ) -> w W t )
29 1 25 26 27 28 fpwwe2lem9 
 |-  ( ( ph /\ ( w W s /\ w W t ) ) -> ( ( w C_ w /\ s = ( t i^i ( w X. w ) ) ) \/ ( w C_ w /\ t = ( s i^i ( w X. w ) ) ) ) )
30 15 24 29 mpjaodan 
 |-  ( ( ph /\ ( w W s /\ w W t ) ) -> s = t )
31 30 ex 
 |-  ( ph -> ( ( w W s /\ w W t ) -> s = t ) )
32 31 alrimiv 
 |-  ( ph -> A. t ( ( w W s /\ w W t ) -> s = t ) )
33 32 alrimivv 
 |-  ( ph -> A. w A. s A. t ( ( w W s /\ w W t ) -> s = t ) )
34 dffun2 
 |-  ( Fun W <-> ( Rel W /\ A. w A. s A. t ( ( w W s /\ w W t ) -> s = t ) ) )
35 6 33 34 sylanbrc 
 |-  ( ph -> Fun W )
36 35 funfnd 
 |-  ( ph -> W Fn dom W )
37 vex 
 |-  s e. _V
38 37 elrn 
 |-  ( s e. ran W <-> E. w w W s )
39 5 releldmi 
 |-  ( w W s -> w e. dom W )
40 39 adantl 
 |-  ( ( ph /\ w W s ) -> w e. dom W )
41 elssuni 
 |-  ( w e. dom W -> w C_ U. dom W )
42 40 41 syl 
 |-  ( ( ph /\ w W s ) -> w C_ U. dom W )
43 42 4 sseqtrrdi 
 |-  ( ( ph /\ w W s ) -> w C_ X )
44 xpss12 
 |-  ( ( w C_ X /\ w C_ X ) -> ( w X. w ) C_ ( X X. X ) )
45 43 43 44 syl2anc 
 |-  ( ( ph /\ w W s ) -> ( w X. w ) C_ ( X X. X ) )
46 19 45 sstrd 
 |-  ( ( ph /\ w W s ) -> s C_ ( X X. X ) )
47 46 ex 
 |-  ( ph -> ( w W s -> s C_ ( X X. X ) ) )
48 velpw 
 |-  ( s e. ~P ( X X. X ) <-> s C_ ( X X. X ) )
49 47 48 syl6ibr 
 |-  ( ph -> ( w W s -> s e. ~P ( X X. X ) ) )
50 49 exlimdv 
 |-  ( ph -> ( E. w w W s -> s e. ~P ( X X. X ) ) )
51 38 50 syl5bi 
 |-  ( ph -> ( s e. ran W -> s e. ~P ( X X. X ) ) )
52 51 ssrdv 
 |-  ( ph -> ran W C_ ~P ( X X. X ) )
53 df-f 
 |-  ( W : dom W --> ~P ( X X. X ) <-> ( W Fn dom W /\ ran W C_ ~P ( X X. X ) ) )
54 36 52 53 sylanbrc 
 |-  ( ph -> W : dom W --> ~P ( X X. X ) )