Step |
Hyp |
Ref |
Expression |
1 |
|
dmrelrnrel.x |
|- F/ x ph |
2 |
|
dmrelrnrel.y |
|- F/ y ph |
3 |
|
dmrelrnrel.i |
|- ( ph -> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) |
4 |
|
dmrelrnrel.b |
|- ( ph -> B e. A ) |
5 |
|
dmrelrnrel.c |
|- ( ph -> C e. A ) |
6 |
|
dmrelrnrel.r |
|- ( ph -> B R C ) |
7 |
|
id |
|- ( ph -> ph ) |
8 |
7 4 5
|
jca31 |
|- ( ph -> ( ( ph /\ B e. A ) /\ C e. A ) ) |
9 |
|
nfv |
|- F/ y B e. A |
10 |
2 9
|
nfan |
|- F/ y ( ph /\ B e. A ) |
11 |
|
nfv |
|- F/ y C e. A |
12 |
10 11
|
nfan |
|- F/ y ( ( ph /\ B e. A ) /\ C e. A ) |
13 |
|
nfv |
|- F/ y ( B R C -> ( F ` B ) S ( F ` C ) ) |
14 |
12 13
|
nfim |
|- F/ y ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) |
15 |
9 14
|
nfim |
|- F/ y ( B e. A -> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) |
16 |
|
eleq1 |
|- ( y = C -> ( y e. A <-> C e. A ) ) |
17 |
16
|
anbi2d |
|- ( y = C -> ( ( ( ph /\ B e. A ) /\ y e. A ) <-> ( ( ph /\ B e. A ) /\ C e. A ) ) ) |
18 |
|
breq2 |
|- ( y = C -> ( B R y <-> B R C ) ) |
19 |
|
fveq2 |
|- ( y = C -> ( F ` y ) = ( F ` C ) ) |
20 |
19
|
breq2d |
|- ( y = C -> ( ( F ` B ) S ( F ` y ) <-> ( F ` B ) S ( F ` C ) ) ) |
21 |
18 20
|
imbi12d |
|- ( y = C -> ( ( B R y -> ( F ` B ) S ( F ` y ) ) <-> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) |
22 |
17 21
|
imbi12d |
|- ( y = C -> ( ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) <-> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) ) |
23 |
22
|
imbi2d |
|- ( y = C -> ( ( B e. A -> ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) ) <-> ( B e. A -> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) ) ) |
24 |
|
nfv |
|- F/ x B e. A |
25 |
1 24
|
nfan |
|- F/ x ( ph /\ B e. A ) |
26 |
|
nfv |
|- F/ x y e. A |
27 |
25 26
|
nfan |
|- F/ x ( ( ph /\ B e. A ) /\ y e. A ) |
28 |
|
nfv |
|- F/ x ( B R y -> ( F ` B ) S ( F ` y ) ) |
29 |
27 28
|
nfim |
|- F/ x ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) |
30 |
|
eleq1 |
|- ( x = B -> ( x e. A <-> B e. A ) ) |
31 |
30
|
anbi2d |
|- ( x = B -> ( ( ph /\ x e. A ) <-> ( ph /\ B e. A ) ) ) |
32 |
31
|
anbi1d |
|- ( x = B -> ( ( ( ph /\ x e. A ) /\ y e. A ) <-> ( ( ph /\ B e. A ) /\ y e. A ) ) ) |
33 |
|
breq1 |
|- ( x = B -> ( x R y <-> B R y ) ) |
34 |
|
fveq2 |
|- ( x = B -> ( F ` x ) = ( F ` B ) ) |
35 |
34
|
breq1d |
|- ( x = B -> ( ( F ` x ) S ( F ` y ) <-> ( F ` B ) S ( F ` y ) ) ) |
36 |
33 35
|
imbi12d |
|- ( x = B -> ( ( x R y -> ( F ` x ) S ( F ` y ) ) <-> ( B R y -> ( F ` B ) S ( F ` y ) ) ) ) |
37 |
32 36
|
imbi12d |
|- ( x = B -> ( ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( x R y -> ( F ` x ) S ( F ` y ) ) ) <-> ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) ) ) |
38 |
3
|
r19.21bi |
|- ( ( ph /\ x e. A ) -> A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) |
39 |
38
|
r19.21bi |
|- ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( x R y -> ( F ` x ) S ( F ` y ) ) ) |
40 |
29 37 39
|
vtoclg1f |
|- ( B e. A -> ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) ) |
41 |
15 23 40
|
vtoclg1f |
|- ( C e. A -> ( B e. A -> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) ) |
42 |
5 4 41
|
sylc |
|- ( ph -> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) |
43 |
8 6 42
|
mp2d |
|- ( ph -> ( F ` B ) S ( F ` C ) ) |