Step |
Hyp |
Ref |
Expression |
1 |
|
supsrlem.1 |
|- B = { w | ( C +R [ <. w , 1P >. ] ~R ) e. A } |
2 |
|
supsrlem.2 |
|- C e. R. |
3 |
|
0idsr |
|- ( C e. R. -> ( C +R 0R ) = C ) |
4 |
2 3
|
mp1i |
|- ( ( C e. A /\ E. x e. R. A. y e. A y ( C +R 0R ) = C ) |
5 |
|
simpl |
|- ( ( C e. A /\ E. x e. R. A. y e. A y C e. A ) |
6 |
4 5
|
eqeltrd |
|- ( ( C e. A /\ E. x e. R. A. y e. A y ( C +R 0R ) e. A ) |
7 |
|
1pr |
|- 1P e. P. |
8 |
7
|
elexi |
|- 1P e. _V |
9 |
|
opeq1 |
|- ( w = 1P -> <. w , 1P >. = <. 1P , 1P >. ) |
10 |
9
|
eceq1d |
|- ( w = 1P -> [ <. w , 1P >. ] ~R = [ <. 1P , 1P >. ] ~R ) |
11 |
|
df-0r |
|- 0R = [ <. 1P , 1P >. ] ~R |
12 |
10 11
|
eqtr4di |
|- ( w = 1P -> [ <. w , 1P >. ] ~R = 0R ) |
13 |
12
|
oveq2d |
|- ( w = 1P -> ( C +R [ <. w , 1P >. ] ~R ) = ( C +R 0R ) ) |
14 |
13
|
eleq1d |
|- ( w = 1P -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> ( C +R 0R ) e. A ) ) |
15 |
8 14 1
|
elab2 |
|- ( 1P e. B <-> ( C +R 0R ) e. A ) |
16 |
6 15
|
sylibr |
|- ( ( C e. A /\ E. x e. R. A. y e. A y 1P e. B ) |
17 |
16
|
ne0d |
|- ( ( C e. A /\ E. x e. R. A. y e. A y B =/= (/) ) |
18 |
|
breq1 |
|- ( y = C -> ( y C |
19 |
18
|
rspccv |
|- ( A. y e. A y ( C e. A -> C |
20 |
|
0lt1sr |
|- 0R |
21 |
|
m1r |
|- -1R e. R. |
22 |
|
ltasr |
|- ( -1R e. R. -> ( 0R ( -1R +R 0R ) |
23 |
21 22
|
ax-mp |
|- ( 0R ( -1R +R 0R ) |
24 |
20 23
|
mpbi |
|- ( -1R +R 0R ) |
25 |
|
0idsr |
|- ( -1R e. R. -> ( -1R +R 0R ) = -1R ) |
26 |
21 25
|
ax-mp |
|- ( -1R +R 0R ) = -1R |
27 |
|
m1p1sr |
|- ( -1R +R 1R ) = 0R |
28 |
24 26 27
|
3brtr3i |
|- -1R |
29 |
|
ltasr |
|- ( C e. R. -> ( -1R ( C +R -1R ) |
30 |
2 29
|
ax-mp |
|- ( -1R ( C +R -1R ) |
31 |
28 30
|
mpbi |
|- ( C +R -1R ) |
32 |
2 3
|
ax-mp |
|- ( C +R 0R ) = C |
33 |
31 32
|
breqtri |
|- ( C +R -1R ) |
34 |
|
ltsosr |
|- |
35 |
|
ltrelsr |
|- |
36 |
34 35
|
sotri |
|- ( ( ( C +R -1R ) ( C +R -1R ) |
37 |
33 36
|
mpan |
|- ( C ( C +R -1R ) |
38 |
2
|
map2psrpr |
|- ( ( C +R -1R ) E. v e. P. ( C +R [ <. v , 1P >. ] ~R ) = x ) |
39 |
37 38
|
sylib |
|- ( C E. v e. P. ( C +R [ <. v , 1P >. ] ~R ) = x ) |
40 |
19 39
|
syl6 |
|- ( A. y e. A y ( C e. A -> E. v e. P. ( C +R [ <. v , 1P >. ] ~R ) = x ) ) |
41 |
|
breq2 |
|- ( ( C +R [ <. v , 1P >. ] ~R ) = x -> ( y . ] ~R ) <-> y |
42 |
41
|
ralbidv |
|- ( ( C +R [ <. v , 1P >. ] ~R ) = x -> ( A. y e. A y . ] ~R ) <-> A. y e. A y |
43 |
1
|
abeq2i |
|- ( w e. B <-> ( C +R [ <. w , 1P >. ] ~R ) e. A ) |
44 |
|
breq1 |
|- ( y = ( C +R [ <. w , 1P >. ] ~R ) -> ( y . ] ~R ) <-> ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) ) ) |
45 |
44
|
rspccv |
|- ( A. y e. A y . ] ~R ) -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A -> ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) ) ) |
46 |
2
|
ltpsrpr |
|- ( ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) <-> w |
47 |
45 46
|
syl6ib |
|- ( A. y e. A y . ] ~R ) -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A -> w |
48 |
43 47
|
syl5bi |
|- ( A. y e. A y . ] ~R ) -> ( w e. B -> w |
49 |
48
|
ralrimiv |
|- ( A. y e. A y . ] ~R ) -> A. w e. B w |
50 |
42 49
|
syl6bir |
|- ( ( C +R [ <. v , 1P >. ] ~R ) = x -> ( A. y e. A y A. w e. B w |
51 |
50
|
com12 |
|- ( A. y e. A y ( ( C +R [ <. v , 1P >. ] ~R ) = x -> A. w e. B w |
52 |
51
|
reximdv |
|- ( A. y e. A y ( E. v e. P. ( C +R [ <. v , 1P >. ] ~R ) = x -> E. v e. P. A. w e. B w |
53 |
40 52
|
syld |
|- ( A. y e. A y ( C e. A -> E. v e. P. A. w e. B w |
54 |
53
|
rexlimivw |
|- ( E. x e. R. A. y e. A y ( C e. A -> E. v e. P. A. w e. B w |
55 |
54
|
impcom |
|- ( ( C e. A /\ E. x e. R. A. y e. A y E. v e. P. A. w e. B w |
56 |
|
supexpr |
|- ( ( B =/= (/) /\ E. v e. P. A. w e. B w E. v e. P. ( A. w e. B -. v E. u e. B w |
57 |
17 55 56
|
syl2anc |
|- ( ( C e. A /\ E. x e. R. A. y e. A y E. v e. P. ( A. w e. B -. v E. u e. B w |
58 |
2
|
mappsrpr |
|- ( ( C +R -1R ) . ] ~R ) <-> v e. P. ) |
59 |
35
|
brel |
|- ( ( C +R -1R ) . ] ~R ) -> ( ( C +R -1R ) e. R. /\ ( C +R [ <. v , 1P >. ] ~R ) e. R. ) ) |
60 |
58 59
|
sylbir |
|- ( v e. P. -> ( ( C +R -1R ) e. R. /\ ( C +R [ <. v , 1P >. ] ~R ) e. R. ) ) |
61 |
60
|
simprd |
|- ( v e. P. -> ( C +R [ <. v , 1P >. ] ~R ) e. R. ) |
62 |
61
|
adantl |
|- ( ( ( C e. A /\ E. x e. R. A. y e. A y ( C +R [ <. v , 1P >. ] ~R ) e. R. ) |
63 |
34 35
|
sotri |
|- ( ( ( C +R -1R ) . ] ~R ) /\ ( C +R [ <. v , 1P >. ] ~R ) ( C +R -1R ) |
64 |
58 63
|
sylanbr |
|- ( ( v e. P. /\ ( C +R [ <. v , 1P >. ] ~R ) ( C +R -1R ) |
65 |
2
|
map2psrpr |
|- ( ( C +R -1R ) E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y ) |
66 |
64 65
|
sylib |
|- ( ( v e. P. /\ ( C +R [ <. v , 1P >. ] ~R ) E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y ) |
67 |
|
rexex |
|- ( E. w e. P. ( C +R [ <. w , 1P >. ] ~R ) = y -> E. w ( C +R [ <. w , 1P >. ] ~R ) = y ) |
68 |
|
df-ral |
|- ( A. w e. B -. v A. w ( w e. B -> -. v |
69 |
|
19.29 |
|- ( ( A. w ( w e. B -> -. v . ] ~R ) = y ) -> E. w ( ( w e. B -> -. v . ] ~R ) = y ) ) |
70 |
|
eleq1 |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> y e. A ) ) |
71 |
43 70
|
syl5bb |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( w e. B <-> y e. A ) ) |
72 |
2
|
ltpsrpr |
|- ( ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) <-> v |
73 |
|
breq2 |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) <-> ( C +R [ <. v , 1P >. ] ~R ) |
74 |
72 73
|
bitr3id |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( v ( C +R [ <. v , 1P >. ] ~R ) |
75 |
74
|
notbid |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( -. v -. ( C +R [ <. v , 1P >. ] ~R ) |
76 |
71 75
|
imbi12d |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( w e. B -> -. v ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R ) |
77 |
76
|
biimpac |
|- ( ( ( w e. B -> -. v . ] ~R ) = y ) -> ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R ) |
78 |
77
|
exlimiv |
|- ( E. w ( ( w e. B -> -. v . ] ~R ) = y ) -> ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R ) |
79 |
69 78
|
syl |
|- ( ( A. w ( w e. B -> -. v . ] ~R ) = y ) -> ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R ) |
80 |
68 79
|
sylanb |
|- ( ( A. w e. B -. v . ] ~R ) = y ) -> ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R ) |
81 |
80
|
expcom |
|- ( E. w ( C +R [ <. w , 1P >. ] ~R ) = y -> ( A. w e. B -. v ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R ) |
82 |
66 67 81
|
3syl |
|- ( ( v e. P. /\ ( C +R [ <. v , 1P >. ] ~R ) ( A. w e. B -. v ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R ) |
83 |
82
|
impd |
|- ( ( v e. P. /\ ( C +R [ <. v , 1P >. ] ~R ) ( ( A. w e. B -. v -. ( C +R [ <. v , 1P >. ] ~R ) |
84 |
83
|
impancom |
|- ( ( v e. P. /\ ( A. w e. B -. v ( ( C +R [ <. v , 1P >. ] ~R ) -. ( C +R [ <. v , 1P >. ] ~R ) |
85 |
84
|
pm2.01d |
|- ( ( v e. P. /\ ( A. w e. B -. v -. ( C +R [ <. v , 1P >. ] ~R ) |
86 |
85
|
expr |
|- ( ( v e. P. /\ A. w e. B -. v ( y e. A -> -. ( C +R [ <. v , 1P >. ] ~R ) |
87 |
86
|
ralrimiv |
|- ( ( v e. P. /\ A. w e. B -. v A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) |
88 |
87
|
ex |
|- ( v e. P. -> ( A. w e. B -. v A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) |
89 |
88
|
adantl |
|- ( ( ( C e. A /\ E. x e. R. A. y e. A y ( A. w e. B -. v A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) |
90 |
|
r19.29 |
|- ( ( A. w e. P. ( w E. u e. B w . ] ~R ) = y ) -> E. w e. P. ( ( w E. u e. B w . ] ~R ) = y ) ) |
91 |
|
breq1 |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) <-> y . ] ~R ) ) ) |
92 |
46 91
|
bitr3id |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( w y . ] ~R ) ) ) |
93 |
92
|
biimprd |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( y . ] ~R ) -> w |
94 |
|
vex |
|- u e. _V |
95 |
|
opeq1 |
|- ( w = u -> <. w , 1P >. = <. u , 1P >. ) |
96 |
95
|
eceq1d |
|- ( w = u -> [ <. w , 1P >. ] ~R = [ <. u , 1P >. ] ~R ) |
97 |
96
|
oveq2d |
|- ( w = u -> ( C +R [ <. w , 1P >. ] ~R ) = ( C +R [ <. u , 1P >. ] ~R ) ) |
98 |
97
|
eleq1d |
|- ( w = u -> ( ( C +R [ <. w , 1P >. ] ~R ) e. A <-> ( C +R [ <. u , 1P >. ] ~R ) e. A ) ) |
99 |
94 98 1
|
elab2 |
|- ( u e. B <-> ( C +R [ <. u , 1P >. ] ~R ) e. A ) |
100 |
|
breq2 |
|- ( z = ( C +R [ <. u , 1P >. ] ~R ) -> ( ( C +R [ <. w , 1P >. ] ~R ) ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) ) ) |
101 |
2
|
ltpsrpr |
|- ( ( C +R [ <. w , 1P >. ] ~R ) . ] ~R ) <-> w |
102 |
100 101
|
bitrdi |
|- ( z = ( C +R [ <. u , 1P >. ] ~R ) -> ( ( C +R [ <. w , 1P >. ] ~R ) w |
103 |
102
|
rspcev |
|- ( ( ( C +R [ <. u , 1P >. ] ~R ) e. A /\ w E. z e. A ( C +R [ <. w , 1P >. ] ~R ) |
104 |
99 103
|
sylanb |
|- ( ( u e. B /\ w E. z e. A ( C +R [ <. w , 1P >. ] ~R ) |
105 |
104
|
rexlimiva |
|- ( E. u e. B w E. z e. A ( C +R [ <. w , 1P >. ] ~R ) |
106 |
|
breq1 |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( C +R [ <. w , 1P >. ] ~R ) y |
107 |
106
|
rexbidv |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( E. z e. A ( C +R [ <. w , 1P >. ] ~R ) E. z e. A y |
108 |
105 107
|
syl5ib |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( E. u e. B w E. z e. A y |
109 |
93 108
|
imim12d |
|- ( ( C +R [ <. w , 1P >. ] ~R ) = y -> ( ( w E. u e. B w ( y . ] ~R ) -> E. z e. A y |
110 |
109
|
impcom |
|- ( ( ( w E. u e. B w . ] ~R ) = y ) -> ( y . ] ~R ) -> E. z e. A y |
111 |
110
|
rexlimivw |
|- ( E. w e. P. ( ( w E. u e. B w . ] ~R ) = y ) -> ( y . ] ~R ) -> E. z e. A y |
112 |
90 111
|
syl |
|- ( ( A. w e. P. ( w E. u e. B w . ] ~R ) = y ) -> ( y . ] ~R ) -> E. z e. A y |
113 |
65 112
|
sylan2b |
|- ( ( A. w e. P. ( w E. u e. B w ( y . ] ~R ) -> E. z e. A y |
114 |
113
|
ex |
|- ( A. w e. P. ( w E. u e. B w ( ( C +R -1R ) ( y . ] ~R ) -> E. z e. A y |
115 |
114
|
adantl |
|- ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w E. u e. B w ( ( C +R -1R ) ( y . ] ~R ) -> E. z e. A y |
116 |
115
|
a1dd |
|- ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w E. u e. B w ( ( C +R -1R ) ( y e. R. -> ( y . ] ~R ) -> E. z e. A y |
117 |
34 35
|
sotri2 |
|- ( ( y e. R. /\ -. ( C +R -1R ) y |
118 |
33 117
|
mp3an3 |
|- ( ( y e. R. /\ -. ( C +R -1R ) y |
119 |
|
breq2 |
|- ( z = C -> ( y y |
120 |
119
|
rspcev |
|- ( ( C e. A /\ y E. z e. A y |
121 |
120
|
ex |
|- ( C e. A -> ( y E. z e. A y |
122 |
121
|
a1dd |
|- ( C e. A -> ( y ( y . ] ~R ) -> E. z e. A y |
123 |
118 122
|
syl5 |
|- ( C e. A -> ( ( y e. R. /\ -. ( C +R -1R ) ( y . ] ~R ) -> E. z e. A y |
124 |
123
|
expcomd |
|- ( C e. A -> ( -. ( C +R -1R ) ( y e. R. -> ( y . ] ~R ) -> E. z e. A y |
125 |
124
|
ad2antrr |
|- ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w E. u e. B w ( -. ( C +R -1R ) ( y e. R. -> ( y . ] ~R ) -> E. z e. A y |
126 |
116 125
|
pm2.61d |
|- ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w E. u e. B w ( y e. R. -> ( y . ] ~R ) -> E. z e. A y |
127 |
126
|
ralrimiv |
|- ( ( ( C e. A /\ v e. P. ) /\ A. w e. P. ( w E. u e. B w A. y e. R. ( y . ] ~R ) -> E. z e. A y |
128 |
127
|
ex |
|- ( ( C e. A /\ v e. P. ) -> ( A. w e. P. ( w E. u e. B w A. y e. R. ( y . ] ~R ) -> E. z e. A y |
129 |
128
|
adantlr |
|- ( ( ( C e. A /\ E. x e. R. A. y e. A y ( A. w e. P. ( w E. u e. B w A. y e. R. ( y . ] ~R ) -> E. z e. A y |
130 |
89 129
|
anim12d |
|- ( ( ( C e. A /\ E. x e. R. A. y e. A y ( ( A. w e. B -. v E. u e. B w ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) -> E. z e. A y |
131 |
|
breq1 |
|- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( x ( C +R [ <. v , 1P >. ] ~R ) |
132 |
131
|
notbid |
|- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( -. x -. ( C +R [ <. v , 1P >. ] ~R ) |
133 |
132
|
ralbidv |
|- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( A. y e. A -. x A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) |
134 |
|
breq2 |
|- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( y y . ] ~R ) ) ) |
135 |
134
|
imbi1d |
|- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( ( y E. z e. A y ( y . ] ~R ) -> E. z e. A y |
136 |
135
|
ralbidv |
|- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( A. y e. R. ( y E. z e. A y A. y e. R. ( y . ] ~R ) -> E. z e. A y |
137 |
133 136
|
anbi12d |
|- ( x = ( C +R [ <. v , 1P >. ] ~R ) -> ( ( A. y e. A -. x E. z e. A y ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) -> E. z e. A y |
138 |
137
|
rspcev |
|- ( ( ( C +R [ <. v , 1P >. ] ~R ) e. R. /\ ( A. y e. A -. ( C +R [ <. v , 1P >. ] ~R ) . ] ~R ) -> E. z e. A y E. x e. R. ( A. y e. A -. x E. z e. A y |
139 |
62 130 138
|
syl6an |
|- ( ( ( C e. A /\ E. x e. R. A. y e. A y ( ( A. w e. B -. v E. u e. B w E. x e. R. ( A. y e. A -. x E. z e. A y |
140 |
139
|
rexlimdva |
|- ( ( C e. A /\ E. x e. R. A. y e. A y ( E. v e. P. ( A. w e. B -. v E. u e. B w E. x e. R. ( A. y e. A -. x E. z e. A y |
141 |
57 140
|
mpd |
|- ( ( C e. A /\ E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y |