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