Step |
Hyp |
Ref |
Expression |
1 |
|
caofref.1 |
|- ( ph -> A e. V ) |
2 |
|
caofref.2 |
|- ( ph -> F : A --> S ) |
3 |
|
caofcom.3 |
|- ( ph -> G : A --> S ) |
4 |
|
caofrss.4 |
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y -> x T y ) ) |
5 |
2
|
ffvelrnda |
|- ( ( ph /\ w e. A ) -> ( F ` w ) e. S ) |
6 |
3
|
ffvelrnda |
|- ( ( ph /\ w e. A ) -> ( G ` w ) e. S ) |
7 |
4
|
ralrimivva |
|- ( ph -> A. x e. S A. y e. S ( x R y -> x T y ) ) |
8 |
7
|
adantr |
|- ( ( ph /\ w e. A ) -> A. x e. S A. y e. S ( x R y -> x T y ) ) |
9 |
|
breq1 |
|- ( x = ( F ` w ) -> ( x R y <-> ( F ` w ) R y ) ) |
10 |
|
breq1 |
|- ( x = ( F ` w ) -> ( x T y <-> ( F ` w ) T y ) ) |
11 |
9 10
|
imbi12d |
|- ( x = ( F ` w ) -> ( ( x R y -> x T y ) <-> ( ( F ` w ) R y -> ( F ` w ) T y ) ) ) |
12 |
|
breq2 |
|- ( y = ( G ` w ) -> ( ( F ` w ) R y <-> ( F ` w ) R ( G ` w ) ) ) |
13 |
|
breq2 |
|- ( y = ( G ` w ) -> ( ( F ` w ) T y <-> ( F ` w ) T ( G ` w ) ) ) |
14 |
12 13
|
imbi12d |
|- ( y = ( G ` w ) -> ( ( ( F ` w ) R y -> ( F ` w ) T y ) <-> ( ( F ` w ) R ( G ` w ) -> ( F ` w ) T ( G ` w ) ) ) ) |
15 |
11 14
|
rspc2va |
|- ( ( ( ( F ` w ) e. S /\ ( G ` w ) e. S ) /\ A. x e. S A. y e. S ( x R y -> x T y ) ) -> ( ( F ` w ) R ( G ` w ) -> ( F ` w ) T ( G ` w ) ) ) |
16 |
5 6 8 15
|
syl21anc |
|- ( ( ph /\ w e. A ) -> ( ( F ` w ) R ( G ` w ) -> ( F ` w ) T ( G ` w ) ) ) |
17 |
16
|
ralimdva |
|- ( ph -> ( A. w e. A ( F ` w ) R ( G ` w ) -> A. w e. A ( F ` w ) T ( G ` w ) ) ) |
18 |
2
|
ffnd |
|- ( ph -> F Fn A ) |
19 |
3
|
ffnd |
|- ( ph -> G Fn A ) |
20 |
|
inidm |
|- ( A i^i A ) = A |
21 |
|
eqidd |
|- ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) ) |
22 |
|
eqidd |
|- ( ( ph /\ w e. A ) -> ( G ` w ) = ( G ` w ) ) |
23 |
18 19 1 1 20 21 22
|
ofrfval |
|- ( ph -> ( F oR R G <-> A. w e. A ( F ` w ) R ( G ` w ) ) ) |
24 |
18 19 1 1 20 21 22
|
ofrfval |
|- ( ph -> ( F oR T G <-> A. w e. A ( F ` w ) T ( G ` w ) ) ) |
25 |
17 23 24
|
3imtr4d |
|- ( ph -> ( F oR R G -> F oR T G ) ) |