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 2 3 4
|
fpwwe2lem10 |
|- ( ph -> W : dom W --> ~P ( X X. X ) ) |
6 |
5
|
ffund |
|- ( ph -> Fun W ) |
7 |
|
funbrfv2b |
|- ( Fun W -> ( Y W R <-> ( Y e. dom W /\ ( W ` Y ) = R ) ) ) |
8 |
6 7
|
syl |
|- ( ph -> ( Y W R <-> ( Y e. dom W /\ ( W ` Y ) = R ) ) ) |
9 |
8
|
simprbda |
|- ( ( ph /\ Y W R ) -> Y e. dom W ) |
10 |
9
|
adantrr |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y e. dom W ) |
11 |
|
elssuni |
|- ( Y e. dom W -> Y C_ U. dom W ) |
12 |
11 4
|
sseqtrrdi |
|- ( Y e. dom W -> Y C_ X ) |
13 |
10 12
|
syl |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y C_ X ) |
14 |
|
simpl |
|- ( ( X C_ Y /\ ( W ` X ) = ( R i^i ( Y X. X ) ) ) -> X C_ Y ) |
15 |
14
|
a1i |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( X C_ Y /\ ( W ` X ) = ( R i^i ( Y X. X ) ) ) -> X C_ Y ) ) |
16 |
|
simplrr |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( Y F R ) e. Y ) |
17 |
2
|
adantr |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> A e. V ) |
18 |
17
|
adantr |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> A e. V ) |
19 |
1 2 3 4
|
fpwwe2lem11 |
|- ( ph -> X e. dom W ) |
20 |
|
funfvbrb |
|- ( Fun W -> ( X e. dom W <-> X W ( W ` X ) ) ) |
21 |
6 20
|
syl |
|- ( ph -> ( X e. dom W <-> X W ( W ` X ) ) ) |
22 |
19 21
|
mpbid |
|- ( ph -> X W ( W ` X ) ) |
23 |
1 2
|
fpwwe2lem2 |
|- ( ph -> ( X W ( W ` X ) <-> ( ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) /\ ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) ) ) ) |
24 |
22 23
|
mpbid |
|- ( ph -> ( ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) /\ ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) ) ) |
25 |
24
|
ad2antrr |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) /\ ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) ) ) |
26 |
25
|
simpld |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) ) |
27 |
26
|
simpld |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> X C_ A ) |
28 |
18 27
|
ssexd |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> X e. _V ) |
29 |
|
difexg |
|- ( X e. _V -> ( X \ Y ) e. _V ) |
30 |
28 29
|
syl |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X \ Y ) e. _V ) |
31 |
25
|
simprd |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) ) |
32 |
31
|
simpld |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( W ` X ) We X ) |
33 |
|
wefr |
|- ( ( W ` X ) We X -> ( W ` X ) Fr X ) |
34 |
32 33
|
syl |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( W ` X ) Fr X ) |
35 |
|
difssd |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X \ Y ) C_ X ) |
36 |
|
fri |
|- ( ( ( ( X \ Y ) e. _V /\ ( W ` X ) Fr X ) /\ ( ( X \ Y ) C_ X /\ ( X \ Y ) =/= (/) ) ) -> E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z ) |
37 |
36
|
expr |
|- ( ( ( ( X \ Y ) e. _V /\ ( W ` X ) Fr X ) /\ ( X \ Y ) C_ X ) -> ( ( X \ Y ) =/= (/) -> E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z ) ) |
38 |
30 34 35 37
|
syl21anc |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( X \ Y ) =/= (/) -> E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z ) ) |
39 |
|
ssdif0 |
|- ( ( X i^i ( `' ( W ` X ) " { z } ) ) C_ Y <-> ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y ) = (/) ) |
40 |
|
indif1 |
|- ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y ) |
41 |
40
|
eqeq1i |
|- ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y ) = (/) ) |
42 |
|
disj |
|- ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> A. w e. ( X \ Y ) -. w e. ( `' ( W ` X ) " { z } ) ) |
43 |
|
vex |
|- w e. _V |
44 |
43
|
eliniseg |
|- ( z e. _V -> ( w e. ( `' ( W ` X ) " { z } ) <-> w ( W ` X ) z ) ) |
45 |
44
|
elv |
|- ( w e. ( `' ( W ` X ) " { z } ) <-> w ( W ` X ) z ) |
46 |
45
|
notbii |
|- ( -. w e. ( `' ( W ` X ) " { z } ) <-> -. w ( W ` X ) z ) |
47 |
46
|
ralbii |
|- ( A. w e. ( X \ Y ) -. w e. ( `' ( W ` X ) " { z } ) <-> A. w e. ( X \ Y ) -. w ( W ` X ) z ) |
48 |
42 47
|
bitri |
|- ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> A. w e. ( X \ Y ) -. w ( W ` X ) z ) |
49 |
39 41 48
|
3bitr2i |
|- ( ( X i^i ( `' ( W ` X ) " { z } ) ) C_ Y <-> A. w e. ( X \ Y ) -. w ( W ` X ) z ) |
50 |
|
cnvimass |
|- ( `' ( W ` X ) " { z } ) C_ dom ( W ` X ) |
51 |
26
|
simprd |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( W ` X ) C_ ( X X. X ) ) |
52 |
|
dmss |
|- ( ( W ` X ) C_ ( X X. X ) -> dom ( W ` X ) C_ dom ( X X. X ) ) |
53 |
51 52
|
syl |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> dom ( W ` X ) C_ dom ( X X. X ) ) |
54 |
|
dmxpid |
|- dom ( X X. X ) = X |
55 |
53 54
|
sseqtrdi |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> dom ( W ` X ) C_ X ) |
56 |
50 55
|
sstrid |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( `' ( W ` X ) " { z } ) C_ X ) |
57 |
|
sseqin2 |
|- ( ( `' ( W ` X ) " { z } ) C_ X <-> ( X i^i ( `' ( W ` X ) " { z } ) ) = ( `' ( W ` X ) " { z } ) ) |
58 |
56 57
|
sylib |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X i^i ( `' ( W ` X ) " { z } ) ) = ( `' ( W ` X ) " { z } ) ) |
59 |
58
|
sseq1d |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( X i^i ( `' ( W ` X ) " { z } ) ) C_ Y <-> ( `' ( W ` X ) " { z } ) C_ Y ) ) |
60 |
49 59
|
bitr3id |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( A. w e. ( X \ Y ) -. w ( W ` X ) z <-> ( `' ( W ` X ) " { z } ) C_ Y ) ) |
61 |
60
|
rexbidv |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z <-> E. z e. ( X \ Y ) ( `' ( W ` X ) " { z } ) C_ Y ) ) |
62 |
|
eldifn |
|- ( z e. ( X \ Y ) -> -. z e. Y ) |
63 |
62
|
ad2antrl |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> -. z e. Y ) |
64 |
|
eleq1w |
|- ( w = z -> ( w e. Y <-> z e. Y ) ) |
65 |
64
|
notbid |
|- ( w = z -> ( -. w e. Y <-> -. z e. Y ) ) |
66 |
63 65
|
syl5ibrcom |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( w = z -> -. w e. Y ) ) |
67 |
66
|
con2d |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( w e. Y -> -. w = z ) ) |
68 |
67
|
imp |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> -. w = z ) |
69 |
63
|
adantr |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> -. z e. Y ) |
70 |
|
simprr |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> R = ( ( W ` X ) i^i ( X X. Y ) ) ) |
71 |
70
|
ad2antrr |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> R = ( ( W ` X ) i^i ( X X. Y ) ) ) |
72 |
71
|
breqd |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z R w <-> z ( ( W ` X ) i^i ( X X. Y ) ) w ) ) |
73 |
|
eldifi |
|- ( z e. ( X \ Y ) -> z e. X ) |
74 |
73
|
ad2antrl |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> z e. X ) |
75 |
74
|
adantr |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> z e. X ) |
76 |
|
simpr |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> w e. Y ) |
77 |
|
brxp |
|- ( z ( X X. Y ) w <-> ( z e. X /\ w e. Y ) ) |
78 |
75 76 77
|
sylanbrc |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> z ( X X. Y ) w ) |
79 |
|
brin |
|- ( z ( ( W ` X ) i^i ( X X. Y ) ) w <-> ( z ( W ` X ) w /\ z ( X X. Y ) w ) ) |
80 |
79
|
rbaib |
|- ( z ( X X. Y ) w -> ( z ( ( W ` X ) i^i ( X X. Y ) ) w <-> z ( W ` X ) w ) ) |
81 |
78 80
|
syl |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z ( ( W ` X ) i^i ( X X. Y ) ) w <-> z ( W ` X ) w ) ) |
82 |
72 81
|
bitrd |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z R w <-> z ( W ` X ) w ) ) |
83 |
1 2
|
fpwwe2lem2 |
|- ( ph -> ( Y W R <-> ( ( Y C_ A /\ R C_ ( Y X. Y ) ) /\ ( R We Y /\ A. y e. Y [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) ) ) |
84 |
83
|
biimpa |
|- ( ( ph /\ Y W R ) -> ( ( Y C_ A /\ R C_ ( Y X. Y ) ) /\ ( R We Y /\ A. y e. Y [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) ) |
85 |
84
|
adantrr |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( Y C_ A /\ R C_ ( Y X. Y ) ) /\ ( R We Y /\ A. y e. Y [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) ) |
86 |
85
|
simpld |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( Y C_ A /\ R C_ ( Y X. Y ) ) ) |
87 |
86
|
simprd |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> R C_ ( Y X. Y ) ) |
88 |
87
|
ad5ant12 |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> R C_ ( Y X. Y ) ) |
89 |
88
|
ssbrd |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z R w -> z ( Y X. Y ) w ) ) |
90 |
|
brxp |
|- ( z ( Y X. Y ) w <-> ( z e. Y /\ w e. Y ) ) |
91 |
90
|
simplbi |
|- ( z ( Y X. Y ) w -> z e. Y ) |
92 |
89 91
|
syl6 |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z R w -> z e. Y ) ) |
93 |
82 92
|
sylbird |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z ( W ` X ) w -> z e. Y ) ) |
94 |
69 93
|
mtod |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> -. z ( W ` X ) w ) |
95 |
32
|
ad2antrr |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( W ` X ) We X ) |
96 |
|
weso |
|- ( ( W ` X ) We X -> ( W ` X ) Or X ) |
97 |
95 96
|
syl |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( W ` X ) Or X ) |
98 |
13
|
ad2antrr |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> Y C_ X ) |
99 |
98
|
sselda |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> w e. X ) |
100 |
|
sotric |
|- ( ( ( W ` X ) Or X /\ ( w e. X /\ z e. X ) ) -> ( w ( W ` X ) z <-> -. ( w = z \/ z ( W ` X ) w ) ) ) |
101 |
|
ioran |
|- ( -. ( w = z \/ z ( W ` X ) w ) <-> ( -. w = z /\ -. z ( W ` X ) w ) ) |
102 |
100 101
|
bitrdi |
|- ( ( ( W ` X ) Or X /\ ( w e. X /\ z e. X ) ) -> ( w ( W ` X ) z <-> ( -. w = z /\ -. z ( W ` X ) w ) ) ) |
103 |
97 99 75 102
|
syl12anc |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( w ( W ` X ) z <-> ( -. w = z /\ -. z ( W ` X ) w ) ) ) |
104 |
68 94 103
|
mpbir2and |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> w ( W ` X ) z ) |
105 |
104 45
|
sylibr |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> w e. ( `' ( W ` X ) " { z } ) ) |
106 |
105
|
ex |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( w e. Y -> w e. ( `' ( W ` X ) " { z } ) ) ) |
107 |
106
|
ssrdv |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> Y C_ ( `' ( W ` X ) " { z } ) ) |
108 |
|
simprr |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( `' ( W ` X ) " { z } ) C_ Y ) |
109 |
107 108
|
eqssd |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> Y = ( `' ( W ` X ) " { z } ) ) |
110 |
|
in32 |
|- ( ( ( W ` X ) i^i ( X X. Y ) ) i^i ( Y X. Y ) ) = ( ( ( W ` X ) i^i ( Y X. Y ) ) i^i ( X X. Y ) ) |
111 |
|
simplrr |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> R = ( ( W ` X ) i^i ( X X. Y ) ) ) |
112 |
111
|
ineq1d |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( R i^i ( Y X. Y ) ) = ( ( ( W ` X ) i^i ( X X. Y ) ) i^i ( Y X. Y ) ) ) |
113 |
87
|
ad2antrr |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> R C_ ( Y X. Y ) ) |
114 |
|
df-ss |
|- ( R C_ ( Y X. Y ) <-> ( R i^i ( Y X. Y ) ) = R ) |
115 |
113 114
|
sylib |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( R i^i ( Y X. Y ) ) = R ) |
116 |
112 115
|
eqtr3d |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( ( W ` X ) i^i ( X X. Y ) ) i^i ( Y X. Y ) ) = R ) |
117 |
|
inss2 |
|- ( ( W ` X ) i^i ( Y X. Y ) ) C_ ( Y X. Y ) |
118 |
|
xpss1 |
|- ( Y C_ X -> ( Y X. Y ) C_ ( X X. Y ) ) |
119 |
98 118
|
syl |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( Y X. Y ) C_ ( X X. Y ) ) |
120 |
117 119
|
sstrid |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( W ` X ) i^i ( Y X. Y ) ) C_ ( X X. Y ) ) |
121 |
|
df-ss |
|- ( ( ( W ` X ) i^i ( Y X. Y ) ) C_ ( X X. Y ) <-> ( ( ( W ` X ) i^i ( Y X. Y ) ) i^i ( X X. Y ) ) = ( ( W ` X ) i^i ( Y X. Y ) ) ) |
122 |
120 121
|
sylib |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( ( W ` X ) i^i ( Y X. Y ) ) i^i ( X X. Y ) ) = ( ( W ` X ) i^i ( Y X. Y ) ) ) |
123 |
110 116 122
|
3eqtr3a |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> R = ( ( W ` X ) i^i ( Y X. Y ) ) ) |
124 |
109
|
sqxpeqd |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( Y X. Y ) = ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) |
125 |
124
|
ineq2d |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( W ` X ) i^i ( Y X. Y ) ) = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) ) |
126 |
123 125
|
eqtrd |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> R = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) ) |
127 |
109 126
|
oveq12d |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( Y F R ) = ( ( `' ( W ` X ) " { z } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) ) ) |
128 |
18
|
adantr |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> A e. V ) |
129 |
22
|
adantr |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X W ( W ` X ) ) |
130 |
129
|
ad2antrr |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> X W ( W ` X ) ) |
131 |
1 128 130
|
fpwwe2lem3 |
|- ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ z e. X ) -> ( ( `' ( W ` X ) " { z } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) ) = z ) |
132 |
74 131
|
mpdan |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( `' ( W ` X ) " { z } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) ) = z ) |
133 |
127 132
|
eqtrd |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( Y F R ) = z ) |
134 |
133 63
|
eqneltrd |
|- ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> -. ( Y F R ) e. Y ) |
135 |
134
|
rexlimdvaa |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( E. z e. ( X \ Y ) ( `' ( W ` X ) " { z } ) C_ Y -> -. ( Y F R ) e. Y ) ) |
136 |
61 135
|
sylbid |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z -> -. ( Y F R ) e. Y ) ) |
137 |
38 136
|
syld |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( X \ Y ) =/= (/) -> -. ( Y F R ) e. Y ) ) |
138 |
137
|
necon4ad |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( Y F R ) e. Y -> ( X \ Y ) = (/) ) ) |
139 |
16 138
|
mpd |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X \ Y ) = (/) ) |
140 |
|
ssdif0 |
|- ( X C_ Y <-> ( X \ Y ) = (/) ) |
141 |
139 140
|
sylibr |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> X C_ Y ) |
142 |
141
|
ex |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) -> X C_ Y ) ) |
143 |
3
|
adantlr |
|- ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A ) |
144 |
|
simprl |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y W R ) |
145 |
1 17 143 129 144
|
fpwwe2lem9 |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( X C_ Y /\ ( W ` X ) = ( R i^i ( Y X. X ) ) ) \/ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) ) |
146 |
15 142 145
|
mpjaod |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X C_ Y ) |
147 |
13 146
|
eqssd |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y = X ) |
148 |
6
|
adantr |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Fun W ) |
149 |
147 144
|
eqbrtrrd |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X W R ) |
150 |
|
funbrfv |
|- ( Fun W -> ( X W R -> ( W ` X ) = R ) ) |
151 |
148 149 150
|
sylc |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( W ` X ) = R ) |
152 |
151
|
eqcomd |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> R = ( W ` X ) ) |
153 |
147 152
|
jca |
|- ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( Y = X /\ R = ( W ` X ) ) ) |
154 |
153
|
ex |
|- ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) -> ( Y = X /\ R = ( W ` X ) ) ) ) |
155 |
1 2 3 4
|
fpwwe2lem12 |
|- ( ph -> ( X F ( W ` X ) ) e. X ) |
156 |
22 155
|
jca |
|- ( ph -> ( X W ( W ` X ) /\ ( X F ( W ` X ) ) e. X ) ) |
157 |
|
breq12 |
|- ( ( Y = X /\ R = ( W ` X ) ) -> ( Y W R <-> X W ( W ` X ) ) ) |
158 |
|
oveq12 |
|- ( ( Y = X /\ R = ( W ` X ) ) -> ( Y F R ) = ( X F ( W ` X ) ) ) |
159 |
|
simpl |
|- ( ( Y = X /\ R = ( W ` X ) ) -> Y = X ) |
160 |
158 159
|
eleq12d |
|- ( ( Y = X /\ R = ( W ` X ) ) -> ( ( Y F R ) e. Y <-> ( X F ( W ` X ) ) e. X ) ) |
161 |
157 160
|
anbi12d |
|- ( ( Y = X /\ R = ( W ` X ) ) -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( X W ( W ` X ) /\ ( X F ( W ` X ) ) e. X ) ) ) |
162 |
156 161
|
syl5ibrcom |
|- ( ph -> ( ( Y = X /\ R = ( W ` X ) ) -> ( Y W R /\ ( Y F R ) e. Y ) ) ) |
163 |
154 162
|
impbid |
|- ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) ) |