Step |
Hyp |
Ref |
Expression |
1 |
|
frpoinsg.1 |
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ y e. A ) -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) ) |
2 |
|
dfss3 |
|- ( Pred ( R , A , w ) C_ { y e. A | ph } <-> A. z e. Pred ( R , A , w ) z e. { y e. A | ph } ) |
3 |
|
nfcv |
|- F/_ y A |
4 |
3
|
elrabsf |
|- ( z e. { y e. A | ph } <-> ( z e. A /\ [. z / y ]. ph ) ) |
5 |
4
|
simprbi |
|- ( z e. { y e. A | ph } -> [. z / y ]. ph ) |
6 |
5
|
ralimi |
|- ( A. z e. Pred ( R , A , w ) z e. { y e. A | ph } -> A. z e. Pred ( R , A , w ) [. z / y ]. ph ) |
7 |
2 6
|
sylbi |
|- ( Pred ( R , A , w ) C_ { y e. A | ph } -> A. z e. Pred ( R , A , w ) [. z / y ]. ph ) |
8 |
|
nfv |
|- F/ y ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) |
9 |
|
nfcv |
|- F/_ y Pred ( R , A , w ) |
10 |
|
nfsbc1v |
|- F/ y [. z / y ]. ph |
11 |
9 10
|
nfralw |
|- F/ y A. z e. Pred ( R , A , w ) [. z / y ]. ph |
12 |
|
nfsbc1v |
|- F/ y [. w / y ]. ph |
13 |
11 12
|
nfim |
|- F/ y ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) |
14 |
8 13
|
nfim |
|- F/ y ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) |
15 |
|
eleq1w |
|- ( y = w -> ( y e. A <-> w e. A ) ) |
16 |
15
|
anbi2d |
|- ( y = w -> ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ y e. A ) <-> ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) ) ) |
17 |
|
predeq3 |
|- ( y = w -> Pred ( R , A , y ) = Pred ( R , A , w ) ) |
18 |
17
|
raleqdv |
|- ( y = w -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph <-> A. z e. Pred ( R , A , w ) [. z / y ]. ph ) ) |
19 |
|
sbceq1a |
|- ( y = w -> ( ph <-> [. w / y ]. ph ) ) |
20 |
18 19
|
imbi12d |
|- ( y = w -> ( ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) <-> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) ) |
21 |
16 20
|
imbi12d |
|- ( y = w -> ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ y e. A ) -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) ) <-> ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) ) ) |
22 |
14 21 1
|
chvarfv |
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) |
23 |
7 22
|
syl5 |
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> [. w / y ]. ph ) ) |
24 |
|
simpr |
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> w e. A ) |
25 |
23 24
|
jctild |
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> ( w e. A /\ [. w / y ]. ph ) ) ) |
26 |
3
|
elrabsf |
|- ( w e. { y e. A | ph } <-> ( w e. A /\ [. w / y ]. ph ) ) |
27 |
25 26
|
syl6ibr |
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) ) |
28 |
27
|
ralrimiva |
|- ( ( R Fr A /\ R Po A /\ R Se A ) -> A. w e. A ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) ) |
29 |
|
ssrab2 |
|- { y e. A | ph } C_ A |
30 |
28 29
|
jctil |
|- ( ( R Fr A /\ R Po A /\ R Se A ) -> ( { y e. A | ph } C_ A /\ A. w e. A ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) ) ) |
31 |
|
frpoind |
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( { y e. A | ph } C_ A /\ A. w e. A ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) ) ) -> A = { y e. A | ph } ) |
32 |
30 31
|
mpdan |
|- ( ( R Fr A /\ R Po A /\ R Se A ) -> A = { y e. A | ph } ) |
33 |
|
rabid2 |
|- ( A = { y e. A | ph } <-> A. y e. A ph ) |
34 |
32 33
|
sylib |
|- ( ( R Fr A /\ R Po A /\ R Se A ) -> A. y e. A ph ) |