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 relopabiv
 |-  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 ) )